The Coq mailing list

[t x <txrev319 AT gmail.com>]

I was thinking about something similar, and I think one possible solution would be to build a layer on top of Coq, where all theorems/lemmas are nodes of a DAG (instead of being file based).

Then, whenever anything is changed, only the "descendants" need to be recompiled.

On Thu, Aug 8, 2013 at 5:35 AM, Kristopher Micinski <micinski AT cs.umd.edu> wrote:

All,

It's pretty common for me to work in ProofGeneral and adopt the following workflow:

 - Create a new file, importing or using some other modules

 - Write down some definitions

 - Attempt some proof

 - Recognize I should pull out a piece of the proof as a lemma, and do that.

 - Refine

The problem with this is that sometimes my files get pretty big, and use a lot of automation (not by necessity, but just because I'll be toying around with ideas and don't want to code up more elaborate Ltac specific to the proofs).  Unfortunately, this leads to the problem that I may refine some definition at the beginning of the file (say, adding another case to a definition) and the whole buffer has to be reprocessed.  The same thing happens even if you back up and repeat steps in ProofGeneral.

The insight is that very often pieces of proofs can be memoized: e.g., perhaps some lemma in the file is completely unaffected and thus the proof could be reified when it is first proved then when the same goal appears tried using (e.g.,) exact.  This would typically be much faster than automation for large proofs, and seems like a simple enough fix.

I don't believe this would be possible to code up in Ltac, but I believe that it would be possible to either extend Coq, or extend ProofGeneral (of which, perhaps the second would be the most appropriate place to start).

In my mind, the "dumb approach" would be to memoize whole proofs and attempt the same ones with something like `exact`.  You may be able to do more: memoizing pieces of the proof using the context, etc...

Has anyone looked at this before?

Kris