The Coq mailing list

[Andrew Appel <appel AT cs.princeton.edu>]

I strongly agree with Adam.

Nested lemmas are very useful during proof development.

Then we often clean up our proof scripts so that you don't see nested lemmas in our published proofs.

Please do not remove nested lemmas from Coq.

-- Andrew Appel

---

From: "Adam Chlipala" <adamc AT csail.mit.edu>
To: "coq-club" <coq-club AT inria.fr>
Sent: Tuesday, January 22, 2019 9:18:32 AM
Subject: Re: [Coq-Club] proving a lemma in a proof

It's certainly the Coq developers' prerogative to focus maintenance
effort in the way you set out, but to those of us doing serious program
verification, where nested lemmas so far seem like an indispensable
feature to avoid having to replay costly proof scripts, your position
comes across frustratingly close to "the Coq developers have decided to
prioritize pure-math applications over verification of realistic
systems."  The latter category probably musters significantly more
funding in the world today, so there is a real danger of a decision at
some point to fork a version oriented toward system verification, which,
after some growing pains, could easily wind up with significantly more
engineering effort devoted and, after a few years, effectively replace
the original Coq version and in some sense remove effective ownership of
the system from Inria.

That doesn't sound like such a nice scenario, so I just wanted to
emphasize the danger here.  Coq is already being used for several
industrial applications, and the Coq team sometimes comes across as
stuck in the 20th-century world where it was quite hypothetical that
there would be real commercial users whose processes could be ruined by
e.g. ceasing to maintain the nested-lemma feature.

On 1/22/19 2:47 AM, Théo Zimmermann wrote:
> Sorry to insist but the simplest answer to this question is: use a
> proper interface which will allow you to state your lemma and prove it
> outside (above) your current proof. Nested lemmas are a feature whose
> use is strongly discouraged. Some users insist they need it (in
> particular during computation heavy proofs) and that's the only reason
> the feature has not been removed but the Coq developers are not
> interested in fixing bugs it may have...