在 coq 中证明定理时如何处理“false = true”命题答案

【问题标题】：How to deal with "false = true" proposition while proving theorems in coq在 coq 中证明定理时如何处理“false = true”命题
【发布时间】：2021-03-28 13:44:01
【问题描述】：

我是 coq 的新手并试图证明这个定理

Inductive expression : Type :=
  | Var (n : nat)
.
.

Theorem variable_equality : forall x : nat, forall n : nat,
  ((equals x n) = true) -> (Var x = Var n).

这是等于的定义


Fixpoint equals (n1 : nat) (n2 : nat) :=
  match (n1, n2) with
    | (O, O)      => true
    | (O, S n)    => false
    | (S n, O)    => false
    | (S n, S n') => equals n n'
  end.

这是我目前的解决方案

Proof.
intros x n. induction x as [| x' IH].
  - destruct n. 
    + reflexivity.
    + simpl. intro.

我最终会得到这样的结果

1 subgoal 
n : nat
H : false = true
-------------------------
Var 0 = Var (S n)

我知道这个输出意味着如果定理必须是正确的，那么命题“Var 0 = Var (S n)”应该遵循命题“false = true”，但我不知道该怎么办继续我的证明。

【问题讨论】：

标签： coq proof theorem

【解决方案1】：

另一种选择，discriminate，这是针对此类目标的专用策略：它应该完全解决此类问题（即假设中不同构造函数的相等性），仅此而已。

Goal false = true -> False.
discriminate.
Qed.

此外，它是一个终结者，这意味着如果在使用后目标没有解决，它就会失败，而 inversion 和 congruence 在某些情况下会成功解决预期的问题并以“意想不到的”方式取得成功。

例如

Goal true = true -> True.
inversion 1.
Qed.

和

Goal true = true -> S 1 = S 1.
congruence.
Qed.

就个人而言，我使用来自 ssreflect 的by []（它也是一个终结者）来实现此类目标和所有“微不足道”的目标：

Require Import ssreflect.

Goal false = true -> False.
by [].
Qed.

【讨论】：

【解决方案2】：

另一种选择：代替inversion，使用congruence：

Goal false=true -> False.
  congruence.
Qed.

这种策略专门用于利用构造函数的不相交性。

【讨论】：

【解决方案3】：

在如下假设上使用inversion：

Goal false=true -> False.
intros H.
inversion H.
Qed.

【讨论】：