为什么 Coquelicot 会弄乱我的子弹？

Question

假设我在 Coq 中写出以下引理和证明：

Lemma foo : forall A, A -> A.
Proof.
  - simpl.
  - auto.
Qed.

在simpl这里没有做任何事情，这是一个不好的使用要点（-）。当我尝试用 编译它时coqc，我收到以下投诉：

Error: [Focus] Wrong bullet -: Current bullet - is not finished.

我很清楚为什么会发生这个错误。当我打开 的第二个要点时auto，它抱怨我没有完成第一个要点。但是，对我来说没有意义的是这段代码编译得很好：

From Coquelicot Require Import Complex.
Lemma foo : forall A, A -> A.
Proof.
  - simpl.
  - auto.
Qed.

似乎导入 from 的行为Coquelicot使得项目符号点被完全忽略。几个问题：

• 为什么会发生这种情况？这是某种错误吗？
• 有没有办法禁用这种行为？我想使用 Coquelicot 并且仍然要检查正确的项目符号使用情况。

我目前使用的是用 OCaml 4.10.2 和 Coquelicot 3.2.0 编译的 Coq 8.13.2。

Answer 1

Coquelicot 依赖于 MathComp，而 MathComp 禁用了项目符号的传统含义（因为它们的使用方式不同）。但是，它们不是在 MathComp 项目本地执行此操作，而是全局设置一个选项，这就是您获得此行为的原因。

要检索预期的行为，您需要将选项重置为默认值，如下所示：

Set Bullet Behavior "Strict Subproofs".

（参见https://coq.inria.fr/refman/proofs/writing-proofs/proof-mode.html#coq:opt.Bullet-Behavior）