Coq 中的后继者不相等

Question

我试图在 Coq 中证明以下引理：

Lemma not_eq_S2: forall m n, S m <> S n -> m <> n.

这似乎很容易，但我不知道如何完成证明。有人可以帮我吗？

谢谢你。

Answer 1

需要知道的是，在 Coq 中，否定是一个暗示 的函数False，所以S m <> S n实际上是S m = S n -> False。因此，与其证明n <> m我们可以引入n = m（我们可以展开not或intros明确告诉去做）并获得目标False。但是 withn = m在上下文中，我们可以重写HS: S n <> S m为HS: S n <> S n，可以由auto或许多其他策略（例如apply HS. reflexivity.或congruence.等）处理。

Lemma not_eq_S2: forall m n, S m <> S n -> m <> n.

Proof. intros m n HS HC. 
  rewrite HC in HS. auto.
Qed.