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

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

sometimes

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