The Coq mailing list

["Soegtrop, Michael" <michael.soegtrop AT intel.com>]

Dear Enrico,

thanks a lot for clarifying the root cause of this. Now we know what the 
stakes are. I think that asynchronous / parallel proof processing is 
definitely a feature worth dropping nested proofs.

One solution to my problem of inaccessible proof states with automation might 
be to proof the lemma beforehand, but to add it to the hint database later.

Best regards,

Michael

-----Original Message-----
From: 
coq-club-request AT inria.fr
 
[mailto:coq-club-request AT inria.fr]
 On Behalf Of Enrico Tassi
Sent: Tuesday, August 04, 2015 7:53 PM
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 Tue, Aug 04, 2015 at 10:36:28AM -0400, Adam Chlipala wrote:
> 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.

Hello, the warning was added because the current implementation/behavior is a 
source of complexity. For example the global scope of a nested lemma makes it 
impossible to process the enclosing proof asynchronously.

The new warning is generated when the enclosing proof is ended to still let 
people state, and even prove, the nested lemma where/when its need is felt, 
but then the user is asked to put the script in flat form, to ease the 
re-processing of the document. Not putting the file in a flat format for 
performance reasons is debatable: when both the enclosed and enclosing lemmas 
are top level and complete , Coq is able to process their proofs 
asynchronously, so you don't have to wait much (this is what happens if you 
refactor the script when you see the warning). 

When the nested lemma is morally local but useful to many sub goals I think 
assert is more clean, and some proof languages even have support for 
bubbling-up sub proofs as much as needed with minimal edits.

On a side note, are nested lemmas documented?

best
--
Enrico Tassi
Intel Deutschland GmbH
Registered Address: Am Campeon 10-12, 85579 Neubiberg, Germany
Tel: +49 89 99 8853-0, www.intel.de
Managing Directors: Christin Eisenschmid, Prof. Dr. Hermann Eul
Chairperson of the Supervisory Board: Tiffany Doon Silva
Registered Office: Munich
Commercial Register: Amtsgericht Muenchen HRB 186928