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 13:53:55 +0100
  • Authentication-results: mail2-smtp-roc.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-f178.google.com
  • Ironport-phdr: 9a23:ezMw5BSOMZZdtdwfWdxwAzYdntpsv+yvbD5Q0YIujvd0So/mwa6yZhWN2/xhgRfzUJnB7Loc0qyK6/CmATRIyK3CmUhKSIZLWR4BhJdetC0bK+nBN3fGKuX3ZTcxBsVIWQwt1Xi6NU9IBJS2PAWK8TW94jEIBxrwKxd+KPjrFY7OlcS30P2594HObwlSizexfbB/IA+qoQnNq8IbnZZsJqEtxxXTv3BGYf5WxWRmJVKSmxbz+MK994N9/ipTpvws6ddOXb31cKokQ7NYCi8mM30u683wqRbDVwqP6WACXWgQjxFFHhLK7BD+Xpf2ryv6qu9w0zSUMMHqUbw5Xymp4rx1QxH0ligIKz858HnWisNuiqJbvAmhrAF7z4LNfY2ZKOZycqbbcNgHR2ROQ9xRWjRODYOybYQBD+QPM+VFoYfju1QAogCzBRW1BO711jNEmmP60K883u88EQ/GxgsgH9cWvXrOrdX6Kr0SUfqrw6LV0zjDaO5W2S3h6IjJbB8hvOyHULVoccrQ10YvDRnFgUuKpYP5ODOVy/4Ns3Sa7+V+SOKikGEnqwRrrTiuwscgkJXGhoUQyl3d8yhy3Yg7Jdq9SEFhYN6kFoNdtyCcN4tsQ8MtWXtkuCggyrAApJW1fzAKxYw5yxLDb/GLaYuF7xL5WOqMIDp1hWhpdK+9ihux90Wr1/fyWdOu0FlQqypIitnMuW4J1xzU8sWHT+Fy/kal2TqW1gDT9vxILVk6labGKZMswaQ8lpUUsUTEES/2nFv5gLWKeUUj/+ik8+XnYrP4qZ+AL4J4lB3yP6A0lsG8Aek0KBUCUmma9OimybHu/070TK1PjvIsk6nZtJ7aJd4cpq68GwJVyocj5AilDze8ztsUh2UILFVYeBKdk4jpOk/BIO3jAPewhlSjijZrx/TcMrL9BZXNK2DPkK39crZl905c1A0zwMhD6JJTE7ENOe78WkvstNPDFRI5KAy1w+P/CNpnzI8eWGSPArWYMKzIq1OI6PgvcKGwY9o+vy+1APw47ba6hngg3FQZYKOB3J0NaXn+EO4wcGuDZn+5utYMC30H9iE5Ufb2iVCfGWpLZnuoRa967TYmEp6nAJrrSYWkgbjH1yC+SM4FLltaA0yBRC+7P76PXO0BPWfLepc4w240EIO5Qopk7imA8Qrzyr5pNO3Ro3RKupfq1dwz7OrWx0hrqW5ESv+F2mTIdFla23sSTmZvjq96qE15jFyE1Pog2qEKJZlo//pMFzwCG9vcwuh9UY6gXwvAepKIVA/jTIz5UXc+SdU+x9JIaEF4SY2v

Le lun. 28 janv. 2019 à 13:48, Jeremy Dawson
<Jeremy.Dawson AT anu.edu.au>
a écrit :
>
> 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?

Globally means that a tactic must be seen as a function taking n goals
and returning m goals. Hence "all:tac" is ONE tactic that applies to
ALL goals at once (even if it does it sequentially).

P.

> 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