勒柯克初学者 - 证明了一个基本引理

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. 

尝试交互的运行证明了这一点，并检查归纳假设当你到达第二种情况如何变化。