The Coq mailing list

["Jim Fehrle" <jfehrle AT sbcglobal.net>]

I’d like Coq to do much more of the search work needed to find proofs.

 

1) Adam Chlipala’s crush tactic seems like a promising step in that direction—with crush, the number of tactics needed for many proofs seems sharply reduced.  Has there been any thought about integrating this into the Coq code base and using it in the libraries?  Is this a good idea?  What would it take to do this?  (Note I’ve only read about crush, I haven’t tried it for myself yet.)

 

2) My impression is that verifying a proof is much faster than generating the proof from the tactics.  For example, I’ve noticed that compiling the .v files is the slowest part of building Coq.  Is there a user-friendly mechanism to save proofs so that Coq doesn’t need to re-generate proofs from the tactics?

 

If there was such a mechanism, it would be more practical to use very long-running tactics, such as exhaustive searches.  Would it be worthwhile to create or enhance such a mechanism?

 

3) If crush or an exhaustive search fails, users need diagnostic information to help them plan their next step (the human part of the search process).  I don’t know what form this should take—haven’t thought about it much.

 

FWIW I’m still a novice when it comes to Coq.  I want to focus on improving Coq rather than using it myself.

 

I’d appreciate your thoughts.

 

Thanks,

 

Jim