autorewrite is arbitrarily slow to fail in obvious cases

JasonGross commented 6 years ago

Version

8.7.0

Operating system

Linux

Description of the problem

Consider this code:

Require Import Coq.ZArith.ZArith.
Axiom g : nat -> Prop.
Axiom f : forall a : nat, g a = False.
Axiom f' : forall a0 a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 a12 a13 a14 a15 a16 a17 a18 a19 a20 : nat,
    g (a0 + a1 + a2 + a3 + a4 + a5 + a6 + a7 + a8 + a9 + a10 + a11 + a12 + a13 + a14 + a14 + a16 + a17 + a18 + a19 + a20) = False.

Definition bigt0 := ltac:(let t := eval vm_compute in Z.div_mod in exact t).

Ltac bigt' n :=
  lazymatch n with
  | 0 => constr:(bigt0 = bigt0)
  | S ?n => let v := bigt' n in
            constr:(v = v)
  end.
Ltac bigt n :=
  let v := bigt' n in
  eval cbv delta [bigt0] in v.
Notation big n := ltac:(let t := bigt n in exact t) (only parsing).

Axiom h : Prop -> Prop.
Axiom h' : forall a0 a1 a2 a3 a4 a5 a6 : big 11 = big 11,
    h (a0 = a1 /\ a2 = a3) = False.

Hint Rewrite
     f' f' f' f' f' f' f' f' f' f'
     f' f' f' f' f' f' f' f' f' f'
     f' f' f' f' f' f' f' f' f' f'
     f' f' f' f' f' f' f' f' f' f'
     f' f' f' f' f' f' f' f' f' f'
     f' f' f' f' f' f' f' f' f' f'
     : foo.
Hint Rewrite
     h'
     : hoo.

Goal True = True.
  Time autorewrite with foo.  (* 0.05 s *)
  Time autorewrite with hoo. (* 1.838 s *)

Note that Set Keyed Unification does not change the performance. The time of autorewrite with foo is dependent on how many arguments f' takes. The time of autorewrite with hoo grows exponentially with the argument to big, i.e., linearly with the term size of the arguments. This is absolute nonsense, and is a real bottleneck in fiat-crypto's src/Arithmetic/Core.v file. If the rewrite hint ends in an equality, and the LHS (RHS for <- hints) is headed by a global constant which does not appear anywhere in the goal, having that hint in the rewrite db should be free.

ppedrot commented 6 years ago

So the cost comes from the function Equality.instantiate_lemma, and more precisely its subcall to reduce_to_quantified_ind that keeps headish-normalizing your big term (it's calling simpl, AFAIU). I don't know how easily we can tweak that, I need to understand the invariants first.

JasonGross commented 6 years ago

that keeps headish-normalizing your big term (it's calling simpl, AFAIU)

Ew, really? I am failing to find a case that relies on simpl flags, though. Is there one?

ppedrot commented 6 years ago

You always have the problem of refolding fixpoints, so if ever you define some equality relation by a fixpoint over some inductive data structure, not having simpl is going to potentially leave the fixpoint unfolded in the body, which can be not pleasant. I agree that this is a very rare case though.

Actually, there is also a call to beta-iota reduction after that simpl pass, for the holy backward compatibility, and I think that this is the one that causes trouble in your instance.

JasonGross commented 6 years ago

Getting the hnf with refolding should still permit lazy evaluation of the arguments, in theory, right?

Anyway, maybe I should post the actual example. It's a lot more code, but if the solution requires fiddling with the reduction engine, not just adding a fast path that keys on head constants, then it's probably important to have the actual lemmas I'm having trouble with and not this fake minimized test case. (The case I'm actually running into looks a lot more like foo than hoo.)

JasonGross commented 6 years ago

relation by a fixpoint over some inductive data structure, not having simpl is going to potentially leave the fixpoint unfolded in the body, which can be not pleasant

I still think a fast path should be possible. Compute the headish inductive at Hint Rewrite time. If you can't, mark it as dynamic; otherwise cache it. Then we pay the cost only once. If need be, put this behavior behind a flag or database attribute.

mattam82 commented 6 years ago

Does Unset/Set Refolding Reduction change anything, by any chance? I think I have examples in Equations suffering from the same performance problem as well but didn’t investigate yet.

ppedrot commented 6 years ago

After a cursory glance, I'm under the terrible impression that the code of autorewrite doesn't use at all the underlying discrimination net and tries to rewrite with every hint in the base... The only part that actually takes advantage of the net is the hint strategy (as in rewrite strategies).