The Coq mailing list

[Jeremy Dawson <Jeremy.Dawson AT anu.edu.au>]

Hi Theo,

What does
split; [> foo1; foo2 ..].
mean?

I find in the documentation that
tac1 ; tac2 means apply tac2 to every subgoal resulting from tac1,
and that
[> tac1 | tac2 | ...] means apply tac1, tac2, etc, one to each of 
several subgoals.

Is [> foo1; foo2 ..] simply a tactic itself, or is
split; [> foo1; foo2 ..] a compound expression with a special meaning?
(If so, I couldn't find it in the documentation)

Anyhow, the question raised by Qinxiang which also puzzles me is 
illustrated in more detail by the following

Variable a: nat.
Variable b: nat.

Ltac foo1 := try reflexivity; try split.
Ltac foo2 := try reflexivity.
Ltac foo3 := foo1 ; foo2.

Goal exists x, (x = a /\ x = a + b) /\ x = b.
eexists.
split; (foo1; foo2). (* sets x to b, why ?? *)
Undo.
split ; foo3. (* sets x to b, why ?? *)
Undo.
split.  1 : foo3. 2 : foo3. Show. (* sets x to a *)
Undo.  Undo.  Undo.
split. all : foo3. (* sets x to b *)
Abort.

Ie, here, it would seem that
split ; foo3.
does the same as
split. all : foo3.
which does the same as
split.  2 : foo3. 1 : foo3.
but is different from
split.  1 : foo3. 2 : foo3.

ie the step
all : foo3.
acts on subgoal 2 before subgoal 1

whereas in a different example

Goal exists x, (x = a) /\ x = b.
eexists.
(split; foo2). (* sets x to a *)
Undo.
split. all : foo2. (* sets x to a *)
Undo.  Undo.
split. 1 : foo2. foo2. (* sets x to a *)
Undo.  Undo.  Undo.
split. 2 : foo2. foo2. (* sets x to b *)
Abort.

split. all : foo2.
acts on subgoal 1 before subgoal 2

This is what I and probably also Qinxiang don't understand.

So the question is what are the semantics of tac1 ; tac2
and of all : tac?

(Thanks Qinxiang for working out this example to illustrate the issue, I 
tried to do so myself but found it highly non-trivial)

Cheers,

Jeremy


On 01/23/2019 10:13 PM, Théo Zimmermann wrote:
> I suppose that you thought that:
> 
> Goal exists c, (c = a /\ c = a + b) /\ c = b.
> eexists.
> split; (foo1; foo2).
> Abort.
> 
> would mean something like:
> 
> Goal exists c, (c = a /\ c = a + b) /\ c = b.
> eexists.
> split; [> foo1; foo2 ..].
> Abort.
> 
> but that is not the case.
> 
> Le mer. 23 janv. 2019 à 12:02, Théo Zimmermann 
> <theo.zimmi AT gmail.com
>  
> <mailto:theo.zimmi AT gmail.com>>
>  a écrit :
> 
>     Why did you think the output should be different? The part of the
>     manual cited by Jeremy precisely says the converse.
> 
>     Le mer. 23 janv. 2019 à 11:49, Cao Qinxiang 
> <caoqinxiang AT gmail.com
>     
> <mailto:caoqinxiang AT gmail.com>>
>  a écrit :
> 
>         This is an interesting question. I try the following script.
> 
>         Variable a: nat.
>         Variable b: nat.
> 
>         Ltac foo1 := try reflexivity; try split.
>         Ltac foo2 := try reflexivity.
> 
>         Goal exists c, (c = a /\ c = a + b) /\ c = b.
>         eexists.
>         split; (foo1; foo2).
>         Abort.
> 
>         Goal exists c, (c = a /\ c = a + b) /\ c = b.
>         eexists.
>         (split; foo1); foo2.
>         Abort.
> 
>         I thought the outcome should be different. But it turns out to
>         be the same. Anyone can explain that?
> 
>         Best,
>         Qinxiang Cao
>         Shanghai Jiao Tong University, John Hopcroft Center
>         Room 1110-2, SJTUSE Building
>         800 Dongchuan Road, Shanghai, China, 200240
> 
> 
> 
>         On Wed, Jan 23, 2019 at 6:19 PM Théo Zimmermann
>         
> <theo.zimmi AT gmail.com
>  
> <mailto:theo.zimmi AT gmail.com>>
>  wrote:
> 
> 
> 
>             Le mer. 23 janv. 2019 à 10:33, Jeremy Dawson
>             
> <Jeremy.Dawson AT anu.edu.au
>  
> <mailto:Jeremy.Dawson AT anu.edu.au>>
>             a écrit :
> 
> 
>                 Hi,
> 
>                 thanks for all the answers to my previous questions,
>                 some of which I'm
>                 still working through.
> 
>                 In https://coq.inria.fr/refman/proof-engine/ltac.html
>                 under Semantics then under Sequence it says
>                 Sequence is associative.
> 
>                 I would take that to mean that
>                 (tac1 ; tac2) ; tac3
>                 is the same as
>                 tac1 ; (tac2 ; tac3)
> 
>                 But is this so?  What if the tactics do some
>                 instantiating of
>                 existential variables, then the order of attacking
>                 subgoals would matter?
> 
> 
>             The order would be the same in both cases.
> 
> 
>                 Also, for the same reason, it would be useful to know, for
>                 tac1 ; tac2
>                 which order tac2 is applied to the subgoals resulting
>                 from tac1
> 
> 
>             This can depend on tactic, but in practice it would be in
>             the listed order of the goals for virtually all tactics.
> 
> 
>                 Cheers,
> 
>                 Jeremy
>