The Coq mailing list

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

On 08/04/2015 11:13 AM, Pierre Courtieu wrote:
> 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?

My complaint about that feature of Coq 8.5 is that running [Admitted] 
doesn't check that there are no subgoals left, so it's hard to be sure 
that you haven't actually given up the proof earlier than you wanted.  
In Coq 8.4, I discharge subgoals that I want to save for later using 
[admit] and then run [Qed].