Is there any work (/any papers) on creating non-quadratic proof terms for multiple rewriting under binders / for `rewrite_strat`

? (In particular, I want a proof term that is linear in the number of binders being rewritten under, the number of rewrites, and the size of the goal.). cc @Pierre-Marie Pédrot @Matthieu Sozeau

How much work do you think it would be to modify `setoid_rewrite`

/ `rewrite_strat`

/ `autorewrite`

to generate a different proof term? (One which is convertible with the proof term currently being generated, but which is not quadratically sized in the number of binders/rewrite locations)

I think adding some let bindings to share some subterms in the proof could be done at a relatively low cost. Congruence proofs are quite expensive in terms of term copies, e.g. transitivity requires as arguments x y and z, along with the proofs that R x y and R y z which will again certainly have copies of x y and z. Otherwise said congruence proofs applied at depth n of a term always have copies of the subterms of depth n+1 (if any).

@Matthieu Sozeau Indeed for proofs without binders I'd like to see this happen, or at least an option to make it happen. Unfortunately even with let binders the proof cost is still (at least potentially) quadratic even if the proof term size is not, due to (1) https://github.com/coq/coq/issues/11838 (pretyping and native compilation are both quadratic in the number of nested (let-)binders), and (2) if we can't control the conversation strategy well enough, then unifying the let-bound-for-sharing type with the original type can incur quadratic overhead if the substitution of let binders is not handled correctly (I'm not sure whether or not Coq handles it correctly; I'd have to check. I probably should check this.)

So far I haven't managed to build any rewriting proof term that avoids quadratic cost, even when it's only linearly sized. (This is why I was asking about prior work on the topic.)

Furthermore, building a linearly sized proof term for rewriting under binders is significantly more complicated. I don't think it's currently possible in Ltac1 nor in Ltac2, as the only way I've figured out to build the term in sub-quadratic time requires an IntSet with amortized constant or logarithmic time operations, which I think Ltac2 doesn't support. (I'm also wondering if anyone has published an algorithm for linearly-sized proof terms for rewriting under binders.)

Last updated: Feb 01 2023 at 16:03 UTC