勒柯克初學者 - 證明了一個基本引理

Question

我與勒柯克所以也許我的問題初學者也似乎是一個愚蠢的問題，但這裏是我的問題：

我定義中，我定義的類型單模T和功能「my_custom_equal」：

Definition T := nat. 

    Fixpoint my_custom_equal (x y : T) := 
    match x, y with 
     | O, O => true 
     | O, S _ => false 
     | S _, O => false 
     | S sub_x, S sub_y => my_custom_equal sub_x sub_y 
    end. 

    Lemma my_custom_reflex : forall x : T, my_custom_equal x x = true. 
    Proof. 
    intros. 
    induction x. 
    simpl. 
    reflexivity. 
    simpl. 
    rewrite IHx. 
    reflexivity. 
    Qed. 

    Lemma my_custom_unicite : forall x y : T, my_custom_equal x y = true -> x = y. 
    Proof. 
    intros. 
    induction x. 
    induction y. 
    reflexivity. 
    discriminate. 

    Qed. 

正如你所看到的，它是不是很複雜，但我仍然被困在my_custom_unicite證明，我總是達不到，我需要證明的一點是「S X = y「，我的假設是：

y : nat 
H : my_custom_equal 0 (S y) = true 
IHy : my_custom_equal 0 y = true -> 0 = y 
______________________________________(1/1) 
S x = y 

我不明白如何達到這個證明，你能幫我嗎？

謝謝！

Answer 1

這是初學者的典型陷阱。問題是你在x上執行了歸納，此時y已經在您的上下文中引入。正因爲如此，你獲得的歸納假設不充分概括：你真正想要的是有像

forall y, my_custom_equal x y = true -> x = y 

注意額外的forall。解決的辦法是把y回到你的目標：

Lemma my_custom_unicite : forall x y, my_custom_equal x y = true -> x = y. 
Proof. 
intros x y. revert y. 
induction x as [|x IH]. 
- intros []; easy. 
- intros [|y]; try easy. 
    simpl. 
    intros H. 
    rewrite (IH y H). 
    reflexivity. 
Qed. 

嘗試交互的運行證明了這一點，並檢查歸納假設當你到達第二種情況如何變化。