## Stream: Equations devs & users

### Topic: funelim slow

#### James Wood (Aug 09 2022 at 09:22):

I'm noticing that, in cases where I'm doing a lot of dependent pattern matching, `funelim` is much slower than doing the equivalent destructions manually. For example, in the following, the `funelim` line takes 2 or 3 seconds to step over interactively. I think `apply_funelim` in the same position is much quicker, so the slowness must be in the extra stuff `funelim` does. Could someone explain a bit what's slow, whether it's inherently slow, and whether there are some best practices or workarounds to avoid such delays?

``````From Equations Require Import Equations.
Set Equations Transparent.
Require Import List.
Import ListNotations.

Equations sum_map {A B A' B' : Set} :
(A -> A') -> (B -> B') -> (A + B -> A' + B') :=
| f, g, inl x => inl (f x)
| f, g, inr y => inr (g y).

Section interleaving.
Context {A : Set}.

Inductive interleaving : forall (xs ys zs : list A), Set :=
| inil : interleaving nil nil nil
| lcons {z xs ys zs} : interleaving xs ys zs -> interleaving (z :: xs) ys (z :: zs)
| rcons {z xs ys zs} : interleaving xs ys zs -> interleaving xs (z :: ys) (z :: zs)
.

Inductive any {T : A -> Set} : list A -> Set :=
| here {x xs} : T x -> any (x :: xs)
| there {x xs} : any xs -> any (x :: xs)
.
Arguments any T xs : clear implicits.

Equations any_interleaving {T} {xs ys zs : list A} :
interleaving xs ys zs -> any T zs -> any T xs + any T ys :=
| lcons i, here t => inl (here t)
| rcons i, here t => inr (here t)
| lcons i, there e => sum_map there id (any_interleaving i e)
| rcons i, there e => sum_map id there (any_interleaving i e)
.

Equations ll_any_interleaving {T} {xs ys zs : list A} :
interleaving xs ys zs -> any T xs -> any T zs :=
| lcons i, here t => here t
| lcons i, there f => there (ll_any_interleaving i f)
| rcons i, f => there (ll_any_interleaving i f).

Lemma ll_any_interleaving_beta {T} {xs ys zs : list A}
(i : interleaving xs ys zs) (f : any T xs) :
any_interleaving i (ll_any_interleaving i f) = inl f.
Proof.
funelim (ll_any_interleaving i f).
- reflexivity.
- cbn.
rewrite-> H.
reflexivity.
- cbn.
rewrite-> H.
reflexivity.
Qed.

End interleaving.
``````

#### Alexander Gryzlov (Aug 09 2022 at 14:27):

Yeah I've also had to fall back on `apply_funelim` sometimes

#### Matthieu Sozeau (Aug 11 2022 at 10:16):

Indeed, `funelim` is not very optimized so in cases your induction does not need any generalization (e.g. when the call to eliminate is on distinct variables), `apply_funelim` will perform better. The slowness is due to doing a lot of substitutions/noconfusion steps, building some big proof terms. There might be other issues explaining the slowness, like applying unecessary reductions in the tactics but I couldn't spot a particular culprit last time I looked.

Last updated: Nov 29 2023 at 05:01 UTC