为什么 Coq 不允许在 Linux 和 Windows 中以 QED 结尾的定理？

Question

我正在使用 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): Attempt to save a proof with given up goals. If this is really what you want to do, use Admitted in place of Qed.

知道这里发生了什么吗？

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

Answer 1

我才发现不是操作系统的问题。这是因为 LibTactics 来自 Software Foundations (https://softwarefoundations.cis.upenn.edu/plf-current/LibTactics.html)。如果我们在 Coq 证明脚本中导入了 LibTactics，那么我们就可以将 Qed 放在带有 admits 的引理末尾。

Answer 2

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

如果你仍然想调试一个证明并且需要使用Qed，我建议使用一个临时公理：

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

现在你可以使用 todo 作为战术而不是 admit 并且它允许你使用 Qed.

为什么 Coq 不允许在 Linux 和 Windows 中以 QED 结尾的定理？

Why Coq doesn't allow a theorem with admits to end with QED in Linux and Windows?

coq

coqide

gallina