coq - 分号“;”之间的 Coq 执行区别和句号“。”

Question

给定一个使用战术的有效 Coq 证明;，是否有一个通用公式可以将其转换为有效的等效证明，并.替换为;？

许多 Coq 证明使用;或策略排序策略。作为初学者，我想观察各个步骤的执行情况，所以我想替换.，;但令我惊讶的是，我发现这可能会破坏证明。

关于的文档;很少，我还没有找到.任何地方的明确讨论。我确实看到了一篇论文，上面写着非正式的意思t1; t2是

适用于在当前证明上下文中t2由执行产生的每个子目标，t1

我想知道是否.只对当前子目标进行操作并解释不同的行为？但特别想知道是否有通用的解决方案来修复替换.为;.

score 16 · Accepted Answer

的语义tac1 ; tac2是运行tac1，然后运行tac2在由 . 创建的所有子目标上tac1。所以你可能会面临多种情况：

如果运行后没有剩余目标，tac1则tac2永远不会运行，Coq 只是默默地成功。例如，在第一个推导中，我们; intros在（有效）证明的末尾有一个无用的：

Goal forall (A : Prop), A -> (A /\ A /\ A /\ A /\ A).
intros ; repeat split ; assumption ; intros.
Qed.

如果我们隔离它，那么我们会得到一个，Error: No such goal.因为我们正在尝试在没有什么可以证明的情况下运行策略！

Goal forall (A : Prop), A -> (A /\ A /\ A /\ A /\ A).
intros ; repeat split ; assumption.
intros. (* Error! *)

如果跑完后只剩下一个目标，tac1那么tac1 ; tac2行为有点像tac1. tac2. 主要区别在于，如果tac2失败，那么整体也会失败，tac1 ; tac2因为两种策略的顺序被视为一个可以整体成功或整体失败的单元。但如果tac2成功，那么它几乎是等价的。

例如，以下证明是有效的：

Goal forall (A : Prop), A -> (A /\ A /\ A /\ A /\ A).
intros.
repeat split ; assumption.
Qed.

最后，如果通过运行生成多个目标，tac1则将tac2应用于所有生成的子目标。在我们的运行示例中，我们可以观察到，如果我们切断之后的战术序列，repeat split那么我们手上有 5 个进球。这意味着我们需要复制/粘贴assumption五次来复制前面给出的证明;：

Goal forall (A : Prop), A -> (A /\ A /\ A /\ A /\ A).
intros ; repeat split.
 assumption.
 assumption.
 assumption.
 assumption.
 assumption.
Qed.

coq - 分号“;”之间的 Coq 执行区别 和句号“。”