Coq 初学者 - 证明一个基本引理

Question

我是 Coq 的初学者，所以我的问题可能看起来很愚蠢，但这是我的问题：

我定义了一个简单的模块，其中我定义了一个类型 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

这是一个典型的初学者陷阱。问题是当 y 已经在您的上下文中引入时，您对 x 进行了归纳。因此，您获得的归纳假设不够普遍：您真正想要的是

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.

以交互方式尝试运行这个证明，并检查当你到达第二种情况时归纳假设如何变化。

Coq 初学者 - 证明一个基本引理

Coq beginner - Prove a basic lemma

coq