The Coq mailing list

["jonikelee AT gmail.com" <jonikelee AT gmail.com>]

Thanks, Jason!


On Wed, 29 Jul 2020 22:51:51 -0400
Jason Gross <jasongross9 AT gmail.com> wrote:

> This is actually the topic of a recent draft of mine, recently
> (re)submitted to POPL 2021
> <http://people.csail.mit.edu/jgross/#partial-evaluation-rewriting>.
> 
> 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 <https://github.com/coq/coq/issues/12524> (setoid_rewrite
> and rewrite_strat are cubic in the number of binders even when there
> are no matches) and #12510 <https://github.com/coq/coq/issues/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
> <https://github.com/coq/coq/issues/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
> <https://people.csail.mit.edu/jgross/personal-website/papers/2021-rewriting-popl-draft.pdf#page=22>
>  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
> <https://gmalecha.github.io/publications/2015/extensible-proof-engineering-in-intensional-type-theory>)
> 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
> <https://github.com/mit-plv/rewriter>, 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
> <https://github.com/mit-plv/rewriter/issues/15>.
> 
> 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.
> >
> >