關於小於

Question

的證明我試圖在Coq中證明一些關於less_than的定理。我 使用這個歸納定義：

Inductive less_than : nat->nat->Prop := 
    | lt1 : forall a, less_than O (S a) 
    | lt2 : forall a b, less_than a b -> less_than a (S b) 
    | lt3 : forall a b, less_than a b -> less_than (S a) (S b). 

，我總是最終需要顯示LT3的倒數，

Lemma inv_lt3, forall a b, less_than (S a) (S b) -> less_than a b. 
Proof. 
    ??? 

我卡住了，會很感激，如果有人有一些提示如何繼續。

（是不是有什麼毛病我的less_than歸納定義？）

謝謝！

Answer 1

首先，您的less_than的定義有點不幸，因爲第二個構造函數是多餘的。您應該考慮切換到簡單：

Inductive less_than : nat -> nat -> Prop := 
| ltO : forall a, less_than O (S a) 
| ltS : forall a b, less_than a b -> less_than (S a) (S b) 
. 

的反轉將隨後的比賽COQ的反轉，使您證明瑣碎：

Lemma inv_ltS: forall a b, less_than (S a) (S b) -> less_than a b. 
Proof. now inversion 1. Qed. 

的第二句話是多餘的，因爲對於每對(a, b) ST。您需要less_than a b的證明，您可以隨時申請lt3a次，然後申請lt1。你lt2其實是在其他兩個構造函數的結果：

Ltac inv H := inversion H; subst; clear H; try tauto. 

(* there is probably an easier way to do that? *) 
Lemma lt2 : forall a b, less_than a b -> less_than a (S b). 
Proof. 
    intros a b. revert a. induction b; intros. 
    inv H. 
    inv H. 
    apply ltO. 
    apply ltS. now apply IHb. 
Qed. 

---

現在，如果你真的想保持你的特定的定義，這裏是你如何試圖證明：

Lemma inv_lt: forall a b, less_than (S a) (S b) -> less_than a b. 
Proof. 
    induction b; intros. 
    inv H. inv H2. 
    inv H. apply lt2. now apply IHb. 
Qed.