如何从明显矛盾的假设中证明是假的

Question

假设我想证明以下定理:

Theorem succ_neq_zero : forall n m: nat, S n = m -> 0 = m -> False.

这个是微不足道的m,因为假设不能同时为后继和零.但是我发现证明这一点非常棘手,而且我不知道如何在没有辅助引理的情况下制作它:

Lemma succ_neq_zero_lemma : forall n : nat, O = S n -> False.
Proof.
  intros.
  inversion H.
Qed.

Theorem succ_neq_zero : forall n m: nat, S n = m -> 0 = m -> False.
Proof.
  intros.
  symmetry in H.
  apply (succ_neq_zero_lemma n).
  transitivity m.
  assumption.
  assumption.
Qed.

我很确定有更好的方法来证明这一点.最好的方法是什么？

Answer 1

你只需要m在第一个等式中替换:

Theorem succ_neq_zero : forall n m: nat, S n = m -> 0 = m -> False.
Proof.
intros n m H1 H2; rewrite <- H2 in H1; inversion H1.
Qed.

Answer 2

有一种非常简单的方法来证明它:

Theorem succ_neq_zero : forall n m: nat, S n = m -> 0 = m -> False.
Proof.
  congruence.
Qed.

该congruence策略是对未解释的符号地面平等的决定过程.对于未解释的符号和构造函数来说,它是完整的,所以在这样的情况下,它可以证明相等0 = m是不可能的.