coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Pierre Courtieu <pierre.courtieu AT gmail.com>
- To: Coq Club <coq-club AT inria.fr>
- Subject: Re: [Coq-Club] [SUSPECTED SPAM] Re: "Sequence is associative." (?)
- Date: Mon, 28 Jan 2019 17:41:30 +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-f179.google.com
- Ironport-phdr: 9a23:Lr9frhcK/83IqGe4nEy3MfYTlGMj4u6mDksu8pMizoh2WeGdxcuyYx7h7PlgxGXEQZ/co6odzbaO4+a4ASQp2tWoiDg6aptCVhsI2409vjcLJ4q7M3D9N+PgdCcgHc5PBxdP9nC/NlVJSo6lPwWB6nK94iQPFRrhKAF7Ovr6GpLIj8Swyuu+54Dfbx9HiTahYr5+Ngm6oRnMvcQKnIVuLbo8xAHUqXVSYeRWwm1oJVOXnxni48q74YBu/SdNtf8/7sBMSar1cbg2QrxeFzQmLns65Nb3uhnZTAuA/WUTX2MLmRdVGQfF7RX6XpDssivms+d2xSeXMdHqQb0yRD+v9LlgRgP2hygbNj456GDXhdJ2jKJHuxKquhhzz5fJbI2JKPZye6XQds4YS2VcRMZcTyNOAo2+YIUPAeQPPvtWoZfhqFUBtha+GRCsCfnzxjNUmnP736s32PkhHwHc2wwgGsoDvm7VrNrrLqcSS/66x7TWwDXEcvNWwyv96InWfRA8vPqBWqpwccvPxkk1DQPKkE+cppDiPzOIzOQNr2mb4PR9Ve+0hG4nrht+ojmrxss2lobJgYcVx0nC+C5kw4g1PcW1RFBnbdOgCpddtCGXO5FrTs4jQmxkojs2x78CtJO9YSME0o4oxwTFZPyCa4WI4gzsVOKWITpggXJqYrO/hxKr/Uih1u3wS9C40FhXoidHltTArH8N1xvU6siITvty4F2t1iqI1wDW8u1EIEY0mrTHK5M53LI8ip4evV7AEyL2gkn6ka6be0Q+9uS16enqZq3qppqGOI91jgH+PL4umsu6AekgKggOXnaU+f6m1LL950H2XLJKjuAskqnFsZDVO9kbq7W2Aw9QyIkj6hK/Ay2639QfmHkLNEhFdw6fj4j1J1HOJ+j1Auu4g1S1iTtk2/TGPqD6DZjWNXjCkLLhfa5n5EJGyQozy8pf55NOBb0bLvLzQBy5iNuNJRggeyew3uyvXN56z8YVXX+FKq6fKqLb91GSsLEBOe6JMbcUtSznJrAO4OP0kX40hBdJZaikx4EaLnu/A+56IkiESXXpi9YFV2wNu1xtH6TRlFSeXGsLND6JVKUm62R+Udr+VNaRdsWWmLWEmRyDMNhTb2FCBEqLFC6xJYqBUvYILimVJ504y2BWZf2aU4YkkCqWmkri0bM+d7jb/yQZsdTo090nv7SOxyF3ziR9CoGm60/IT2xwmTlWFTo/3aQ6oFAkj1najvk+jPtfGtheofhOV1ViOA==
Le lun. 28 janv. 2019 à 14:33, Jeremy Dawson
<Jeremy.Dawson AT anu.edu.au>
a écrit :
>
> OK, so I'm understanding that all:tac is a tactic which does a bit of
> tac on each goal, then a bit more of tac on each goal, and so forth, is
> that correct?
That is not how I see things. all:tac. applies the tac to all goals.
Period. Just don't consider ";" as a way to combine "single goal"
tactics.
> If so then how do I find out or work out what the relevant bits of tac
> are? (eg, if tac is actually repeat tac')
Indeed the status of repeat is strange, but conforms to the documentation:
doc says:
"repeat expr: expr is evaluated to v. If v denotes a tactic, this
tactic is applied to each focused goal *independently*."
so yes repeat is not a multigoal tactical. Which is strange.
Ltac prg a := let t := type of a in idtac t;(intro + now auto).
Goal (forall a b c d e f:bool, False) /\ (forall a y z t u v:nat, False).
Proof.
split;intro.
prg a; prg a ; prg a ; prg a ; prg a. (* nat boobl nat bool ...*)
Undo.
do 5 (prg a). (* same *)
Undo.
do 2 (prg a;prg a). (* same *)
Undo.
repeat ltac:(prg a). (* nat nat ... bool bool ...*)
Undo.
[> prg a; [> prg a ; [> prg a ; [> prg a ; [> prg a .. ].. ].. ].. ]
.. ]. (* same *)
It is indeed strnage that repeat is no a multigoal tactical whereas "do" is.
Is it possible to define multigoal tactics in ltac?
Pierre
- Re: [Coq-Club] "Sequence is associative." (?), (continued)
- Re: [Coq-Club] "Sequence is associative." (?), Jeremy Dawson, 01/28/2019
- Re: [Coq-Club] "Sequence is associative." (?), Pierre Courtieu, 01/28/2019
- Re: [Coq-Club] "Sequence is associative." (?), Jeremy Dawson, 01/28/2019
- Re: [Coq-Club] "Sequence is associative." (?), Pierre Courtieu, 01/28/2019
- Re: [Coq-Club] "Sequence is associative." (?), Jeremy Dawson, 01/28/2019
- Re: [Coq-Club] "Sequence is associative." (?), Pierre Courtieu, 01/28/2019
- Re: [Coq-Club] "Sequence is associative." (?), Jeremy Dawson, 01/28/2019
- Re: [Coq-Club] "Sequence is associative." (?), Pierre Courtieu, 01/28/2019
- Re: [Coq-Club] "Sequence is associative." (?), Jeremy Dawson, 01/28/2019
- Re: [Coq-Club] [SUSPECTED SPAM] Re: "Sequence is associative." (?), COURTIEU Pierre, 01/28/2019
- Re: [Coq-Club] [SUSPECTED SPAM] Re: "Sequence is associative." (?), Pierre Courtieu, 01/28/2019
- Re: [Coq-Club] [SUSPECTED SPAM] Re: "Sequence is associative." (?), Jeremy Dawson, 01/31/2019
- Re: [Coq-Club] "Sequence is associative." (?), Théo Zimmermann, 01/28/2019
- Re: [Coq-Club] "Sequence is associative." (?), Jeremy Dawson, 01/28/2019
- Re: [Coq-Club] "Sequence is associative." (?), Pierre Courtieu, 01/28/2019
- Re: [Coq-Club] "Sequence is associative." (?), Jeremy Dawson, 01/28/2019
- Re: [Coq-Club] "Sequence is associative." (?), Pierre Courtieu, 01/28/2019
- Re: [Coq-Club] "Sequence is associative." (?), Jeremy Dawson, 01/28/2019
Archive powered by MHonArc 2.6.18.