coq - 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反而。但与 n = 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.