Coq中分号“;”和句点“.”之间的执行区别

Question

给定一个使用“;”策略的有效Coq证明，是否存在一般公式可以将其转换为使用“.”替代“;”的有效等价证明？

许多Coq证明使用“;”或策略序列策略。作为初学者，我想观察每个步骤的执行情况，因此我想用“.”替换“;”，但令我惊讶的是，这可能会破坏证明。

关于“;”的文档很少，我没有在任何地方找到关于“.”的明确讨论。我看到了一篇paper，其中说“t1; t2”的非正式含义是

应用“t2”到当前证明上下文中由“t1”执行产生的每个子目标，

我想知道“.”是否只对当前子目标起作用，这解释了不同的行为方式？但我特别想知道是否有一般解决方案来修复由于将“.”替换为“;”而导致的破坏。

- Christopher Brinkley

Answer 1

tac1 ; tac2 的语义是先运行 tac1，然后在 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 会生成多个目标。

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

- gallais

---

谢谢您的案例分解！这非常有帮助。 - Christopher Brinkley

@ChristopherBrinkley 如果这篇帖子回答了你的问题，如果你将其标记为“答案”，那就太好了。 - Anton Trunov

我要指出的是，除了在每个分支中应用该策略之外，最重要的区别可能是Coq将通过“;”回溯。例如，即使tac1只生成一个目标，如果有多种方法可以实现它（一个重要的例子是constructor），那么tac1.tac2将承诺第一个成功并在其上运行tac2。tac1; tac2将使tac1尝试一件事情，然后在此之后尝试tac2，如果失败，则尝试以另一种方式尝试tac1，然后在此之后尝试tac2，如果失败，则尝试以另一种方式尝试tac1，依此类推。 - HTNW