coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: COURTIEU Pierre <pierre.courtieu AT lecnam.net>
- To: Coq Club <coq-club AT inria.fr>
- Subject: Re: [Coq-Club] [SUSPECTED SPAM] Re: "Sequence is associative." (?)
- Date: Mon, 28 Jan 2019 16:15:15 +0000
- Accept-language: fr-FR, en-US
- Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=pierre.courtieu AT lecnam.net; spf=Pass smtp.mailfrom=pierre.courtieu AT lecnam.net; spf=Pass smtp.helo=postmaster AT EUR04-VI1-obe.outbound.protection.outlook.com
- Ironport-phdr: 9a23:B9LXOB9GI6DKZP9uRHKM819IXTAuvvDOBiVQ1KB20ugcTK2v8tzYMVDF4r011RmVBdWds6oMotGVmpioYXYH75eFvSJKW713fDhBt/8rmRc9CtWOE0zxIa2iRSU7GMNfSA0tpCnjYgBaF8nkelLdvGC54yIMFRXjLwp1Ifn+FpLPg8it2O2+557ebx9UiDahfLh/MAi4oQLNu8cMnIBsMLwxyhzHontJf+RZ22ZlLk+Nkhj/+8m94odt/zxftPw9+cFAV776f7kjQrxDEDsmKWE169b1uhTFUACC+2ETUmQSkhpPHgjF8BT3VYr/vyfmquZw3jSRMNboRr4oRzut86ZrSAfpiCgZMT457HrXgdF0gK5CvR6tuwBzz4vSbYqINvRxY7ndcMsaS2RfQ8hRSyJPDICyb4QNDuoOIelWoIbmqlsSthSzHxWgCP/zxjJKgHL9wK000/4mEQHDxAEtAcsAv3rIotvrN6kcXu66x7TSwzXCcfxWwy3955bVeR0mufGMXKx/cdDLyUYxDQ/KklKQqZH/PzOJ1+QCrXWb4vFkVe2xl2EnrRt+oj21yscqlIbJmpsYx1bZ/it62IY4PdK1RFJhbdK5DJddtTuWOohsTs8/X21kpT42xqMatZO/ZiQHy5QqywTCZ/GGcoWE+A/vWeWNLTtginJqZrGyiwq3/EWlzuDxUse530pPoydFkNTDqH4A2hnS58WESfZw/EKs1iuT2A/O9u5JJ10/m7DBJJ472LEwk4IesUTdES/yn0X7lKCYeUs49OS05Onre7rpqJyBO4NtjQHxKbohlta4AeQlLggBRG+b+fm61LL+50H5WK9KjvoqkqbHrJ/aOcUbpqm/AwNP1YYj9gq/DzOh0NQfnnkLNk5KeBWCj4TxOlHOJu73DeunjlmjjDtn3e3KMqHjD5nXLXXPiqrtcapg50JEzQo819Ff55ZaCrEbJ/LzX1f8tMTZDhAnKQy02fjoBM9h2YMZRGKPGLOZMKLMvl+V/e8vJ/eDa5MTuDnnLvgp/fjugmElmVMFZ6mmwYMXaGykHvRhO0iWfX3sgs4YHWgWugo+UfflhUaZUT9TYnayR7gz6is6CIKgF4fDR5qijKaP3CehTdVqYTVtDUnEOnP1fc3QUPAVLSmWP8VJkzoeVLHnRZV3hj+0swqv4J1aFNb11xBQjZPuzsJ4r7nLlBwo7zEyBMOAyX2MQnxcmm4DQTYzmqZyvRoumR+4zaFkjqkARpRo7PRTX1J/bMaElr0oO5XJQgvEO+yxZhOjS9SiDys2S4trkdsDaEB0HpOkgwyRhnP2UY9QrKSCAdkPyoyZx2L4fpwvz3vN0qAkyV8rXpkXbDD0tutE7wHWQrXxvQCZmqKtKftO8RP3rDvG80vX+UZSXUh3TLnPWm0Zag3Ot9Pl60jeTrioT7M6Lg9Gzs3EIaxPOITk
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 "all:repeat tac" is equivalent to "all:[>tac ; [> tac ; etc ..]
..]", and NOT to "all:tac;tac;..."
See this example:
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.
all:repeat (let t := type of a in idtac t;(intro+now auto)).
Undo.
(* equivalently*)
all: [> prg a; [> prg a ; [> prg a ; [> prg a ; [> prg a .. ].. ]..
].. ] .. ].
On one hand I think things behave the way they are described in the
documentation.
On the orher hand I tried to define a repeat2 tactical in ltac that
would apply things like an iteration of ";" but I did not succeed. If
someone knows how to do that I would be interested.
Hope this helps,
Pierre
> For example, based on what you say I might guess that
> all : repeat tac
> goes back and forth between two goals, applying tac to each (as though
> one instance of tac counted a bit of (repeat tac) - but it seems that is
> not what happens (eg as in my emails in the thread
> Re: [Coq-Club] goal selectors; tactic expressions)
>
> Cheers,
>
> Jeremy
>
> On 01/28/2019 11:53 PM, Pierre Courtieu wrote:
> > 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.
> >
- Re: [Coq-Club] "Sequence is associative." (?), (continued)
- Re: [Coq-Club] "Sequence is associative." (?), Jeremy Dawson, 01/24/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] "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
Archive powered by MHonArc 2.6.18.