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

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 是不可能的。

Answer 3

了解同余的工作原理可能会有用。

为了证明由不同的构造函数构造的两个项实际上是不同的，只需创建一个函数，一种情况下 returns True 另一种情况下 False ，然后用它来证明True = False。我认为这在 Coq'Art

中有解释

Example not_congruent: 0 <> 1.
  intros C. (* now our goal is 'False' *)
  pose (fun m=>match m with 0=>True |S _=>False end) as f.
  assert (Contra: f 1 = f 0) by (rewrite C; reflexivity).
  now replace False with True by Contra.
Qed.

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

How to prove False from obviously contradictory assumptions

proof

coq