The Coq mailing list

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

Dear Jim,

 

I don’t think that something like the crunch tactic is that helpful for larger developments. If I remember right, Adam wrote in his book, that this is more of an example, and that it needs to be tailored to what is needed in specific cases. The main question is how does a mechanism look for a highly configurable version of crunch.

 

The approach I usually use is as follows:

 

·        I use hint databases

·        I split theorems into two categories, those which are more suitable for forward search (extending from what you have) and those more suitable for backward search (going back from your goal). In which category a theorem belongs depends mostly on the relative specificness of the goals and hypothesis. Stuff with complex hypothesis and easy goal is better for forward search, stuff with complex goal and likely easy to satisfy hypothesis is more for backward search. One can easily see that this split improves proof search effectiveness very substantially.

·        Theorems in between I put together with some guard tactics, which check if the theorem is likely to be useful either in forward or in backward search.

 

My main problem is that Coq doesn’t have a good mechanism for a forward theorem databases and forward application. Hint databases and eauto work inherently in backwards mode. I would need a tactic which applies lemmas from a hint database as long as applicable lemmas exist. Eauto can’t be used for this (easily) because it insists on solving the goal and backtracks. I usually end up with a tactic in the hint database which does the forward stuff, but it requires really ugly hacks to get this extensible (although it works reasonably well in practice).

 

Regarding saving proofs: I think it would make more sense to have some sort of machine learning to guide eauto search to theorems which are applicable in certain situations. The result of something like this might get fairly scary … Saving proof terms likely has no significant advantages over using fine grain .v and .vo files with properly designed dependencies to minimize recompiles. I think the dependencies in quite a few Coq libraries and projects have not been designed but somehow happened, and are not specifically good examples for managing this.

 

Best regards,

 

Michael

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, Christian Lamprechter
Chairperson of the Supervisory Board: Nicole Lau
Registered Office: Munich
Commercial Register: Amtsgericht Muenchen HRB 186928