如何解决Coq 证明无意义的归纳属性蕴涵?
在来自 Logical Foundations 的 IndProp.v 中,我们有以下归纳属性:
Inductive nostutter {X:Type} : list X -> Prop :=
| nos_nil : nostutter []
| nos_one : forall x,nostutter [x]
| nos_cons : forall x h l,nostutter (h :: l) -> (x <> h) -> (nostutter (x :: h :: l)).
是否可以解决这个问题:
1 subgoal
X : Type
x : X
H : nostutter [] -> nostutter [x]
______________________________________(1/1)
False
大概需要某种歧视或矛盾,因为 nostutter [] -> nostutter [x]
似乎没有意义,但我看不出有什么可以让我取得进展。只是无法证明吗?
解决方法
我认为对于含义的含义存在一些混淆。 nostutter [] -> nostutter [x]
是一个完全合理的假设——事实上,它是一个定理:
Require Import Coq.Lists.List.
Import ListNotations.
Inductive nostutter {X:Type} : list X -> Prop :=
| nos_nil : nostutter []
| nos_one : forall x,nostutter [x]
| nos_cons : forall x h l,nostutter (h :: l) -> (x <> h) -> (nostutter (x :: h :: l)).
Lemma not_goal {X} (x : X) : @nostutter X [] -> nostutter [x].
Proof. intros _; apply nos_one. Qed.
蕴涵 A -> B
表示我们可以通过证明 B
为真来证明 A
。如果我们可以在没有额外假设的情况下证明 B
,就像 nostutter [x]
的情况一样,那么蕴涵是微不足道的。
版权声明:本文内容由互联网用户自发贡献,该文观点与技术仅代表作者本人。本站仅提供信息存储空间服务,不拥有所有权,不承担相关法律责任。如发现本站有涉嫌侵权/违法违规的内容, 请发送邮件至 dio@foxmail.com 举报,一经查实,本站将立刻删除。