The Coq mailing list

[Clément Pit-Claudel <cpitclaudel AT gmail.com>]

On 2/12/21 11:06 AM, Eddy Westbrook wrote:
> 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?

How slow is slow?  We had a lot of these issues in Fiat, and we basically 
decided to be happy with derivations in the order of minutes.

One thing that helps is to shrink your terms as much as possible.  This can 
mean `set`-ing things into the context or `Define`-ing constants out of your 
proofs (for example, we had dependent types that made many references to the 
same `string`s; we got measurable speedups by moving these strings to 
`Definition`s).

In some version of Coq, unifying a variable against itself is faster, so you 
could try seeing if `set`ting your largest terms before applying your lemmas 
is faster.  

Do you get the same performance issues with `simple refine` as with simple 
apply?