The Coq mailing list

[Jim Fehrle <jim.fehrle AT gmail.com>]

Hi Jeremy,

A crude workaround would be to re-enter the lemma using a new name, then do proof cleanup later on.  It would help to file a bug report at https://github.com/coq/coq/issues with a short but complete example that shows the problem.

Jim

On Tue, Jan 22, 2019 at 8:29 AM Maxime Dénès <mail AT maximedenes.fr> wrote:

Hi Adam,

Verification of realistic systems is very much something that the Coq
developers have in mind.

The situation with nested lemmas is complex, because it is partially a
chicken-and-egg problem, as it is making some improvements (that would
precisely help increase productivity) more difficult.

However, the plan is not to remove the feature until we provide
replacements that users judge satisfactory (like a better interaction
model with UIs). It is very clear to us that it is not the case today,
and there is no plan to remove the feature in the short term. It has
been disabled by default because it was often used by accident by
beginners, but can be enabled via a simple option.

We (more precisely, Emilio, Enrico, Vincent and I) recently started an
effort at improving the general situation w.r.t. UI support, starting
from the Coq side. We hope it will lead to an improved experience,
especially in the context of large-scale proofs. It involves a lot of
very technical work on the state, document representation and phasing of
the system, so we will need some patience from our users, but we hope
the result will be worth it.

As a side remark, the development processes are now fully open, so
"significantly more engineering effort" could already be added to what
is currently being done (and indeed very welcome), if investors are
willing to fund it, without the need for forking.

Maxime.

On 1/22/19 3:18 PM, Adam Chlipala wrote:
> 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...