Stream: Equations devs & users

Topic: funelim slow


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

view this post on Zulip Alexander Gryzlov (Aug 09 2022 at 14:27):

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

view this post on Zulip 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: Jan 29 2023 at 16:02 UTC