Zulip Chat Archive

Stream: new members

Topic: simp on has_coe_to_fun


Akaho Akane (Nov 03 2022 at 13:58):

I am trying to define a homomorphism-like structure, but using has_coe_to_fun makes the simp tactic very slow (especially when there are many symbols).

Example :

@[notation_class] class has_add₁ (α : Type*) := (add : α  α  α)
@[notation_class] class has_add₂ (α : Type*) := (add : α  α  α)
@[notation_class] class has_add₃ (α : Type*) := (add : α  α  α)
@[notation_class] class has_add₄ (α : Type*) := (add : α  α  α)

infix ` +₁ `:60 := has_add₁.add
infix ` +₂ `:60 := has_add₂.add
infix ` +₃ `:60 := has_add₃.add
infix ` +₄ `:60 := has_add₄.add

variables (α : Type*) (β : Type*) (γ : Type*)
  [has_add₁ α] [has_add₁ β] [has_add₁ γ]
  [has_add₂ α] [has_add₂ β] [has_add₂ γ]
  [has_add₃ α] [has_add₃ β] [has_add₃ γ]
  [has_add₄ α] [has_add₄ β] [has_add₄ γ]

structure hom :=
(to_fun : α  β)
(map_add₁' :  a b, to_fun (a +₁ b) = to_fun a +₁ to_fun b)
(map_add₂' :  a b, to_fun (a +₂ b) = to_fun a +₂ to_fun b)
(map_add₃' :  a b, to_fun (a +₃ b) = to_fun a +₃ to_fun b)
(map_add₄' :  a b, to_fun (a +₄ b) = to_fun a +₄ to_fun b)

namespace hom

instance : has_coe_to_fun (hom α β) (λ _, α  β) := hom.to_fun

variables {α} {β} {γ} (f₁ : hom β γ) (f f₂ : hom α β)

lemma to_fun_eq (a) : f.to_fun a = f a := rfl

def comp : hom α γ :=
{ to_fun := f₁.to_fun  f₂.to_fun,
  map_add₁' := by simp[f₁.map_add₁', f₂.map_add₁'],
  map_add₂' := by simp[f₁.map_add₂', f₂.map_add₂'],
  map_add₃' := by simp[f₁.map_add₃', f₂.map_add₃'],
  map_add₄' := by simp[f₁.map_add₄', f₂.map_add₄'] }

@[simp] lemma map_add₁ :  a b, f (a +₁ b) = f a +₁ f b := hom.map_add₁' _
@[simp] lemma map_add₂ :  a b, f (a +₂ b) = f a +₂ f b := hom.map_add₂' _
@[simp] lemma map_add₃ :  a b, f (a +₃ b) = f a +₃ f b := hom.map_add₃' _
@[simp] lemma map_add₄ :  a b, f (a +₄ b) = f a +₄ f b := hom.map_add₄' _

def comp' : hom α γ :=
{ to_fun := f₁.to_fun  f₂.to_fun,
  map_add₁' := by simp[to_fun_eq],
  map_add₂' := by simp[to_fun_eq],
  map_add₃' := by simp[to_fun_eq],
  map_add₄' := by simp[to_fun_eq] }

end hom

In this example, comp' is much slower than comp. How can I deal with these problems?

Eric Wieser (Nov 03 2022 at 17:44):

I'd write comp' with f₁ ∘ f₂ instead, but I see the same behavior; set_option profiler true reports a 5x difference for me.

Eric Wieser (Nov 03 2022 at 17:46):

Even putting @[simp] on to_fun_eq is enough to slow down the first version just as much


Last updated: Dec 20 2023 at 11:08 UTC