The Coq mailing list

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

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