The Coq mailing list

[Théo Zimmermann <theo.zimmi AT gmail.com>]

"all: tac" would be allowed to proceed like this (treat two goals at
once differently from the way it would treat these two subgoals if it
were applied on each one separately). However, most tactics are not
implemented like this. When they are called on multiple goals, they
just "dispatch" on each goal independently, which means that for most
tactics doing:

foo; [> bar .. ]

i.e.:

foo; [> bar | bar | bar ]

with the right number of goals, is the same as doing:

foo; bar

However, because that is not true of all tactics, it cannot in turn be
true of a constructor like ";" which can be used to combine two
tactics to create a new one.

Therefore:

foo; [> bar; foobar .. ]

is not the same as

foo; (bar; foobar)

In the latter case, bar will be applied to all subgoals generated by
foo, and foobar will be applied to all subgoals generated by bar.


Le lun. 28 janv. 2019 à 14:34, Jeremy Dawson
<Jeremy.Dawson AT anu.edu.au>
 a écrit :
>
> OK, so I'm understanding that all:tac is a tactic which does a bit of
> tac on each goal, then a bit more of tac on each goal, and so forth, is
> that correct?
>
> If so then how do I find out or work out what the relevant bits of tac
> are? (eg, if tac is actually repeat tac')
>
> For example, based on what you say I might guess that
> all : repeat tac
> goes back and forth between two goals, applying tac to each (as though
> one instance of tac counted a bit of (repeat tac) - but it seems that is
> not what happens (eg as in my emails in the thread
> Re: [Coq-Club] goal selectors; tactic expressions)
>
> Cheers,
>
> Jeremy
>
> On 01/28/2019 11:53 PM, Pierre Courtieu wrote:
> > Le lun. 28 janv. 2019 à 13:48, Jeremy Dawson
> > <Jeremy.Dawson AT anu.edu.au>
> >   a écrit :
> >> Thanks, but the words GLOBALLY and INDEPENDENTLY are the words used in
> >> the documentation (which, as I said, I don't understand).  What do they
> >> mean?
> > Globally means that a tactic must be seen as a function taking n goals
> > and returning m goals. Hence "all:tac" is ONE tactic that applies to
> > ALL goals at once (even if it does it sequentially).
> >
> > P.
> >