Coq 分号 ";"和句点 "."之间的执行差异

Question

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

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

关于 ; 的文档很少，而且我还没有在任何地方找到对 . 的明确讨论。我确实看到了paper这表示 t1 的非正式含义； t2 是

apply t2 to every subgoal produced by the execution of t1 in the current proof context,

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

造成的损坏。

Answer 1

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

运行后没有目标 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然后tac1 ; tac2行为有点像 tac1. tac2 。主要区别在于如果 tac2那么整个 tac1 ; tac2 都会失败因为两种策略的序列被视为一个整体，要么整体成功，要么整体失败。但如果tac2成功了，那么它几乎是等价的。

例如以下证明是有效的:

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

正在运行 tac1产生多个目标。

最后，如果运行 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.