The Coq mailing list

[Pierre Courtieu <pierre.courtieu AT gmail.com>]

Le lun. 28 janv. 2019 à 11:08, Jeremy Dawson
<Jeremy.Dawson AT anu.edu.au>
 a écrit :
>
> Thanks, but in fact it works the opposite of what I would have expected,
> just as
> split ; (prgt 22 ; prgt 33).
> does.
>
> As I said, I'm trying to understand what these constructions do.
>
> Why do you expect your macro to work as it does?

Sorry I did not understand your question. I think you should consider that

Set Default Selected Goal "all".

is the "natural" (understand: monadic) mode of ltac.

Set Default Goal Selector "all".
Variable P : Prop.
Variable Q : Prop.
Goal P /\ Q.
split.
prgt 22.
prgt 33.

In this mode doing "t;u." is like doing "t. u.".
If you want a "depth first" aplication of tactics you need to do:

split; [> prgt 22; prgt 33 .. ].

https://coq.inria.fr/distrib/current/refman/proof-engine/ltac.html#local-application-of-tactics

Hope this helps,
Pierre

>
> Jeremy
>
>
> On 01/28/2019 08:29 PM, Pierre Courtieu wrote:
> > Hi,
> > I guess Ltac functions are not macros, they define new tactics
> > considered as one single step by tacticals.
> >
> > If you define a macro:
> >
> > Tactic Notation "prgt3" int(t1) int(t2) :=  prgt t1 ; prgt t2.
> >
> > then it works as expected.
> >
> > P.
> >
> > Le lun. 28 janv. 2019 à 09:40, Jeremy Dawson
> > <Jeremy.Dawson AT anu.edu.au>
> >  a écrit :
> >>
> >> Yes, it seems that this is the case in the example below.  I'm trying to
> >> understand why.
> >>
> >> In the example below I would have expected that
> >> split ; (prgt 22 ; prgt 33).
> >> and
> >> split ; (prgt2 22 33).
> >> would have the same result, but they don't.
> >>
> >> Why is this?
> >>
> >> Thanks
> >>
> >> Jeremy
> >>
> >> On 01/23/2019 09:18 PM, Théo Zimmermann wrote:
> >>>
> >>>      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?
> >>>
> >>>
> >>> The order would be the same in both cases.
> >>
> >> Yes, it seems that this is the case in the example below.  I'm trying to
> >> understand why.
> >>
> >> In the example below I would have expected that
> >> split ; (prgt 22 ; prgt 33).
> >> and
> >> split ; (prgt2 22 33).
> >> would have the same result, but they don't.
> >>
> >> Why is this?
> >>
> >> Thanks
> >>
> >> Jeremy
> >>
> >> Ltac prgt t :=
> >>     match goal with
> >>       | [ |- ?P ] => idtac t P
> >>       end.
> >>
> >> Ltac prgt2 t1 t2 := prgt t1 ; prgt t2.
> >>
> >> Variable P : Prop.
> >> Variable Q : Prop.
> >> Goal P /\ Q.
> >>
> >> (split ; prgt 22) ; prgt 33.
> >> Undo.
> >> split ; (prgt 22 ; prgt 33).
> >> Undo.
> >> split ; (prgt2 22 33).