The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

On 07/17/2016 09:45 PM, mukesh tiwari wrote:
> Hi Everyone,
> Pardon me if this is stupid question, but I am trying to understand the
> difference between dot (.) and semicolon (;) in Coq. My understanding is
> that we can interchange the dot and semicolon in Coq file.

It is not true that one can substitute dot for semicolon.  There are 
several reasons:

1.  In the default setting of Coq, with "tac1; tac2", tac2 will be 
applied to all and only the subgoals of tac1.  In "tac1. tac2", tac2 
will be applied to the first goal following the application of tac1, 
which may either be the first subgoal of tac1, or if tac1 solves its 
goal the next goal after tac1.  This behavior can be changed somewhat 
using 'Set Default Goal Selector "all"' - but not completely.

2. in "tac1; tac2", if tac1 has multiple possible successes, then tac2 
may fail on some but not all of them, allowing the combined tactic to 
backtrack and make progress even if tac2 fails initially. In "tac1. 
tac2", if tac2 fails initially then there is no backtracking back to tac1.

I have not tried your example, but I would guess by looking at it that 
there are places where 1 above applies - such as after "case H0" and 
possibly after "apply Not_union".  I doubt that 2 applies at all.

-- Jonathan

>   If you add dot
> after each tactic then you see the intermediate steps/calculation after
> applying the tactic to goal, and if you don't want to see the intermediate
> steps then use semicolon to combine multiple tactics.
>
> Currently I am trying to go though the coq-graph [1] code.
>
>
>     Lemma Union_dec :
>       forall (e1 e2 : U_set) (x : U),
>         {e1 x} + {~ e1 x} -> {e2 x} + {~ e2 x} -> Union e1 e2 x -> {e1 x} +
> {e2 x}.
>     Proof.
>       intros; case H.
>       left; trivial.
>
>       intros; case H0; intros.
>       right; trivial.
>
>       absurd (Union e1 e2 x). apply Not_union; trivial.
>       trivial.
>
>     Qed.
>
> If I replace all the semicolons by dots then It is not provable by
> following the same tactics.
>
> Lemma Union_dec :
>       forall (e1 e2 : U_set) (x : U),
>         {e1 x} + {~ e1 x} -> {e2 x} + {~ e2 x} -> Union e1 e2 x -> {e1 x} +
> {e2 x}.
>     Proof.
>       intros. case H.
>       left. trivial.
>
>       intros. case H0. intros.
>       right. trivial.
>
>       absurd (Union e1 e2 x). apply Not_union. trivial.
>       trivial.
>
> and goal is
>
>    U : Set
>    e1, e2 : U_set
>    x : U
>    H : {e1 x} + {~ e1 x}
>    H0 : {e2 x} + {~ e2 x}
>    H1 : Union e1 e2 x
>    n : ~ e1 x
>    ============================
>     ~ e2 x
>
> subgoal 2 (ID 51) is:
>   Union e1 e2 x
>
>
> Regards,
> Mukesh Tiwari
>
> [1] https://github.com/coq-contribs/graph-basics/blob/master/Sets.v