Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] "Sequence is associative." (?)

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] "Sequence is associative." (?)


Chronological Thread 
  • From: Jeremy Dawson <Jeremy.Dawson AT anu.edu.au>
  • To: "coq-club AT inria.fr" <coq-club AT inria.fr>
  • Subject: Re: [Coq-Club] "Sequence is associative." (?)
  • Date: Mon, 28 Jan 2019 12:48:02 +0000
  • Accept-language: en-US
  • Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=Jeremy.Dawson AT anu.edu.au; spf=Pass smtp.mailfrom=Jeremy.Dawson AT anu.edu.au; spf=Pass smtp.helo=postmaster AT AUS01-SY3-obe.outbound.protection.outlook.com
  • Ironport-phdr: 9a23:wftxLR0/xQl/0gsvsmDT+DRfVm0co7zxezQtwd8ZseMWIvad9pjvdHbS+e9qxAeQG9mDu7Qc06L/iOPJYSQ4+5GPsXQPItRndiQuroEopTEmG9OPEkbhLfTnPGQQFcVGU0J5rTngaRAGUMnxaEfPrXKs8DUcBgvwNRZvJuTyB4Xek9m72/q99pHPYAhEniaxba9vJxiqsAvdsdUbj5F/Iagr0BvJpXVIe+VSxWx2IF+Yggjx6MSt8pN96ipco/0u+dJOXqX8ZKQ4UKdXDC86PGAv5c3krgfMQA2S7XYBSGoWkx5IAw/Y7BHmW5r6ryX3uvZh1CScIMb7S60/Vza/4KdxUBLmiDkJOSMl8G/ZicJwgqBUoBO9qBJwzIHZe52VO+Fkc6/BYd8WWWhMU8BMXCJBGIO8aI4PAvIFM+lGtYnyuV4OrBujDgeiHuzuxCRIhnjw3aYn1OkvFR/J3BY+ENILsHXYttv7O70cUOCuy6nIyy7OYOlQ2Tfg8oTHbA0uoeyWUb1qbMrc0E8iHB7LgFWXrIzqJTKV1uIVvmia6epgT+OvhHQ9pwF/uDiiwNonhIrRho8NxV3I6T91zJspKdC6UkJ3fNCpHZlKuy2HKYd7QNsuTm5stSog17ELvZ62cDIXxJg52xLTceGLfoaL7x77WuaePzR1iG5gdb+6gxu/8lOvx+L5W8Wp3ltFsDdKn9zCtn8T1BHf9s2KRuVm8Uev1juC0R3Y5PteLkAuj6XbLoYswr4umZoXtkTOBjP7l0vrgqOKa0ko4/Wm5Obpb7n/oZ+TLJF7hhv5MqQzhsywGuM4MhUIX2eG4+i8zKfj/UrlQLpUkvI2jqjZsJfcJcgBoa65HhNV0oIk6xa4DDeqysgXnX4CLF5deRKHiZbmO03WLf33EfuzmUmgnCtpyvzcI7HsDJfAImLenLv/f7tx80tcxxAyzdBb6ZJUELYBIPfrV0H1qtPYFAE2Mwm0wur9BttyzI0fWXmIAq+fK67dq1mI5v81L+aSeYAVpSzxJOI45/L2l382hUcdfbW13ZsQcH23AvNmI1yAbXXwhtcBDHwFsxElTO3qjV2CSSRca2yzX6I6/DE7CZipAZ3NRoC30/S923LxFZpPI2tCF1qkEHHydozCVe1GIHaZJdYkmTgZX5CgTZUg3Fegrlmp5aBgK7/29zcVsIOr+NFq/OrV3UUQ+CZ5CtXb/2iSVGZytmoOWnk70L05qFErmQTL6rRxn/ENTY8b3PhOSApvbceNndw/MMj7X0f6RvnMTV+nRtu8BjRoFIA4xcJIbkpgXdy/3Emag3iaRoQNnrnOP6Qat7rG1iGrdc971jDL2LRnhkR0GpISZ13jvbZ28k3oP6CMk0idkPr1J40h53aUsVyyli+JtkweVxNsW6LYW3xZflHRsdny+kLFSfmpFKgjNQxCj8WFL/kTZw==

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



Archive powered by MHonArc 2.6.18.

Top of Page