The Coq mailing list

[Nick Benton <nick AT microsoft.com>]

Quite. I often prove nested lemmas. They do feel dirty, and I always refactor the proof by pulling them out once the enclosing proof is complete. But during interactive development it’s much less convenient to undo the surrounding proof, state the lemma *without now being able to see the intermediate proof state in which you want it*, and then rerun everything to get back to where you were.

 

Nick

 

From: coq-club-request AT inria.fr [mailto:coq-club-request AT inria.fr] On Behalf Of Adam Chlipala
Sent: 03 August 2015 19:24
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] "Nested proofs are deprecated and will stop working in the next Coq version" - Can we keep this?

 

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.