Coq execution difference between semicolon ";" and the period "."

Question

Given the valid evidence of Coq using a tactical method ; whether there is a general formula for its transformation into a valid equivalent proof with a replacement . on ; ?

Many Coq evidence uses tactics ; or tactical sequence. As a beginner, I want to see how the individual steps are performed, so I want to replace . on ; but, to my surprise, I discovered that this could violate the evidence.

Documentation on ; sparse, and I did not find an explicit discussion . wherever. I saw a paper that says the unofficial meaning of t1; t2 t1; t2 -

apply t2 to each subgoal created by executing t1 in the current verification context,

and I wonder if it works . on the current subgoal and what explains the other behavior? But I especially want to know if there is a general solution to fix the breakdown caused by the replacement . on ; .

Answer 1

Semantics of tac1 ; tac2 tac1 ; tac2 must start tac1 , and then run tac2 in all the subgoals created by tac1 . Thus, you may encounter many cases:

After starting tac1

no goals.

If, after starting tac1 there are no targets, then tac2 never starts, and Coq simply succeeds in silence. For example, in this first conclusion we have useless ; intros ; intros at the end of (valid) evidence:

 Goal forall (A : Prop), A -> (A /\ A /\ A /\ A /\ A). intros ; repeat split ; assumption ; intros. Qed. 

If we isolate it, we get Error: No such goal. because we are trying to launch a tactic when there is nothing to prove!

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

After starting tac1 , exactly one goal remains.

If after running tac1 exactly one goal remains, then tac1 ; tac2 tac1 ; tac2 behaves a bit like tac1. tac2 tac1. tac2 . The main difference is that if tac2 fails, then all tac1 ; tac2 tac1 ; tac2 , since the sequence of two tactics is considered as a unit that can either succeed as a whole or not work at all. But if tac2 succeeds, then this is pretty much equivalent.

eg. The following proof is valid:

 Goal forall (A : Prop), A -> (A /\ A /\ A /\ A /\ A). intros. repeat split ; assumption. Qed. 

Running tac1 creates more than one goal.

Finally, if several targets are created when tac1 started, then tac2 is applied to all generated subgoals. In our example, we can notice that if we cut off the sequence of tactics after repeat split , then we have 5 goals in our hands. This means that we need to copy / paste the assumption five times in order to reproduce the evidence obtained earlier using ; :

 Goal forall (A : Prop), A -> (A /\ A /\ A /\ A /\ A). intros ; repeat split. assumption. assumption. assumption. assumption. assumption. Qed.