如何解决在coq中证明定理时如何处理“false = true”命题
我是 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”,但我不知道该怎么做它并继续我的证明。任何帮助将不胜感激。
提前致谢!
解决方法
另一种选择:使用 inversion
代替 congruence
:
Goal false=true -> False.
congruence.
Qed.
这种策略致力于利用构造函数的不相交性。
,在以下假设中使用 inversion
:
Goal false=true -> False.
intros H.
inversion H.
Qed.
,
另一种选择,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.
版权声明:本文内容由互联网用户自发贡献,该文观点与技术仅代表作者本人。本站仅提供信息存储空间服务,不拥有所有权,不承担相关法律责任。如发现本站有涉嫌侵权/违法违规的内容, 请发送邮件至 dio@foxmail.com 举报,一经查实,本站将立刻删除。