coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

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 10:08:17 +0000
Accept-language: en-US
Authentication-results: mail3-smtp-sop.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-ME1-obe.outbound.protection.outlook.com
Ironport-phdr: 9a23:8IGgaBdXUkjN57En0Vc9fNY4lGMj4u6mDksu8pMizoh2WeGdxcW6bB7h7PlgxGXEQZ/co6odzbaO4+a4ASQp2tWoiDg6aptCVhsI2409vjcLJ4q7M3D9N+PgdCcgHc5PBxdP9nC/NlVJSo6lPwWB6nK94iQPFRrhKAF7Ovr6GpLIj8Swyuu+54Dfbx9HiTahYr5+Ngm6oRnMvcQKnIVuLbo8xAHUqXVSYeRWwm1oJVOXnxni48q74YBu/SdNtf8/7sBMSar1cbg2QrxeFzQmLns65Nb3uhnZTAuA/WUTX2MLmRdVGQfF7RX6XpDssivms+d2xSeXMdHqQb0yRD+v6bpgRh31hycdLzM38H/ZhNFsjKxVoxyhqR5ww4/Ib4+aO/VzZb/dcsgASGZdQspdSy5MD4WhZIUPFeoBOuNYopH5qVQQtxuxGwysBePywTFGnHD307Y60+MnEQrb2wEuG8wBsG7Ko9XwNKYeS+67w7PGzDXYaPNW3yzw55LOchA8u/2DQ69/cdfLxUY1CgPIl1OdopHrMTOS0+QCqWmb7+x4WOKujW4nsQBxrSK1yscikInEgJ8exFPc9Shhz4s5Oce0RFNnbdOmCpdcqi+XOopsTs8/Xm1luz42x7ICtJKhYSQHzJQqywTCZ/CZb4SE+A/vWeiSLDtginJqZrGyiwq3/EWlzuDxVdK73VlPoyZYnNTDqG0C2hnd6seZSfZx4kKs1SiU2ADd5exJJ10/m7DBJJ472LEwk4IesUTdES/yn0X7lLObeUs59OS09ujre7LoqJCBO4NtjQHxKbohlta4AeQlLggBRG+b+fm61LL+50H5WK9KjvoqkqbHrJ/aOcUbpqm/AwNP1YYj9gq/DzOh0NQfnnkLNk5KeBWCj4TxOlHOJu73DeunjlmjjDtn3e3KMqHjD5nXM3TOnrbscaxg50JBywc/1dVf6IhVCrEFLvLzQEjxtNnAAxE9LQO02fjoCNB9148EV2yAGKGYMLjVsV+O/e8gOe+MZJIPtDnjNvcl+uTigmUkmVMFZ6mmwYMXaGykHvRhO0iWfX3sgs4YHWgWugo+UfflhUaZUT9TYnayR7gz6is6CIKgF4fDR5qijKaP3CehTdVqYTUMAVeVVHzsao+sWvEWaSvULNUr2mgPUqHkQIs83zmvshX7wvxpNLyH1DcfsMfB2cJ44vybuRgt7jtyR5C/3nuASnAysmoXXDgw9Kl5vApwxkrF2LUu0K8QLsBa+/4cClRyDpXb1eEvU4mjCDKERc+ATROdevvjBDgwStwrxNpXORR0HcjkgxzemSO3UeZMy+67Qacs+6eZ5EDfYt5nwi+chqAnkh8rTtYJPHD03vcipTiWPJbAlgCir4jvdakY23KSpk6+9jLX+WR1CUt3W6iDWm0DbEzLq9i//lnFU7KlFbUgNE1G1NKGLaxJLNbuiAcfSQ==

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?

Thanks

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

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