The Coq mailing list

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

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?

Thanks

Jeremy

On 01/28/2019 11:41 PM, Pierre Courtieu wrote:
> Le lun. 28 janv. 2019 à 12:12, Jeremy Dawson
> <Jeremy.Dawson AT anu.edu.au>
>  a écrit :
>>
>> 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).
> 
> After a semi-colon (not followed by brackets []) the "all:" selector
> is implicitly added.
> 
> (1) tac1 produces 2  resulting subgoals, that tac2 is applied GLOBALLY
> on all of them. i.e. as in "tac1. all:tac2.". Note that it is NOT the
> same as tac1; [tac2 | tac2].
> 
> (2) what you say. as explained in the doc: "In this variant, the
> tactic expr is applied INDEPENDENTLY to each of the goals, ....". i.e.
> it is equivalent to tac1; [tac2 | tac2].
> 
> Note that only (1) is associative. (2) isn't. Note also that it has
> not always been like this in coq. This is one of the results of A.
> Spiwak rewriting of the proof engine a few years ago.
> 
> Best
> P
>> And another question, is (prgt 22 ; prgt 33) a tactic?
> 
> it is, but depending on the context they may be applied independently
> or globally.
> 
>> 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).