James Wood (Aug 09 2022 at 09:22): 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.
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: May 28 2023 at 18:29 UTC