给定一个使用 ; 策略的有效 Coq 证明，是否有一个通用公式可以将其转换为有效的等价证明，用 . 代替 ;？
许多 Coq 证明使用; 或战术序列战术。作为一个初学者，我想观察各个步骤的执行情况，所以我想用. 代替;，但令我惊讶的是，我发现这可能会破坏证明。
; 上的文档很少，而且我在任何地方都没有找到关于 . 的明确讨论。我确实看到了一个paper，上面写着t1; t2 的非正式含义是
将
t2应用于在当前证明上下文中执行t1产生的每个子目标，
我想知道. 是否只对当前子目标起作用并且这解释了不同的行为？但是特别想知道是否有通用的解决方案来修复用.替换;造成的破损。
【问题讨论】：
标签： coq coq-tactic
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 之后只剩下一个目标，那么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 5 次才能复制前面使用; 给出的证明：
Goal forall (A : Prop), A -> (A /\ A /\ A /\ A /\ A).
intros ; repeat split.
assumption.
assumption.
assumption.
assumption.
assumption.
Qed.
【讨论】：
;。例如。即使tac1 只产生一个目标，如果它有多种方法可以做到这一点（一个重要的例子是constructor），那么tac1. tac2 将承诺第一次成功并在其上运行tac2。 tac1; tac2 会让tac1 尝试一件事，然后尝试tac2，如果失败，请尝试tac1 另一种方式，然后尝试tac2，如果失败，请尝试tac1 另一种另一种方式，等等。