coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] [SUSPECTED SPAM] Re: "Sequence is associative." (?)

From: Pierre Courtieu <pierre.courtieu AT gmail.com>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] [SUSPECTED SPAM] Re: "Sequence is associative." (?)
Date: Sun, 3 Feb 2019 15:42:21 +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:WLp81h3ELYIE5ltWsmDT+DRfVm0co7zxezQtwd8Zse0VKfad9pjvdHbS+e9qxAeQG9mDu7Qc06L/iOPJYSQ4+5GPsXQPItRndiQuroEopTEmG9OPEkbhLfTnPGQQFcVGU0J5rTngaRAGUMnxaEfPrXKs8DUcBgvwNRZvJuTyB4Xek9m72/q99pHPYAhEniaxba9vJxiqsAvdsdUbj5F/Iagr0BvJpXVIe+VSxWx2IF+Yggjx6MSt8pN96ipco/0u+dJOXqX8ZKQ4UKdXDC86PGAv5c3krgfMQA2S7XYBSGoWkx5IAw/Y7BHmW5r6ryX3uvZh1CScIMb7S60/Vza/4KdxUBLnhykHODw5/m/ZicJ+kbxVrw66qhNl34LZepuYOOZicq7fe94RWGpPXtxWVyxEGo6ydYoPAPQbPeZCsYb2ukUDrRyjBQm2GOPvyyFHhmLr1qA9y+QhEB/J3BY6H90QqnjbsNL1NLoIUeCpzanH0yjDYuhZ2Tf48ofIcxQhreuQUrJ3dMrc0E8iHB7GgFWIsYHpIS+Z2+AXv2WY7+dsT/+jhm8mpg1rvzSixMMhh4/UjYwP0F/E7z92wIMtKN24VkF7ZdmkHYNVty6ANot2RtouQ2B0uCon07EGt4O3cSoOxZg9yB7fbPuHc4eM4h39TuqePTB4hHd9dLK+gRa971Sgx/XiWsWo1FtGtClIn9nWunwQ1hHe69KLRuZ/80qlwTqP0hrc6uBAIUA6j6rbLJshz6YolpoSr0vDBDX2l1vsgKCKcUUk5/Ko6/jmYrr4u5+RLIB0igTkPaQvnsyzG/g3Mg8LX2SD4+SzyKXj/VHlQLVNlvA5jq7ZsInDKcsHoq65HhRa35046xe/CjemyM4XkWMGLFJDYhKHjpLmN0vAIPDiXr+DhAGnly4uzPTbNJXgBI/MJz7NiuTPZ7F4vnZdxRApwJh04I9OFrAMPbqnQk78rsbVSBQ+Lhaowuv6INp434IaH2mIB/nKY+vprVaU67d3cKG3b4gPtWOlcql317vVlXY83GQlU+ys1JoTZmq/G60/cUqcaHvoxNwGFDVT51ZsfKnRkFSHFAVrSTOqRatlv2M0DYunCcHIQYX/2OXcjhf+JYVfYyV9Mn7JEXrscN/aCfIFaSbXI9M41zJdCunnRIgm2hWj8gT9zug/Iw==

Le jeu. 31 janv. 2019 à 01:10, Jeremy Dawson <Jeremy.Dawson AT anu.edu.au> a écrit :

On 29/1/19 3:41 am, Pierre Courtieu wrote:
> all:tac. applies the tac to all goals.
> Period.

Well, IMRO this is pretty unsatisfactory. Since the order of applying
tactics (or parts of them) to subgoals matters (as in the case, for
example, of instantiating existential variables) you are making it seem
that coq's design is so complicated that it is not worth while trying to
describe it.

I don’t know. Maybe the order in which goals are treated should be explicited in documentation. Or maybe not. If one wants to force a particular ordering then it is possible by focusing.

And there is certainly nothing in the documentation, as far as I can
see, to explain, or even to alert the user to the fact that
all : solve_eqs
when there are two subgoals, solves both, whereas
all : repeat solve_eqs
leaves one of them unsolved

It is sais in documentation as far as I can tell: « applied to each goal independently means that is equivalent to 1:repeat solve_eqs. 2:repeat solve_eqs...

But indeed we need a repeat with the interleaved semantics.

Can you fill a big report about that please?

Best regards

Pierre

Cheers,

Jeremy

Re: [Coq-Club] [SUSPECTED SPAM] Re: "Sequence is associative." (?), Pierre Courtieu, 02/03/2019
- Re: [Coq-Club] [SUSPECTED SPAM] Re: "Sequence is associative." (?), Théo Zimmermann, 02/03/2019
- Re: [Coq-Club] [SUSPECTED SPAM] Re: "Sequence is associative." (?), Jeremy Dawson, 02/04/2019