如何将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.

Answer 2

另一种使用不同自然数库的解决方案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 上的归纳法加上交换律和其他简单的加法性质证明。

Answer 3

提示数据库arith中放入了a + 0 = a等几个常用词条。有了它们，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 使用了三个引理，也可以通过 [=23= 将它们显式指定给 auto ]

一般来说，当你需要一个你认为应该已经证明的引理时，你可以用SearchAbout搜索它。使用 _ 作为通配符，或使用 ?a 作为命名通配符。在你上面的例子中，你想要在右边加一个零，所以

SearchAbout ( _ + 0 =  _ ).

returns

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.

Answer 4

请注意，如果我们调用 omega 策略，我们可以这样做：

Theorem add_increase : forall a b: nat, a > 0 -> a + b > b.
Proof. intros a b. omega. Qed.

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

How to simplify A + 0 > 0 into A > 0?

simplification

coq