Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] proving a lemma in a proof

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] proving a lemma in a proof


Chronological Thread 
  • From: Adam Chlipala <adamc AT csail.mit.edu>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] proving a lemma in a proof
  • Date: Thu, 24 Jan 2019 14:56:41 -0500
  • Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=adamc AT csail.mit.edu; spf=Pass smtp.mailfrom=adamc AT csail.mit.edu; spf=None smtp.helo=postmaster AT outgoing-stata.csail.mit.edu
  • Ironport-phdr: 9a23:KKsVex+AJsBtsP9uRHKM819IXTAuvvDOBiVQ1KB40eMcTK2v8tzYMVDF4r011RmVBdWds6oMotGVmpioYXYH75eFvSJKW713fDhBt/8rmRc9CtWOE0zxIa2iRSU7GMNfSA0tpCnjYgBaF8nkelLdvGC54yIMFRXjLwp1Ifn+FpLPg8it2O2+557ebx9UiDahfLh/MAi4oQLNu8cMnIBsMLwxyhzHontJf+RZ22ZlLk+Nkhj/+8m94odt/zxftPw9+cFAV776f7kjQrxDEDsmKWE169b1uhTFUACC+2ETUmQSkhpPHgjF8BT3VYr/vyfmquZw3jSRMMvrRr42RDui9b9mRgL2hicJNzA382/ZhcJ/g61ZvB2vqAdyw5LXbYyPKPZyYq3QcNEcSGFcXshRTStBAoakYoYTEuUOJ+NYpJTjqlsOqRu+BBGsC/nryjBSm3T72rc13Pk7HgHDwAMtBM4BsG/Oo9X0MKceS+W1zKjUzTnZcfxZxCr95ZHOfxs8ov+MRap9fdfPxUQsDQ/IgEmcpZb7Mz+PyOgBrnSX4/J9We6xiGMrsQ98riS1ysoolIXFnJwZxk7Z+Sh/3Y07P8e3SFRhbt6hCJZQtz+VN49xQs46RGFopTo6yrIBuZ66eigKx40rxwXDa/Odb4iH+AjvW/qKIThihXJlfKizhxOz8Ui80OHzSNS70EtSoipElNnDqGwN2gTO5sSZSfZx5Ems1SqV2wzN8O1IP104mbbDJ54k2LEwl54TsUrZHi/xnUX7lLWZeVg+9eit9+vqeanppoSGOI91jgHyKKEums2jAegiLAcBQnWb9fym1LL/5U35XKlKjvoun6bFt5DaPN0XqbK9Aw9IyYku8A2/Djej0NQAh3YLNlNFeBSdj4joIV7COv74De3sy2irxTxs3rXNOqDrKpTLNHnK1rn7Lphn7EsJ4QY6yJh055ZVErgFKbqnU0P4sdfwBQQwMgjyxuf7Tthxy9VNCiq0HqaFPfaK4hez7eU1LrzUPd5HiHPGM/EgosXWozo8kF4Zc7Ou2MJKOnujF/ViZUCYfTzhjspTSD5W7Dp7d/TjjRi5aRAWf2y7Bv9u7SoyCYbgCIbfAI2hne7ZhXrpLthtfmlDT2u0PzLoeoGDAK9ebz+OLchglDNBTqSoV4Zn3gqntQu8zrt7aOfY539AuA==

Thanks for the clarification of the challenges.  I, at least, agree that nested lemmas matter only as a workaround for UI/performance issues.  It would be awesome to be able to start a new lemma proof before an in-progress lemma and have everything work out without need to replay scripts.

Many of the developments I work on have the property that, while verifying a new program with high automation, we start with a tactic that produces a healthy number of verification conditions (100 is a good ballpark figure).  Each one is then hit with the same big-hammer automation tactic, which could easily take one minute per invocation.  This tactic leaves subgoals around when it isn't able to prove a goal completely, and those subgoals often suggest new hint lemmas that should be proved and registered.  What's needed is a way to prove & register those lemmas without replaying the prior big-hammer invocations... even though clearly registered hints could, in theory, change how the prior invocations ran!  It just isn't worth waiting for everything to be rechecked every time we find a new hint that was missing.  I hope this paragraph explains why nested lemmas are often "strictly necessary" for this kind of development in today's Coq.  I would still rather be able to edit new lemmas asynchronously without disturbing in-progress proofs.

On 1/24/19 12:40 PM, Enrico Tassi wrote:
I believe that the problem is that is makes other things more
complicated (checking proofs in parallel is an example I gave you in
the past IIRC).

Take this example:

Lemma a ...
..
apply b.
..
Lemma b ...
...
Qed.
..
apply b.
..
Qed.

[...]

As a result, as of today we can't process the two proofs in parallel
(if they come nested) while we could if they were one after the other.
The intuition that nesting a lemma is like writing it before is
reasonable, but not correct when we look at the dirty details.

As far as I know this feature is only used to work around UI,
performance, and documentation issues. Hence I believe that while we
work on solving these other issues, that would benefit all kinds of
users, it is reasonable to discourage the use of nested lemmas (unless
it is strictly necessary).



Archive powered by MHonArc 2.6.18.

Top of Page