The Coq mailing list

[Andrew Appel <appel AT princeton.edu>]

Question: how to improve Coq's performance on proof automation for large terms.

Short answer:  reflection

Long answer: reflection, reflection, reflection.  And perhaps uconstr.

Proof automation on large terms is exactly what I've been struggling with for the last few weeks, as I am improving the performance of the Verified Software Toolchain on its new "Verified Software Unit" feature (see "Verified Software Units" by Lennart Beringer forthcoming in ESOP 2021).   What I've found to be effective is:

1. the systematic use of computational reflection;

2. use of boolean equality tests instead of decidable equality

3. in some cases, careful staging of computation

4. in some cases, use of uconstr instead of constr

5. in some cases, use Ltac pattern matching to learn things about terms, and carefully avoid doing reductions that will cause Qed to blow up.

But I still have many residual subgoals that are not reified into things for which reflection works;  that is, this is mixed computation and typechecking in Coq.  With a lot of Ltac programming.

Many of these principles (especially 1 and 2) are the foundation of the ssreflect system, of course.  I'm not using ssreflect, but I'm sure its features would have automated some of the things that I programmed by hand.

---

From: "Eddy Westbrook" <westbrook AT galois.com>
To: "coq-club" <coq-club AT inria.fr>
Cc: "Matthew Yacavone" <myac AT galois.com>
Sent: Friday, February 12, 2021 11:06:06 AM
Subject: [Coq-Club] Proof automation for large terms?

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