9

给定一个使用战术的有效 Coq 证明;,是否有一个通用公式可以将其转换为有效的等效证明,并.替换为;

许多 Coq 证明使用;或 策略 排序 策略。作为初学者,我想观察各个步骤的执行情况,所以我想替换.;但令我惊讶的是,我发现这可能会破坏证明。

关于的文档;很少,我还没有找到.任何地方的明确讨论。我确实看到了一篇论文,上面写着非正式的意思t1; t2

适用于在当前证明上下文中t2由执行产生的每个子目标,t1

我想知道是否.只对当前子目标进行操作并解释不同的行为?但特别想知道是否有通用的解决方案来修复替换.;.

4

1 回答 1

16

的语义tac1 ; tac2是运行tac1,然后运行tac2在由 . 创建的所有子目标上tac1。所以你可能会面临多种情况:

跑完就没有目标了tac1

如果运行后没有剩余目标,tac1tac2永远不会运行,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.
于 2016-03-29T22:17:19.870 回答