slow simp in rejecting Subsingleton

Stream: lean4

[Yakov Pechersky]

Minimized to be std- and mathlib-free. Consider trying to prove that the empty (fin)set is in the univ of a powerset. The simp lemma Fintype.univ_ofSubsingleton tries to fire, and spends a huge amount of time (6 seconds on my machine) struggling to show that, unfortunately, range 2 is not a subsingleton. In mathlib, it's even worse, because it then tries to do the same with IsEmpty.

namespace List

/-- There is only one list of an empty type -/
inductive Perm : List α → List α → Prop
  | nil : Perm [] []
  | cons (x : α) {l₁ l₂ : List α} : Perm l₁ l₂ → Perm (x :: l₁) (x :: l₂)
  | swap (x y : α) (l : List α) : Perm (y :: x :: l) (x :: y :: l)
  | trans {l₁ l₂ l₃ : List α} : Perm l₁ l₂ → Perm l₂ l₃ → Perm l₁ l₃

infixl:50 " ~ " => Perm

@[simp]
protected theorem Perm.refl : ∀ l : List α, l ~ l
  | [] => Perm.nil
  | x :: xs => (Perm.refl xs).cons x

protected theorem Perm.symm {l₁ l₂ : List α} (p : l₁ ~ l₂) : l₂ ~ l₁ :=
  p.rec
    .nil
    (fun x _ _ _ r₁ => .cons x r₁)
    (fun x y l => .swap y x l)
    (fun _ _ r₁ r₂ => .trans r₂ r₁)

theorem Perm.eqv (α) : Equivalence (@Perm α) :=
  ⟨Perm.refl, Perm.symm, Perm.trans⟩

instance isSetoid (α) : Setoid (List α) :=
  Setoid.mk (@Perm α) (Perm.eqv α)

variable (R : α → α → Prop)

inductive Pairwise : List α → Prop
  | nil : Pairwise []
  | cons : ∀ {a : α} {l : List α}, (∀ a', Mem a' l → R a a') → Pairwise l → Pairwise (a :: l)

def Nodup : List α → Prop := Pairwise (· ≠ ·)

def sublists (l : List α) : List (List α) :=
  let f a arr := arr.foldl (init := Array.mkEmpty (arr.size * 2))
    fun r l => (r.push l).push (a :: l)
  (l.foldr f #[[]]).toList

@[simp]
def pmap {p : α → Prop} (f : ∀ a, p a → β) : ∀ l : List α, (∀ a, Mem a l → p a) → List β
  | [], _ => []
  | a :: l, H => f a sorry :: pmap f l sorry


inductive Sublist {α} : List α → List α → Prop
  | slnil : Sublist [] []
  | cons a : Sublist l₁ l₂ → Sublist l₁ (a :: l₂)
  | cons₂ a : Sublist l₁ l₂ → Sublist (a :: l₁) (a :: l₂)

scoped infixl:50 " <+ " => Sublist
def Subperm (l₁ l₂ : List α) : Prop :=
  ∃ (l : _)(_ : l ~ l₁), l <+ l₂

infixl:50 " <+~ " => Subperm

end List

section Quot

variable {α : Sort u} {r : α → α → Prop} {motive : Quot r → Sort v}

@[elab_as_elim]
protected abbrev Quot.recOn'
    (q : Quot r)
    (f : (a : α) → motive (Quot.mk r a))
    (h : (a b : α) → (p : r a b) → Eq.ndrec (f a) (Quot.sound p) = f b)
    : motive q :=
 q.rec f h

end Quot

def Multiset.{u} (α : Type u) : Type u :=
  Quotient (List.isSetoid α)

namespace Multiset

def ofList : List α → Multiset α :=
  Quot.mk _

instance : Coe (List α) (Multiset α) :=
  ⟨ofList⟩

def Nodup (s : Multiset α) : Prop :=
  Quot.liftOn s List.Nodup fun _ _ p => propext sorry

def range (n : Nat) : Multiset Nat :=
  List.range n

def powersetAux (l : List α) : List (Multiset α) :=
  (List.sublists l).map (ofList)

def powerset (s : Multiset α) : Multiset (Multiset α) :=
  Quot.liftOn s
    (fun l => (powersetAux l : Multiset (Multiset α)))
    (fun _ _ h => Quot.sound sorry)

def Mem (a : α) (s : Multiset α) : Prop :=
  Quot.liftOn s (fun l => a ∈ l) fun l₁ l₂ (e : l₁ ~ l₂) => propext <| sorry

instance : Membership α (Multiset α) :=
  ⟨Mem⟩

nonrec def pmap {p : α → Prop} (f : ∀ a, p a → β) (s : Multiset α) : (∀ a, Mem a s → p a) → Multiset β :=
  Quot.recOn' s (fun l H => ofList (List.pmap f l H)) fun l₁ l₂ (pp : l₁ ~ l₂) =>
    funext fun H₂ : ∀ a, List.Mem a l₂ → p a =>
      have H₁ : ∀ a, List.Mem a l₁ → p a := fun a h => H₂ a sorry
      have : ∀ {s₂ e H}, @Eq.ndrec (Multiset α) l₁ (fun s => (∀ a, Mem a s → p a) → Multiset β)
          (fun _ => ofList (List.pmap f l₁ H₁)) s₂ e H = ofList (List.pmap f l₁ H₁) := by
        intro s₂ e _ ; subst e; rfl
      this.trans <| Quot.sound <| sorry

protected def Le (s t : Multiset α) : Prop :=
  (Quotient.liftOn₂ s t (· <+~ ·)) fun _ _ _ _ p₁ p₂ =>
    propext sorry

instance : LE (Multiset α) where
  le := Multiset.Le

def attach (s : Multiset α) : Multiset { x // x ∈ s } :=
  pmap Subtype.mk s fun _a => id

end Multiset

structure Finset (α : Type _) where
  val : Multiset α
  nodup : Multiset.Nodup val

namespace Finset

instance : Membership α (Finset α) :=
  ⟨fun a s => a ∈ s.1⟩

instance : LE (Finset α) :=
  ⟨fun s t => ∀ ⦃a⦄, a ∈ s → a ∈ t⟩

def range (n : Nat) : Finset Nat :=
  ⟨Multiset.range n, sorry⟩

def powerset (s : Finset α) : Finset (Finset α) :=
  ⟨(s.1.powerset.pmap Finset.mk) fun _t h => sorry, sorry⟩

instance {α : Type u} : CoeSort (Finset α) (Type u) :=
  ⟨fun s => { x // x ∈ s }⟩

def attach (s : Finset α) : Finset { x // x ∈ s } :=
  ⟨Multiset.attach s.1, sorry⟩

end Finset


section

open Function

open Nat

universe u v

variable {α β γ : Type _}

class Fintype (α : Type _) where
  elems : Finset α
  complete : ∀ x : α, x ∈ elems

namespace Finset

variable [Fintype α] {s t : Finset α}

def univ : Finset α :=
  @Fintype.elems α _

end Finset

namespace Fintype

/-- Any subsingleton type with a witness is a fintype (with one term). -/
def ofSubsingleton (a : α) [Subsingleton α] : Fintype α :=
  -- ⟨{a}, fun _ => Finset.mem_singleton.2 (Subsingleton.elim _ _)⟩
  ⟨⟨Quotient.mk' [a], sorry⟩, sorry⟩

@[simp]
theorem univ_ofSubsingleton (a : α) [Subsingleton α] : @Finset.univ _ (ofSubsingleton a) = ⟨Quotient.mk' [a], sorry⟩ :=
  rfl

end Fintype

instance Finset.fintypeCoeSort {α : Type u} (s : Finset α) : Fintype s :=
  ⟨s.attach, sorry⟩

end Finset

set_option autoImplicit false
#check (⟨⟨Quotient.mk' [], sorry⟩, sorry⟩ : (Finset.range 2).powerset)

set_option trace.profiler true
theorem foo : ⟨⟨Quotient.mk' [], sorry⟩, sorry⟩ ∈
    (Finset.univ : Finset ((Finset.range 2).powerset)) := by
  simp (config := {
    maxSteps := 100
    maxDischargeDepth := 1
    contextual := false
    memoize := false
    singlePass := false
    zeta := false
    beta := false
    eta := false
    etaStruct := .none
    iota := false
    proj := false
    decide := false
    arith := false
    autoUnfold := false
    dsimp := false
  }) -- if this line, Fintype.univ_ofSubsingleton fires, and is slow (6 s on my computer)
  -- }) [-Fintype.univ_ofSubsingleton]
  sorry

[Yakov Pechersky]

This is the unification step that is slow:

[7.749492s] ❌ [?a] =?= List.pmap Subtype.mk
                                          (List.pmap Finset.mk (Multiset.powersetAux (List.range 2))
                                            (_ :
                                              ∀ (_t : Multiset Nat),
                                                Multiset.Mem _t (Multiset.powerset (Finset.range 2).val) →
                                                  Multiset.Nodup _t))
                                          (_ :
                                            ∀ (_a : Finset Nat),
                                              Multiset.Mem _a (Finset.powerset (Finset.range 2)).val →
                                                Multiset.Mem _a (Finset.powerset (Finset.range 2)).val)

[Kevin Buzzard]

Congratulations on finally minimising this monster!

[Yakov Pechersky]

Even smaller, with no references to any quotients, only lists. Still 1.5 s

class Fintype (α : Type _) where
  elems : List α
  complete : ∀ x : α, x ∈ elems

namespace List

def sublists (l : List α) : List (List α) :=
  let f a arr := arr.foldl (init := Array.mkEmpty (arr.size * 2))
    fun r l => (r.push l).push (a :: l)
  (l.foldr f #[[]]).toList

@[simp]
def pmap {p : α → Prop} (f : ∀ a, p a → β) : ∀ l : List α, (∀ a, Mem a l → p a) → List β
  | [], _ => []
  | a :: l, H => f a sorry :: pmap f l sorry

def attach (s : List α) : List { x // x ∈ s } :=
  pmap Subtype.mk s fun _a => id

@[simp]
theorem mem_attach (l : List α) : ∀ x, x ∈ l.attach
  | ⟨a, h⟩ => sorry

instance {α : Type u} : CoeSort (List α) (Type u) :=
  ⟨fun s => { x // x ∈ s }⟩

variable [Fintype α]

def univ : List α :=
  @Fintype.elems α _

end List

namespace Fintype

/-- Any subsingleton type with a witness is a fintype (with one term). -/
def ofSubsingleton (a : α) [Subsingleton α] : Fintype α :=
  ⟨[a], fun x => by
    rw [Subsingleton.elim x a]
    exact List.Mem.head []⟩

@[simp]
theorem univ_ofSubsingleton (a : α) [Subsingleton α] : @List.univ _ (ofSubsingleton a) = [a] := rfl

end Fintype

instance List.fintypeCoeSort {α : Type u} (s : List α) : Fintype s :=
  ⟨s.attach, mem_attach _⟩

set_option autoImplicit false
#check (⟨[], sorry⟩ : (List.range 2).sublists)

set_option trace.profiler true
theorem foo : ⟨[], sorry⟩ ∈
    (List.univ : List ((List.range 2).sublists)) := by
  simp (config := {
    maxSteps := 100
    maxDischargeDepth := 1
    contextual := false
    memoize := false
    singlePass := false
    zeta := false
    beta := false
    eta := false
    etaStruct := .none
    iota := false
    proj := false
    decide := false
    arith := false
    autoUnfold := false
    dsimp := false
  }) -- if this line, Fintype.univ_ofSubsingleton fires, and is slow (1.5 s on my computer)
  -- }) [-Fintype.univ_ofSubsingleton]
  sorry

[Yakov Pechersky]

Is it that just that univ_ofSubsingleton is a bad simp lemma?

[Scott Morrison]

With set_option trace.Meta.isDefEq true in we get a bit more useful information.

[?a] =?= List.pmap Subtype.mk (List.sublists (List.range 2))
              (_ :
                ∀ (_a : List Nat),
                  List.Mem _a (List.sublists (List.range 2)) → List.Mem _a (List.sublists (List.range 2)))

is taking all the time, but mysteriously its children (where it successfully unifies ?a with the head of the RHS, and then fails to unify [] with the tail of the RHS) are fast. I'm not sure where the time is being sucked up.