The Coq mailing list

[Jonathan <jonikelee AT gmail.com>]

[oops - I hit reply instead of reply-list - forwarding...]

-------- Original Message -------- Subject: Re: [Coq-Club] Ending a section and its dependency analysis of global objects in it Date: Thu, 26 Jun 2014 11:35:04 -0400 From: Jonathan <jonikelee AT gmail.com> To: AUGER Cédric <sedrikov AT gmail.com>

On 06/26/2014 03:39 AM, AUGER Cédric wrote:
> Of course, having interactive abstract would be way better.

I think the problems I was having with Sections just means that one 
shouldn't use Sections for interactive abstract - so here's an 
alternative proposal:

Given a goal that does not contain evars, use emacs to turn the goal 
into a definition that is introduced into the current script just prior 
to the definition that produced the goal - and initially prove this new 
definition with admit.  That requires undoing back in the script - but 
once the new definition is proved via admit, one can roll forward back 
to the originating goal.  Then, prove that goal using eapply Foo; 
assumption (assuming Foo is the name chosen for the abstracted-out 
definition) - so that which actual arguments end up being used by Foo is 
not hard-wired into the proof script.

Or, if you can tolerate definitions in the middle of other definitions 
(Coq allows them - but does anyone use this feature?), the 
roll-back-roll-forward steps can be omitted, and the new abstracted-out 
definition gets inserted right in-line of the current proof script at 
the point of the goal it abstracts.

Later, prove Foo (in place of admitting it).  Then, apply another emacs 
function on that definition that deletes its arguments one at a time 
starting with the last and working backwards - each time checking if Foo 
can still be proven with the given script.  This is basically a 
"meta-ized" version of what Jason has done for abstract, using emacs 
instead of Ltac to do the dependency filtering (that I had wished 
Section would already be doing).

I am not an accomplished emacs hacker, but this doesn't seem like it 
would require much...

-- Jonathan