假设我在 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.
似乎是从Coquelicot
进口的行为使得项目符号点被完全忽略。几个问题:我目前使用的是用 OCaml 4.10.2 和 Coquelicot 3.2.0 编译的 Coq 8.13.2。
最佳答案
Coquelicot 依赖于 MathComp,而 MathComp 禁用了项目符号的传统含义(因为它们的使用方式不同)。但是,它们不是在 MathComp 项目本地执行此操作,而是全局设置一个选项,这就是您获得此行为的原因。
要检索预期的行为,您需要将选项重置为默认值,如下所示:
Set Bullet Behavior "Strict Subproofs".
(参见 https://coq.inria.fr/refman/proofs/writing-proofs/proof-mode.html#coq:opt.Bullet-Behavior)
关于coq - 为什么 Coquelicot 会弄乱我的子弹?,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/68408859/