The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

This is actually the topic of a recent draft of mine, recently (re)submitted to POPL 2021.

Some background: One of the biggest bottlenecks in the rewrite tactics is the allocation of evars (in particular, the allocation of evar contexts) when instantiating lemmas.  This shows up mostly when you have a large context or many binders in the goal, and issues such as #12524 (setoid_rewrite and rewrite_strat are cubic in the number of binders even when there are no matches) and #12510 are about this.  Separately, even when there are no matches and no binders, autorewrite, rewrite, rewrite!, and rewrite? are all quadratic in the size of the goal (#12600).  So I would not say that autorewrite is already optimized, and I believe there are a number of relatively low-hanging fruit.

Second: Getting a proof term that does not incur overhead which is quadratic (or worse) in the number of rewrites is highly non-trivial; you may find the "Performance Bottlenecks of Proof-Producing Rewriting" section (Appendix A) of the aforementioned paper enlightening.

Given this, there is reason (and evidence) to expect that using a reflective procedure will speed things up for you.  I believe Rtac (see, e.g., Gregory Malecha's thesis) has a general reflective rewriter (though I was not able to make it work in recent versions of Coq, and development seems to be abandoned), and the rewriting engine that I created for fiat-crypto, which is the subject of the aforementioned POPL submission, is another example of such a general engine.  Unfortunately, I cannot in good conscience suggest that you use the framework that I built as anything other than an example; it suffers from a number of restrictions that could be lifted with engineering work (such as the fact that while any type without arguments is supported, the only type families supported are option and prod), and, more importantly, it's unmaintainable in its current form and should be rewritten from scratch.

Hope this helps,

Jason

On Wed, Jul 29, 2020 at 7:14 PM jonikelee AT gmail.com <jonikelee AT gmail.com> wrote:

Using Ltac profiling, it looks like about 40% of time spent in one
project I have is within autorewrite, the remainder primarily doing
proof search. The particular autorewrite hint dbs are not large (10 or
so rules each, one has only 3 rules) and the addition of rules ends
before the hint dbs are used. In such cases, would it be advantageous to
create a reflective procedure to replace use of autorewrite by a
particular hint db?  Or is this unlikely to improve performance,
considering that autorewrite is already optimized (presumably)?  I do
not beleive that Qeds are significantly time consuming in this project,
so I don't think shrinking the proof terms will have much benefit.