如何將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

幾個常見的引理如a + 0 = 0等都放在提示數據庫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.

自動通常，當你需要一個你認爲應該已經被證明的引理時，你可以用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.