Stream: Equations devs & users

Topic: Coq equtions is very very slow


view this post on Zulip walker (Jan 17 2023 at 13:11):

So I have a functions that looks like this :

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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Paolo Giarrusso (Jan 17 2023 at 13:52):

And yet, Coq's fine with that.

view this post on Zulip Paolo Giarrusso (Jan 17 2023 at 13:54):

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

view this post on Zulip 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 ?

view this post on Zulip walker (Jan 17 2023 at 13:58):

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

view this post on Zulip Théo Winterhalter (Jan 17 2023 at 13:59):

Have you looked at views?

view this post on Zulip Théo Winterhalter (Jan 17 2023 at 13:59):

https://mattam82.github.io/Coq-Equations/examples/Examples.views.html

view this post on Zulip 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.

view this post on Zulip 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


Last updated: Apr 21 2024 at 01:02 UTC