如何解决如何在 Coq 中证明 (~Q -> ~P) - > (P -> Q)
我试图在 coq 中证明 (~Q -> ~P) - > (P -> Q),这是逆反定理 (P-> Q) (~Q -> ~P) 的逆。目前我正在考虑使用相同的逻辑来证明像这样的逆反定理:
不展开。介绍 P Q. 介绍 A B C. 申请 B. 申请 A. 申请 C.
但是我一开始就卡住了。也许我需要额外的公理来证明逆反定理的逆向。有人可以帮我吗?
解决方法
Require Import Classical.
Lemma myproof : forall (P Q : Prop),(~Q -> ~P) -> (P -> Q) .
unfold not. intros P Q. intros A B.
destruct (classic Q) as [Q_holds|NQ_holds].
apply Q_holds.
apply False_ind.
apply A.
apply NQ_holds.
apply B.
Qed.
,
是的,你需要一些额外的能力(经典逻辑)来做到这一点。 放
Require Import Classical.
在文件的开头。
现在当你有一个提议 Q
with
destruct (classic Q) as [Q_holds|NQ_holds].
它创建了两个子目标:一个在 Q
成立时,另一个在 ~Q
成立时。
连同定理 False_ind
(让您证明 False
中的任何内容)应该足以得出您的证明。
版权声明:本文内容由互联网用户自发贡献,该文观点与技术仅代表作者本人。本站仅提供信息存储空间服务,不拥有所有权,不承担相关法律责任。如发现本站有涉嫌侵权/违法违规的内容, 请发送邮件至 dio@foxmail.com 举报,一经查实,本站将立刻删除。