coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Théo Zimmermann <theo.zimmi AT gmail.com>
- To: Coq Club <coq-club AT inria.fr>
- Subject: Re: [Coq-Club] "Sequence is associative." (?)
- Date: Wed, 23 Jan 2019 14:13:00 +0100
- Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=theo.zimmi AT gmail.com; spf=Pass smtp.mailfrom=theo.zimmi AT gmail.com; spf=None smtp.helo=postmaster AT mail-vs1-f46.google.com
- Ironport-phdr: 9a23:hyD92x8hVn305f9uRHKM819IXTAuvvDOBiVQ1KB30uocTK2v8tzYMVDF4r011RmVBdWds6oMotGVmpioYXYH75eFvSJKW713fDhBt/8rmRc9CtWOE0zxIa2iRSU7GMNfSA0tpCnjYgBaF8nkelLdvGC54yIMFRXjLwp1Ifn+FpLPg8it2O2+557ebx9UiDahfLh/MAi4oQLNu8cMnIBsMLwxyhzHontJf+RZ22ZlLk+Nkhj/+8m94odt/zxftPw9+cFAV776f7kjQrxDEDsmKWE169b1uhTFUACC+2ETUmQSkhpPHgjF8BT3VYr/vyfmquZw3jSRMNboRr4oRzut86ZrSAfpiCgZMT457HrXgdF0gK5CvR6tuwBzz4vSbYqINvRxY7ndcMsVSmpPXMlfVyJPDIChYYURE+UMJvxXo5XnqlYUsReyGQuhCeXywTFInH/22qg63vw/HwHGxgsgGMoBv3fVrNXwMacdT/q1zKzSwjXFafNdxDDw6JTIch8/pvGAR7NxccvUyUkqFgPIlVqQqYn/MDOU0uQBqXSU7+1lVe+2jWMstg9/oj+qxsg2i4nJgJoYylHC9SVjwYY6P8e0SEBhYdK8H5tQtj2aN4trQsw5WW1npCE6yrgAtJWmfyYK0IwqywDDZ/GDaYSF4RLuWPyPLTtlhn9pYr2yihe0/EO90OPzTNO030xPriddktnDqHQN1xvL58iCUPR9/0Oh1S+R1wDI9+1IOE40mKXaJpI7zb4wkZ0TsUvHHiDogkn5kKiWdkA89uip7eTofKnmq4eCO4NojgzyKKcjl8ylDegmLwQDXXKX9Ou92bH7+E32WrRKjvk4kqnDt5DaINwWprK5AwBL1YYv8Re+Dzaj0NQdnHkKN11FeBedgIjoP1HCOuz3DfC6g1i0ijdk2+jGPqH9ApXKNnXMjLDhfa9k50FAzAoz0MtQ6olPCrABJfLzQlX+uMbZDh8/KQy0wvzoBM9z1oMECiqzBfqyN7qamluV7Kp7KO6VIYQRpTzVKv4/5veog2VvynEHeqz84ZuWb0eKH/FjLl+caHzqyoMdEWoN+Bg/SenroFKHWD9XIX21WvRvtXkAFIu6ANKbFciWi7ub0XL+R8UOPzEUOhW3CX7tMr68dbIJYSOWLNVml2VdB7ekQo4lkxqpsV2jkuY1Hq/v4iQd8Knb+p1t/eSKzEM98DV1C4KW1GTfFzgpzFNNfCc/2eVEmWI4ylqH1vIl0flRFNgW+egQFwlma9jTyOt1D920UQXELI+E
Jean-Christophe, indeed, the documentation is incorrect. The two bind at the same level. I've fixed that as part of https://github.com/coq/coq/pull/9384.
Jeremy, you are absolutely correct when you remark that:
split ; foo3.
does the same as
split. all : foo3.
which does the same as
split. 2 : foo3. 1 : foo3.
but is different from
split. 1 : foo3. 2 : foo3.
does the same as
split. all : foo3.
which does the same as
split. 2 : foo3. 1 : foo3.
but is different from
split. 1 : foo3. 2 : foo3.
ie the step
all : foo3.
acts on subgoal 2 before subgoal 1
all : foo3.
acts on subgoal 2 before subgoal 1
This is because by default tactics work on multiple goals at the same time, and ";" will carry this property.
If you replace "all: foo3" with "all: [> foo3 .. ]", it forces the tactic to be called independently on each goal.
Le mer. 23 janv. 2019 à 13:32, Jean-Christophe Léchenet <jean-christophe.lechenet AT irisa.fr> a écrit :
For the following kind of tactic _expression_, the associativity is not so clear:
Goal (True /\ (False \/ True))
/\ (True /\ (False \/ True)).
Proof.
Fail split; split; [|right].
(* The command has indeed failed with message:
Tactic failure: Incorrect number of goals (expected 4 tactics). *)
split; (split; [|right]).
I understand that the manual treats ";" and "; [ ]" as two separate notations, in which case my example is not a contradiction to the associativity of ";".
However, it also notes that "; [ ]" binds more closely than ";", which does not seem to be the case in my example.
Jean-Christophe
Le 23/01/2019 à 11:18, Théo Zimmermann a écrit :
Le mer. 23 janv. 2019 à 10:33, Jeremy Dawson <Jeremy.Dawson AT anu.edu.au> a écrit :
Hi,
thanks for all the answers to my previous questions, some of which I'm
still working through.
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? What if the tactics do some instantiating of
existential variables, then the order of attacking subgoals would matter?
The order would be the same in both cases.
Also, for the same reason, it would be useful to know, for
tac1 ; tac2
which order tac2 is applied to the subgoals resulting from tac1
This can depend on tactic, but in practice it would be in the listed order of the goals for virtually all tactics.
Cheers,
Jeremy
- [Coq-Club] "Sequence is associative." (?), Jeremy Dawson, 01/23/2019
- Re: [Coq-Club] "Sequence is associative." (?), Théo Zimmermann, 01/23/2019
- Re: [Coq-Club] "Sequence is associative." (?), Cao Qinxiang, 01/23/2019
- Re: [Coq-Club] "Sequence is associative." (?), Théo Zimmermann, 01/23/2019
- Re: [Coq-Club] "Sequence is associative." (?), Théo Zimmermann, 01/23/2019
- Re: [Coq-Club] "Sequence is associative." (?), Jeremy Dawson, 01/23/2019
- Re: [Coq-Club] "Sequence is associative." (?), Théo Zimmermann, 01/23/2019
- Re: [Coq-Club] "Sequence is associative." (?), Théo Zimmermann, 01/23/2019
- Re: [Coq-Club] "Sequence is associative." (?), Jean-Christophe Léchenet, 01/23/2019
- Re: [Coq-Club] "Sequence is associative." (?), Théo Zimmermann, 01/23/2019
- Re: [Coq-Club] "Sequence is associative." (?), Théo Zimmermann, 01/23/2019
- Re: [Coq-Club] "Sequence is associative." (?), Jeremy Dawson, 01/24/2019
- Re: [Coq-Club] "Sequence is associative." (?), Jeremy Dawson, 01/24/2019
- Re: [Coq-Club] "Sequence is associative." (?), Théo Zimmermann, 01/23/2019
- Re: [Coq-Club] "Sequence is associative." (?), Théo Zimmermann, 01/23/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." (?), 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." (?), Cao Qinxiang, 01/23/2019
- Re: [Coq-Club] "Sequence is associative." (?), Théo Zimmermann, 01/23/2019
Archive powered by MHonArc 2.6.18.