0

我正在使用 Coq 8.10.0。以下证明脚本似乎在 Mac 中工作（忽略警告）：

Lemma plus_comm : forall (n m : nat), n + m = m + n.
Proof.
  intros.
  - admit.
Qed.

但是 Linux (Ubuntu) 和 Windows 不接受相同的证明脚本。它抛出以下错误：

（在证明 plus_comm 中）：尝试保存放弃目标的证明。如果这确实是您想要做的，请使用 Admitted 代替 Qed。

知道这里发生了什么吗？

PS：我知道理想情况下，承认的证明应该以 Admitted 而不是 Qed/Defined 结尾。我正在尝试调试证明脚本。

4

2 回答 2

2

你确定你在 macOS 和 Windows/Linux 上使用相同的 Coq 版本吗？我不记得究竟是哪个版本引入了行为变化，但现在默认是不允许Qed不完整的证明。

如果您仍想调试证明并需要使用Qed，我建议使用临时公理：

Axiom todo : forall {A}, A.
Tactic Notation "todo" := (exact todo).

现在您可以将todo其用作一种策略而不是，admit它将允许您使用Qed.

于 2020-12-23T09:06:27.030 回答
1

我只是想通这不是因为操作系统。这是因为来自软件基金会的LibTactics ( https://softwarefoundations.cis.upenn.edu/plf-current/LibTactics.html )。如果我们在 Coq 证明脚本中导入了LibTactics，这允许我们将 Qed 放在带有承认的引理的末尾。

于 2020-12-23T09:04:50.547 回答