The Coq mailing list

[Pierre Courtieu <pierre.courtieu AT gmail.com>]

I agree with Adam. When the current proof script would take 5 minutes (or more) to rerun you don't want to lose these 5 minutes because of that stupid auxiliary lemma you forgot to prove. You just want to prove it and keep on with your main lemma. My point is that it should not stay nested in a finished proof because the nestedness is misleading and does not reflect the real structure of the document.

Thinking out loud: maybe nested lemmas should follow the same discipline as admits: a proof containing nested lemmas should not be ended by Qed?

Pierre

Le mardi 4 août 2015, Adam Chlipala <adamc AT csail.mit.edu> a écrit :

Again, for highly automated proofs, it often makes a huge difference to save the need to rerun even one line of a proof script.  This feature facilitates that process optimization.

On 08/04/2015 10:04 AM, Cedric Auger wrote:

If so, I was wrong about how nested lemma work (I did not tried it). And almost all what I wrote could be forgotten.

I simply guessed that the mechanism was similar to what occurs with the "abstract" tactic.

But well, in that case, I could not find really relevant arguments to remove this feature (but even less to keep it, in fact, beside retrocompatibility).

Thus I will only state that it needlessly (from my point of view) complicates the syntax, and I find it simpler to keep the "Lemma L1 : … Qed. Lemma L2 : … Qed …" form, rather than having well parenthesized "Dyck" lemmas.

In my experience of Coq, I never needed that feature.