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: 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 12:02:53 +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-ua1-f48.google.com
  • Ironport-phdr: 9a23:CNe1rhwYb3/I9SbXCy+O+j09IxM/srCxBDY+r6Qd1OIeIJqq85mqBkHD//Il1AaPAd2Lraocw8Pt8InYEVQa5piAtH1QOLdtbDQizfssogo7HcSeAlf6JvO5JwYzHcBFSUM3tyrjaRsdF8nxfUDdrWOv5jAOBBr/KRB1JuPoEYLOksi7ze+/94HQbglSmDaxfa55IQmrownWqsQYm5ZpJLwryhvOrHtIeuBWyn1tKFmOgRvy5dq+8YB6/ShItP0v68BPUaPhf6QlVrNYFygpM3o05MLwqxbOSxaE62YGXWUXlhpIBBXF7A3/U5zsvCb2qvZx1S+HNsDtU7s6RSqt4LtqSB/wiScIKTg58H3MisdtiK5XuQ+tqwBjz4LRZoyeKfhwcb7Hfd4CSmVBUMReWSxPDI2/coUBEfYOMP1CoIXhvVYDtweyCRWuCe7p1zRGhmX23ao/0+k5Dw/G3BYnH9UWv3vXrdX1MaISXv6vzKnN1zrDafVW0ir65YjUchAuv/aMUahxcMrQzEkvEgLFg06fqYzgJTyV1+ANv3KH4OpnUOKikmgqoBx/rDiow8cjkIjJhoQNx1DF8yV52oc1KseiRE51e96pFoZbuSKCN4ZuXM8uX2VltDw5x7AGo5K3YjYGxIo9yxPQaPGKdZWD7Aj5W+aLOzh4gWpoeLKhiBa29kit0uj8WdO10FZOtyZFj8PDum0U2xzd5cWKSeFx/kim2TaI2ADT7v9LLVoomqrcLp4t2r8wlpwNvkTfBiL6hln6gauMekgn+uWk8frrbqv4qpOGOIJ5iRnyMqE0lcy+BeQ4PBIOX2+e+emkyL3j/VP2QLJQgvw3k6nZtZXaJcUAq662Bg9ayIcj6xKlAzi619QYmGELLEhZdxKfk4jpJ1bOLejkAve4mlSgiStkx/TbPrL6GZjNNXjCkLL5fbln8UJcyQwzzcpe551OEL0BLujzCQfNs4nzCQZxGAipya6zA9Jkk4gaRGinA6mDMaqUv0Xetcw1JOzZWI+UvwHPKv0g6uTrhHk/0QsBfaSum4kWbXW5NvtjKkSdJ3Hrh4FSQi8xogMiQbmy2xW5WjlJaiP3Bvpkv2BpOMedFY7GA7uVrvmE1Sa/EIdRYzkfWF+JGHbsMY6DXqVVMX7AEopaijUBEIOZZco5zxj37V31zrNmKqzf/ShK7cu+hugw3PXakFQJzRIxD8mZ1DvQHWR9n2dNWjZvma4j8QpyzVCM1aU+iPtdR4Re

Why did you think the output should be different? The part of the manual cited by Jeremy precisely says the converse.

Le mer. 23 janv. 2019 à 11:49, Cao Qinxiang <caoqinxiang AT gmail.com> a écrit :
This is an interesting question. I try the following script.

Variable a: nat.
Variable b: nat.

Ltac foo1 := try reflexivity; try split.
Ltac foo2 := try reflexivity.

Goal exists c, (c = a /\ c = a + b) /\ c = b.
eexists.
split; (foo1; foo2).
Abort.

Goal exists c, (c = a /\ c = a + b) /\ c = b.
eexists.
(split; foo1); foo2.
Abort.

I thought the outcome should be different. But it turns out to be the same. Anyone can explain that?

Best,
Qinxiang Cao
Shanghai Jiao Tong University, John Hopcroft Center
Room 1110-2, SJTUSE Building
800 Dongchuan Road, Shanghai, China, 200240



On Wed, Jan 23, 2019 at 6:19 PM Théo Zimmermann <theo.zimmi AT gmail.com> wrote:


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



Archive powered by MHonArc 2.6.18.

Top of Page