问题描述
使用 c：
If there are no goals left after running tac1 then tac2 is never run and Coq simply silently succeeds. For instance, in this first derivation we have a useless ; intros at the end of the (valid) proof:
Goal forall (A : Prop), A -> (A /\ A /\ A /\ A /\ A). intros ; repeat split ; assumption ; intros. Qed.
如果我们将其隔离，则会出现错误：没有这样的目标。 ，因为我们试图在没有任何证据证明的情况下采取战术！
If we isolate it, then we get an Error: No such goal. because we are trying to run a tactics when there is nothing to prove!
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 成功，那么就差不多了。
There is exactly one goal left after running tac1.
If there is precisely one goal left after running tac1 then tac1 ; tac2 behaves a bit like tac1. tac2. The main difference is that if tac2 fails then so does the whole of tac1 ; tac2 because the sequence of two tactics is seen as a unit that can either succeed as a whole or fail as a whole. But if tac2 succeeds, then it's pretty much equivalent.
例如以下证明是有效的证明：
E.g. the following proof is a valid one:
Goal forall (A : Prop), A -> (A /\ A /\ A /\ A /\ A). intros. repeat split ; assumption. Qed.
运行 tac1 会产生多个目标。
最后，如果通过运行 tac1 生成了多个目标，则 tac2 应用于所有生成的子目标。在我们的运行示例中，我们可以观察到，如果在重复拆分之后切断战术顺序，那么我们手上就有5个目标。这意味着我们需要复制/粘贴假设五次，以复制先前使用; 给出的证明：
Running tac1 generates more than one goal.
Finally, if multiple goals are generated by running tac1 then tac2 is applied to all of the generated subgoals. In our running example, we can observe that if we cut off the sequence of tactics after repeat split then we have 5 goals on our hands. Which means that we need to copy / paste assumption five times to replicate the proof given earlier using ;:
Goal forall (A : Prop), A -> (A /\ A /\ A /\ A /\ A). intros ; repeat split. assumption. assumption. assumption. assumption. assumption. Qed.
这篇关于分号“;”之间的Coq执行差异和句点“。”的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持！