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 `funelim`

s.

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.

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

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

And yet, Coq's fine with that.

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

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 ?

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

Have you looked at views?

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

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

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