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

Question

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

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

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

这是equals的定义

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”，但我不知道该怎么做并移动继续我的证明。

Answer 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.

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

Require Import ssreflect.

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

Answer 2

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

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

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

Answer 3

用于inversion以下假设：

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