coq - 如何将 A + 0 > 0 简化为 A > 0？

Question

我只是 Coq 的初学者，我一直在尝试证明一些关于自然数的基本定理。我已经做了一些，不是很优雅，但完成得更少。但是我完全坚持完成这个定理:

Theorem add_increase: (forall a b: nat, a > 0 -> a + b > b).
Proof.
  intros A.
  intros B.
  intros H.
  case B.

输入这个，我得到这个输出:

2 subgoals
A, B : nat
H : A > 0
______________________________________(1/2)
A + 0 > 0
______________________________________(2/2)
forall n : nat, A + S n > S n

显然，第一个目标很容易简化为假设 H .但是，我无法弄清楚如何进行这种直接的简化。

Answer 1

简化这一点的一种方法是使用一个相当无聊的引理

Lemma add_zero_r : forall n, n + 0 = n.
Proof.
  intros n. induction n. reflexivity.
  simpl. rewrite IHn. reflexivity.
Qed.

接下来用它来重写你的目标:

Theorem add_increase: (forall a b: nat, a > 0 -> a + b > b).
Proof.
  intros A.
  intros B.
  intros H.
  case B.
  rewrite (add_zero_r A).
  assumption.

为了完成另一个证明案例，我使用了一个小引理和一种策略，以简化证明自然数不等式的任务。

首先，我导入了 Omega图书馆。

Require Import Omega.

证明另一个无聊的事实。

Lemma add_succ_r : forall n m, n + (S m) = S (n + m).
Proof.
  intros n m. induction n. reflexivity.
  simpl. rewrite IHn. reflexivity.
Qed.

然后返回 add_increase prove我们有以下目标:

A, B : nat
H : A > 0
============================
forall n : nat, A + S n > S n

可以通过以下方式解决:

 intros C.
 rewrite (add_succ_r A C).
 omega.

再一次，我使用了之前的证明引理来重写目标。 omega战术是一种非常有用的方法，因为它是所谓的 quantifier free Presburger arithmetic 的完整决策程序。 ，并根据您的上下文，它可以解决目标 automagically .

这是您证明的完整解决方案:

 Require Import Omega.

 Lemma add_zero_r : forall n, n + 0 = n.
 Proof.
   intros n. induction n. reflexivity.
   simpl. rewrite IHn. reflexivity.
 Qed.

 Lemma add_succ_r : forall n m, n + (S m) = S (n + m).
 Proof.
  intros n m. induction n. reflexivity.
  simpl. rewrite IHn. reflexivity.
 Qed.

Theorem add_increase: (forall a b: nat, a > 0 -> a + b > b).
Proof.
  intros A.
  intros B.
  intros H.
  case B.
  rewrite (add_zero_r A).
  assumption.
  intros C.
  rewrite (add_succ_r A C).
  omega.
 Qed.