The Coq mailing list

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

On 08/03/2015 12:38 PM, Cedric Auger wrote:

2015-08-03 17:14 GMT+02:00 Soegtrop, Michael <michael.soegtrop AT intel.com>:

Dear Coq Users and Team,

recent versions of Coq give this message when proofs are nested (a new Lemma is started inside of a proof)

"Nested proofs are deprecated and will stop working in the next Coq version"

I would like to have a discussion on this because I use this regularly. I like a heavily automated proof style and when automation gets stuck, I tend to solve this by providing some additional idea in a new lemma and add this to the hint database. It makes sense to do this inline/nested for 2 reasons:

- it is quicker (at least during proof development) in case the automation did laboriously crunch through a few 100 cases successfully and left over only 1 or 2.

​You can still use the "assert" tactic, almost exactly the same way you use "Lemma".​

I'd like to second the request for keeping nested lemmas.  The big difference vs. [assert] is that nested lemmas may be used in parts of the proof script that are not in the binding scope of the point where you put the lemma proof.

The overwhelming motivation (for me) is to avoid wasting time rerunning the part of the current proof script, up to the point where you realize the lemma is called for.  I expect that the Coq team doesn't generally plan in terms of supporting cases where single lines of Ltac run for minutes or hours, but those cases are important to me and probably others, too.  [assert] avoids those problems but then limits the scope where the new lemma can be referenced.  Also, adding the lemma in the current context can cause undesirable perturbations in Ltac automation.  If the lemma statement is long, there can be a substantial performance cost.