The Coq mailing list

[COURTIEU Pierre <pierre.courtieu AT lecnam.net>]

Le lun. 28 janv. 2019 à 14:33, 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?

That is not how I see things. all:tac. applies the tac to all goals.
Period. Just don't consider ";" as a way to combine "single goal"
tactics.


> 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')

Indeed the status of repeat is strange, but conforms to the documentation:

doc says:
"repeat expr:    expr is evaluated to v. If v denotes a tactic, this
tactic is applied to each focused goal *independently*."

so "all:repeat tac" is equivalent to "all:[>tac ; [> tac ; etc ..]
..]", and NOT to "all:tac;tac;..."
See this example:

Ltac prg a := let t := type of a in idtac t;(intro + now auto).

Goal (forall a b c d e f:bool, False)/\(forall a y z t u v:nat, False).
Proof.
  split;intro.
  all:repeat (let t := type of a in idtac t;(intro+now auto)).
  Undo.
  (* equivalently*)
  all: [> prg a; [> prg a ; [> prg a ; [> prg a ; [> prg a .. ].. ]..
].. ] ..  ].

On one hand I think things behave the way they are described in the
documentation.

On the orher hand I tried to define a repeat2 tactical in ltac that
would apply things like an iteration of ";" but I did not succeed. If
someone knows how to do that I would be interested.

Hope this helps,
Pierre



> 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.
> >