The Coq mailing list

[Gabriel Scherer <gabriel.scherer AT gmail.com>]

On Mon, Aug 12, 2013 at 9:08 PM, Kristopher Micinski <micinski AT cs.umd.edu> wrote:
> I think this would help a lot for usability and might lead to some interesting research.

The good news is that this has already led to interesting research (with hopefully more to come), as you can find in Matthias Puech's PhD thesis, "Certificates for incremental type checking"
  http://www.cs.unibo.it/~puech/thesis.pdf
  http://www.cs.unibo.it/~puech/#research

On Mon, Aug 12, 2013 at 9:08 PM, Kristopher Micinski <micinski AT cs.umd.edu> wrote:

Yes, that would be the self adjusting inspired way to handle this.  In fact, one could say that this structure is approximated right now by using multiple modules.  I haven't thought about this from the deeper perspective of why this is necessary, or how it would play with the module system (i.e., would it be a transparent layer, or integrate with the language, my thought is the former).

I think this would help a lot for usability and might lead to some interesting research.  One thing that would be to ask, more than the naive strategy of calculating dependencies: are there smarter equivalences that could be inferred.

In the ideal case this would apply in the broader range to (pieces of) automation rather than simple raw proof objects: what if something in your environment can be attacked using "almost the same" strategy as something you've done before.

Kris

On Mon, Aug 12, 2013 at 2:20 PM, t x <txrev319 AT gmail.com> wrote:

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