的语义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.