我只是 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。但是，我就是不知道如何进行这种简单的简化。
【问题讨论】：
标签： coq simplification
一种简化的方法是使用一个相当无聊的引理
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.
【讨论】：
induction n as [| n1 IHn1] 将IHn 的名称更改为IHn1。
a + 0 = a 等几个常见的引理被放入提示数据库arith。有了它们，auto 通常可以解决很多此类简单的目标，所以使用auto with arith.
Require Import Arith.
Theorem add_increase: (forall a b: nat, a > 0 -> a + b > b).
destruct a; intros b H.
- inversion H. (* base case, H: 0 > 0 *)
- simpl. auto with arith.
Qed.
要查看auto 使用了哪些引理，您可以Print add_increase. 在这种情况下，auto 使用了三个引理，也可以通过auto using gt_le_S, le_lt_n_Sm, le_plus_r. 将它们显式赋予 auto
一般来说，当您需要一个您认为应该已经被证明的引理时，您可以使用SearchAbout 搜索它。使用_ 作为通配符，或使用?a 作为命名通配符。在你上面的例子中，你想要在右边添加一个零，所以
SearchAbout ( _ + 0 = _ ).
返回
plus_0_r: forall n : nat, n + 0 = n
NPeano.Nat.add_0_r: forall n : nat, n + 0 = n
您甚至可以在库中找到与您要证明的内容相近的引理。
SearchAbout ( _ > _ -> _ + _ > _ ).
发现
plus_gt_compat_l: forall n m p : nat, n > m -> p + n > p + m
非常接近add_increase。
Theorem add_increase: (forall a b: nat, a > 0 -> a + b > b).
intros.
pose (plus_gt_compat_l a 0 b H) as A.
repeat rewrite (plus_comm b) in A.
apply A.
Qed.
【讨论】：
a+0=a 不是0...
使用不同的自然数库ssrnat 和 ssreflect 证明语言（库需要）的另一种解决方案：
From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq.
Theorem add_increase a b : 0 < a -> b < a + b.
Proof. by rewrite -{1}[b]add0n ltn_add2r. Qed.
ltn_add2r : (m + p < n + p) = (m < n) 引理由p 的归纳证明，直接由p 的归纳证明，加上交换性和其他简单的加法性质。
【讨论】：
请注意，如果我们调用 omega 策略，我们可以这样做：
Theorem add_increase : forall a b: nat, a > 0 -> a + b > b.
Proof. intros a b. omega. Qed.
【讨论】：