Jason Gross (Jun 13 2020 at 03:41): Jason Gross (Jun 13 2020 at 03:41):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
Jason Gross (Jun 13 2020 at 20:10):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)
Matthieu Sozeau (Jun 15 2020 at 11:37):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).
Jason Gross (Jun 17 2020 at 15:45):@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.)
Jason Gross (Jun 17 2020 at 15:46):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.)
Jason Gross (Jun 17 2020 at 15:51):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: Jun 09 2023 at 07:01 UTC