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: Pierre Courtieu <pierre.courtieu AT gmail.com>
  • To: Coq Club <coq-club AT inria.fr>
  • Subject: Re: [Coq-Club] "Sequence is associative." (?)
  • Date: Mon, 28 Jan 2019 11:25:25 +0100
  • Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=pierre.courtieu AT gmail.com; spf=Pass smtp.mailfrom=pierre.courtieu AT gmail.com; spf=None smtp.helo=postmaster AT mail-it1-f169.google.com
  • Ironport-phdr: 9a23:tUS6RxDPHRvnWtRa23mEUyQJP3N1i/DPJgcQr6AfoPdwSPT5psbcNUDSrc9gkEXOFd2Cra4c26yO6+jJYi8p2d65qncMcZhBBVcuqP49uEgeOvODElDxN/XwbiY3T4xoXV5h+GynYwAOQJ6tL1LdrWev4jEMBx7xKRR6JvjvGo7Vks+7y/2+94fcbglUhzexe69+IAmrpgjNq8cahpdvJLwswRXTuHtIfOpWxWJsJV2Nmhv3+9m98p1+/SlOovwt78FPX7n0cKQ+VrxYES8pM3sp683xtBnMVhWA630BWWgLiBVIAgzF7BbnXpfttybxq+Rw1DWGMcDwULs5Qiqp4bt1RxD0iScHLz85/3/Risxsl6JQvRatqwViz4LIfI2ZMfxzdb7fc9wHX2pMRsleVyJDDY28YYUBDPcPM/hEoIfyvFYOsQK+CBOwCO/z1jNFhHn71rA63eQ7FgHG2RQtEcgPsHvKttX1LrkdWv2rwanP0DXDde9W2Tbj54jVbxsspumMXbNufsrL00kgCRnJgUmXqYz4JTOVyuUNvHaG7+d7WuKvjnQoqwB1ojS12sgsjYzJi5sTx1vZ+yt5x4M1Kse5SE59edOkEZ1QtzubN4RsWM8iTXtotSAnwbMFoZ62ZDYGxIgjyhLFaPGKc5KE7g/iWeuQOzt0mXNodba5ih2v60av0Pf8WdOx0FtSripKjN3MtncV2hzW8MeHS/998l6g2TaTygzf8+9ELV01mKffMZIhzbkwlp0csUTHACD6gln5jKiTdkk8++io7froYqn+q5OCK4N5jhvyP6cul8ClHOg1MwkDU3KG9em90LDv5Uj5T69Ljv0ynKnZqpfaJcEDq66hAg9azJwj6wyhADu8zNsYmmQHLEhZeBKGkYfpJkrDIP/9DfilglSslC1nyOzBPr3kGpnNNGTMkK/9fbZh7E5R0BY8zddG555NFr4BJO/zVVTqudzDDh45NhS0zPz9BNV80IMeQ2OPDbWDPKPcq1/brt4odsKLfcc+vCv3Y6wu4Oerhnskk3cce7Oo1N0ZcibrMO5hJhChYHf2mNpJOmAXpBY/QfGi3EWDXCRJajC5WL8m+jA2FaqpCI7CQsamh7nXj3TzJYFfem0TUgPEKnzvbYjRHq5UMHvDcP8kqSQNUP2ac6Fk0BivsAHgzL8+d7jb/yQZsdTo090nvrSPxyF3ziR9CoGm60/IV3t9xzpaSDo/3aQ5qkt4mA/ajPpIxsdAHNkW3MtnFwc3MZmGkb5/AtH2HwPdJ5KHEQj3BNqhBj41Q5Q6xNpcO0s=

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