如何处理"false = true"；证明定理中的命题 [英] How to deal with "false = true" proposition while proving theorems in coq

问题描述

我不熟悉coq并试图证明这个定理

I am new to coq and trying to prove this theorem

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.

到目前为止，这是我的解决方法

This is my solution so far

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)"为0.应当遵循命题"false = true"；如果该定理必须是正确的，但我不知道该怎么做并继续我的证明.任何帮助将不胜感激.

I understand that this output means that the proposition "Var 0 = Var (S n)" should follow from the proposition "false = true" if the theorem has to be correct, but I don't know what to do about it and move ahead with my proof. Any help would be appreciated.

提前谢谢！

推荐答案

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

Another option: instead of inversion, use congruence:

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

此策略专用于利用构造函数的不相交性.

This tactic is dedicated to exploiting disjointness of constructors.

这篇关于如何处理"false = true"；证明定理中的命题的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！