autorewrite, rewrite, rewrite!, and rewrite? are all quadratic in the size of the goal even when there are no occurences

[JasonGross]

Description of the problem

Consider this code:

Axiom f : nat -> nat.
Axiom g : nat -> nat.
Axiom fg : forall x, f x = g x.

Axiom f' : nat -> nat -> nat.
Axiom g' : nat -> nat -> nat.
Axiom f'g' : forall x y, f' x y = g' x y.

Hint Rewrite fg : rew_fg.

Fixpoint comp_pow {A} (f : A -> A) (n : nat) (x : A) {struct n} : A
  := match n with
     | O => x
     | S n => f (comp_pow f n x)
     end.

Fixpoint comp_pow_tree {A} (f : A -> A -> A) (n : nat) (x : A) {struct n} : A
  := match n with
     | O => x
     | S n => f (comp_pow_tree f n x) (comp_pow_tree f n x)
     end.

Local Infix "^" := comp_pow : core_scope.

Notation goal_noop n := (forall x, (g^n) x = (g^n) x).
Notation goal_noop_exp lgn := (forall x, comp_pow_tree g' lgn x = comp_pow_tree g' lgn x).

Ltac redgoal _ := cbv [comp_pow comp_pow_tree]; intro.

On goals of the form goal_noop n, we can follow redgoal () with autorewrite with rew_fg, try rewrite !fg, try rewrite fg, or rewrite ?fg. All of these are quadratic in n:

Interestingly, SSReflect's rewrite does not suffer from this issue, having performance linear in the size of the goal, and only takes more than a second on goals larger than 10⁶ terms (goal_noop_exp lgn for lgn >= 19):

(the "cold" line is for a cold cache; the rest are run on the same goal immediately after running the cold-cache one)

This isn't super-high priority, but goals (e.g., in the category theory library) can easily reach upwards of 50,000 terms, and having autorewrite take 3 seconds (or more) to do nothing is kind-of slow.

What's causing the quadratic behavior here?

cc @ppedrot @mattam82

Coq Version

8.11

[JasonGross]

@ppedrot Is this evar allocation or something else?

[ppedrot]

So, it's not so much evar allocation, but it's indeed indirectly due to the fact that the evar contexts are linear. The problem is that the old unification checks that a term is closed before deciding what to do (in Unification.matchrec), and rewrite relies on unification to apply the lemma. I had a patch somewhere that probably solved this problem which was even turned into a PR, but closed because no observable effect.

EDIT: this is #14253.

[ppedrot]

I confirm that #14253 solves the issue.

[JasonGross]

@ppedrot #14253 only fixed this when the rewriting lemma has no evars, right?