分号“;”之间的Coq执行差异和句点“。” [英] Coq execution difference between semicolon ";" and period "."

问题描述

使用给出有效的Coq证明； 战术，是否存在使用将其转换为有效的等效证明的通用公式。代替; ？

Given a valid Coq proof using the ; tactical, is there a general formula for converting it to a valid equivalent proof with . substituted for ;?

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

Many Coq proofs use the ; or tactic sequencing tactical. As a beginner, I want to watch the individual steps execute, so I want to substitute . for ;, but to my surprise I find that this may break the proof.

上的文档； 很少，我还没有找到对的明确讨论。随处可见。我确实看到了纸张表示<$的非正式含义c $ c> t1; t2 是

Documentation on ; is sparse, and I haven't found an explicit discussion of . anywhere. I did see a paper that says informal meaning of t1; t2 is

将 t2 应用于每个产生的子目标通过在当前证明上下文中执行 t1 ，

apply t2 to every subgoal produced by the execution of t1 in the current proof context,

如果。仅在当前子目标上运行，这说明了不同的行为吗？但是尤其是我想知道是否有一种通用的解决方法来修复由。替换为; 造成的损坏。 / p>

and I wonder if . only operates on the current subgoal and that explains the different behavior? But especially I want to know if there is a general solution to repairing the breakage caused by substituting . for ;.

推荐答案

tac1的语义； tac2 将在 all tac1 ，然后运行 tac2 > tac1 创建的子目标。因此，您可能会遇到各种情况：

The semantics of tac1 ; tac2 is to run tac1 and then run tac2 on all the subgoals created by tac1. So you may face a variety of cases:

如果运行 tac1 后没有目标，则永远不会运行 tac2 而Coq只是默默地成功了。例如，在第一个推导中，我们有一个无用的; （有效）证明结尾处的简介 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执行差异和句点“。”的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！