Skip to Content.
Sympa Menu

coq-club - [Coq-Club] "Sequence is associative." (?)

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] "Sequence is associative." (?)


Chronological Thread 
  • From: Jeremy Dawson <Jeremy.Dawson AT anu.edu.au>
  • To: "coq-club AT inria.fr" <coq-club AT inria.fr>
  • Subject: [Coq-Club] "Sequence is associative." (?)
  • Date: Wed, 23 Jan 2019 09:32:27 +0000
  • Accept-language: en-US
  • Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=Jeremy.Dawson AT anu.edu.au; spf=Pass smtp.mailfrom=Jeremy.Dawson AT anu.edu.au; spf=Pass smtp.helo=postmaster AT AUS01-SY3-obe.outbound.protection.outlook.com
  • Ironport-phdr: 9a23:ePQ0bBeOWFJvovNLaJi4TZpYlGMj4u6mDksu8pMizoh2WeGdxcW6YB7h7PlgxGXEQZ/co6odzbaO4+a4ASQp2tWoiDg6aptCVhsI2409vjcLJ4q7M3D9N+PgdCcgHc5PBxdP9nC/NlVJSo6lPwWB6nK94iQPFRrhKAF7Ovr6GpLIj8Swyuu+54Dfbx9HiTahYr5+Ngm6oRnMvcQKnIVuLbo8xAHUqXVSYeRWwm1oJVOXnxni48q74YBu/SdNtf8/7sBMSar1cbg2QrxeFzQmLns65Nb3uhnZTAuA/WUTX2MLmRdVGQfF7RX6XpDssivms+d2xSeXMdHqQb0yRD+v6bpgRh31hycdLzM38H/ZhNFsjKxVoxyhpgBwzYHbb4yOKPpxZbnQcc8GSWZdXMtcUTFKDIOmb4sICuoMJeJWoJfnp1QQqBu/BRSnCu31xT5GnX/22qs62PkmHA/CwgMgBcwBsHHUrdnvOqkdS+60zLLPzTXFdP5ZwzH96JXSfh8/vP6MQKh8ftDMyUQ2EQ7Ok1ueqYvgPzyP1+QNtXCW7+tmVeK1im4osRt9oja1xsoql4LHhZoVx0jL+Cll2oo5OMG0RUxhbdK5HpZdtTuWO5ZqTs4sW21ltyI3xqcbtZO/fCUG0okrywDDZ/CdboSF7BHuWP6fIThmh39pZLeyihOw/ES8yeDxV8y53VlEriZbj9bBs3AA2AHT58ecT/Zx4Eas1DaM2g3V9+pKO1o7lbDBJJ4k2rMwloQcsUDEHiLuhEj5grKYelk59uSx9uroYLvrqoabN4BvlA7yKKMumtGjAesjNQgOQm6b9vmm2L375035R6lKgeMqnanFsZDaIsIbqrS+Aw9IzoYj7xG/DzCl0NgCgXYHK1dFdAqGj4jvJV7OPOj1APijj1i2jTtn2/LLMqf8DpjDLHXPiqrtcapz5kJEzQo819Ff55ZaCrEbJ/LzX1f8utjGAR8jLQO0xubmBM9z2IwEV2OPGaiZMKXJvFCS4OIvPvOAa5EItzbgMfQq/ePugWcjmVABZampwYcXaHegE/t6JEWZeGPgjcsFEWcXpQUzV/fqiV2HUT5LfXm+RaM85jchCIKnF4jPXI6tgKbSlBu8S9ddYXkDAVSRG1/pcZ+FUrECcmjadsRmi3kPUaWrY44nzxCn8gHgnelJNO3Rrw8Vr5/mxZBZ7vLIkhd6oR55FcmYwiehRn5vmWUgTjkrmq1zvAp01wHQguBDn/VEGIkLtLtyWQAgOMuElr0oO5XJQgvEO+yxZhOjS9SiDys2S4trkdYIfgBwF8jkhw2RhnP2UY9QrKSCAdkPyoyZx2L4fpwvwnDbkqQtkh8vX5kXbDD0tutE7wHWQrXxvQCZmqKtKftO9RP2rD7G9lvV+UZSXUh3TLnPWm0Zag3Ot9Pl60jeTrioT7M6Lg9Gzs3EIaxPOITk
  • Spamdiagnosticmetadata: NSPM
  • Spamdiagnosticoutput: 1:99


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?

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

Cheers,

Jeremy



Archive powered by MHonArc 2.6.18.

Top of Page