Coq equtions is very very slow · Equations devs & users

Equations converts_to (t1: Term) (t2: Term) (fuel: nat): bool :=
converts_to (var x1) (var x2) _ := x1 == x2;
converts_to (univ l1) (univ l2) _ := l1 == l2;
converts_to (pi A1 B1) (pi A2 B2) (S n) := converts_to A1 A2 n && converts_to B1 B2 n;
converts_to (lam A1 t1) (lam A2 t2) (S n) := converts_to A1 A2 n && converts_to t1 t2 n;
converts_to (appl a1 b1) (appl a2 b2) (S n) with (multi_reduce_head n (appl a1 b1)), (multi_reduce_head n (appl a2 b2)) := {
    | Ok t1, Ok t2 => converts_to t1 t2 n
    | _, _ => (converts_to a1 a2 n) && (converts_to b1 b2 n)
    };
converts_to _ _ _ := false.

But It has few more cases many of which use the keyword with (I mainly do this for funelim) but it is taking too much time to compile this function (7 minutes and still going) I am not sure if it will go forever, I wonder why is it slow, and what can I do about it and still get nice funelims.

walker (Jan 17 2023 at 13:32):

Edit: I tried removing some of the cases and convert them to matches, and it is somewhat faster, so the question is what computation is taking long time, and it is something tht can be disabled ?
Also currently funelim gives 58 branches.

Paolo Giarrusso (Jan 17 2023 at 13:50):

FWIW, looks like writing an inductive judgment and a plain Coq decision procedure for it should be a decent backup. I'm not sure whether there are unexpected slowdowns in Coq conversion (Unification Debugging might help find, and Opaque might help fix) or intrinsic complexity problems with the program and Equations's translation

Paolo Giarrusso (Jan 17 2023 at 13:51):

The inductive here would have 5 branches, while this match in plain Coq expands to (about) 2 * (constructor_count Term)^2 cases

Paolo Giarrusso (Jan 17 2023 at 13:52):

Paolo Giarrusso (Jan 17 2023 at 13:54):

Not sure if the translation to eliminators can take space linear in the input size?

walker (Jan 17 2023 at 13:58):

I imagine the full thing has about 150 branches (including unrolling all the instances of _) I imagine that is pushing things to the edge of what coq-equations can do ?

walker (Jan 17 2023 at 13:58):

but yes, I am implementing a version of some inductive judgement as a fixpoint-like thing.

Théo Winterhalter (Jan 17 2023 at 13:59):

Théo Winterhalter (Jan 17 2023 at 14:00):

This way you define beforehand the split you plan to do in your Equations definition to help Equations focus on the right things.

Matthieu Sozeau (Jan 17 2023 at 17:45):

It might be one of the tactics taking a long time. What if you try the derive(noind, noeqns) attribute ? If it’s fast then it’s likely to be that