The Coq mailing list

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

Thanks but I don't understand what you are saying about

Set Default Selected Goal "all". and
the "natural" (understand: monadic) mode of ltac.

Could I ask
(1) what does tac1 ; tac2 do, where tac1 and tac2 are tactics?
(2) what does tac1 ; [> tac2 ..] do, where tac1 and tac2 are tactics?

For example, the answer to one of these questions might be, where, for 
example, tac1 produces 2 resulting subgoals, that tac2 is then applied 
to the first of those subgoals, then to the second (or vice versa).  And 
the answer to the other question I expect should be something different.

And yes, I've read what seems to be the relevant bit of the 
documentation several times, and I don't understand what it is saying.

And another question, is (prgt 22 ; prgt 33) a tactic?

Thanks,

Jeremy

On 01/28/2019 09:25 PM, Pierre Courtieu wrote:
> 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).