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

Chr*_*ley 6 coq coq-tactic

鉴于使用;战术的有效Coq证明,是否有通用公式将其转换为有效的等效证明并.替换;

许多Coq证明使用;或战术排序战术.作为一个初学者,我想看的各个步骤执行,所以我想替换.;,但让我吃惊,我觉得这可能会破坏证据.

文档;很稀疏,我没有找到.任何地方的明确讨论.我确实看到了,上面写着非正式的意义t1; t2就是

适用于在当前证据背景下t2执行的每个子目标t1,

我想知道是否.只对当前的子目标进行操作并解释了不同的行为?但是,尤其是我想知道如果有修复由替换破损的通用解决方案.;.

gal*_*ais 13

语义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.
Run Code Online (Sandbox Code Playgroud)

如果我们孤立它,那么我们得到一个Error: No such goal.因为我们正试图在没有什么可证明的时候运行战术!

Goal forall (A : Prop), A -> (A /\ A /\ A /\ A /\ A).
intros ; repeat split ; assumption.
intros. (* Error! *)
Run Code Online (Sandbox Code Playgroud)

跑完后还剩下一个目标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.
Run Code Online (Sandbox Code Playgroud)

跑步会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.
Run Code Online (Sandbox Code Playgroud)