如何处理"false = true";证明定理中的命题 [英] How to deal with "false = true" proposition while proving theorems in coq
本文介绍了如何处理"false = true";证明定理中的命题的处理方法,对大家解决问题具有一定的参考价值,需要的朋友们下面随着小编来一起学习吧!
问题描述
我不熟悉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屋!
查看全文