gpt4 book ai didi

coq - Coq 中的反例证明

转载 作者:行者123 更新时间:2023-12-04 16:15:27 27 4
gpt4 key购买 nike

在命题和谓词演算中证明了数十个引理后(有些比其他的更具挑战性,但通常仍然可以在 intro-apply-destruct 自动驾驶仪上证明)我从 ~forall 开始打了一个并立即被捕获。显然,我缺乏对 Coq 的理解和知识。所以,我要求使用低级 Coq 技术来证明一般形式的语句

~forall A [B].., C -> D.  
exists A [B].., ~(C -> D).

换句话说,我希望有一个通用的 Coq 方法来设置和触发反例。 (量化上述函数的主要原因是它是 Coq 中的(或)原始连接词。)如果你想要例子,我建议例如
~forall P Q: Prop, P -> Q.
~forall P: Prop, P -> ~P.

有一个 related question它既没有提出也没有回答我的问题,所以我想它不是重复的。

最佳答案

回想一下 ~ P定义为 P -> False .换句话说,为了显示这样的陈述,假设P 就足够了。并得出矛盾。关键是你可以使用P以您喜欢的任何方式作为假设。在普遍量化陈述的特殊情况下,specialize战术可能会派上用场。这种策略允许我们实例化具有特定值的通用量化变量。例如,

Goal ~ forall P Q, P -> Q.
Proof.
intros contra.
specialize (contra True False). (* replace the hypothesis
by [True -> False] *)
apply contra. (* At this point the goal becomes [True] *)
trivial.
Qed.

关于coq - Coq 中的反例证明,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/35726672/

27 4 0
Copyright 2021 - 2024 cfsdn All Rights Reserved 蜀ICP备2022000587号
广告合作:1813099741@qq.com 6ren.com