The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

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...