The Coq mailing list

[Eddy Westbrook <westbrook AT galois.com>]

Fellow Coq clubbers,

Does anyone have experience using proof automation and hint databases to 
prove theorems with large terms?

We are working on building a tactic to generate refinement proofs for monadic 
terms. Choosing the proof rule to apply in almost every case is rote, and can 
be done with a simple pattern-match on the top-level form of the terms. 
However, we have found that the automation really slows down when the terms 
start to get large. After profiling the tactic, it seems that it is just the 
“simple apply” rules generated by Resolve hints that are taking the majority 
of the time. I assume this is just unification running over large terms?

Anyway, any suggestions would be greatly appreciated!

Thanks,
-Eddy