The Coq mailing list

[Enrico Tassi <enrico.tassi AT inria.fr>]

On Wed, 2019-01-23 at 09:52 +0000, Soegtrop, Michael wrote:
> In case I got it wrong, can you explain what the problem with nested
> proofs is, so that a mere Coq user can understand it?

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.

Note that the two "apply b" are different, the former is
from an Imported module, for example, while the latter is
the nested lemma b.

One cannot really check the document as if b was coming before a
since he would "capture" both occurrences of "b" and change the
meaning of the document. Or actually he could, but he would have to
perform a more complex binding analysis and transformation (than just
moving the text of b before the text for a). Ltac1 is very buggy^W
liberal wrt binding, so it would not be easy to code this
transformation reliably.

Similar problems involve universes (names and constraints), as other
pointed out.

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

My2C,
-- 
Enrico Tassi