如何解决为什么 Coq 不允许在 Linux 和 Windows 中以 QED 结尾的定理?
我使用的是 Coq 8.10.0。以下证明脚本似乎适用于 Mac(忽略警告):
Lemma plus_comm : forall (n m : nat),n + m = m + n.
Proof.
intros.
- admit.
Qed.
但是在 Linux (Ubuntu) 和 Windows 中不接受相同的证明脚本。它抛出以下错误:
(in proof plus_comm):尝试保存已放弃目标的证明。如果 这确实是您想要做的,使用 Admitted 代替 Qed。
知道这里发生了什么吗?
PS:我知道理想情况下,带有录取的证明应该以 Admitted 而不是 Qed/Defined 结尾。我正在尝试调试证明脚本。
解决方法
您确定在 macOS 和 Windows/Linux 上使用相同的 Coq 版本吗?我不记得确切是哪个版本引入了行为变化,但现在默认情况下是在不完整的证明上禁止 Qed
。
如果您仍想调试证明并需要使用 Qed
,我建议您使用临时公理:
Axiom todo : forall {A},A.
Tactic Notation "todo" := (exact todo).
现在您可以使用 todo
作为策略而不是 admit
,它将允许您使用 Qed
。
我才发现不是操作系统的原因。这是因为来自 Software Foundations (https://softwarefoundations.cis.upenn.edu/plf-current/LibTactics.html) 的 LibTactics。如果我们在 Coq 证明脚本中导入了 LibTactics,那么我们就可以将 Qed 放在带承认的引理的末尾。
版权声明:本文内容由互联网用户自发贡献,该文观点与技术仅代表作者本人。本站仅提供信息存储空间服务,不拥有所有权,不承担相关法律责任。如发现本站有涉嫌侵权/违法违规的内容, 请发送邮件至 dio@foxmail.com 举报,一经查实,本站将立刻删除。