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

【问题标题】：How to prove False from obviously contradictory assumptions如何从明显矛盾的假设中证明 False
【发布时间】：2015-03-26 18:56:05
【问题描述】：

假设我想证明以下定理：

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.

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

【问题讨论】：

标签： coq proof

【解决方案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.

【讨论】：

或者更简洁但仍然明确：intros n m H <-; discriminate H.（不太明确的intros; subst; discriminate.也可以）。

【解决方案2】：

有一个非常简单的方法来证明它：

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

congruence 策略是一种在未解释符号上进行地面平等的决策程序。对于未解释的符号和构造函数来说它是完整的，所以在这种情况下，它可以证明相等 0 = m 是不可能的。

【讨论】：

【解决方案3】：

了解全等的工作原理可能很有用。

为了证明由不同构造函数构造的两个项实际上是不同的，只需创建一个函数，在一种情况下返回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.

【讨论】：