simp on has_coe_to_fun

Stream: new members

[Akaho Akane]

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]

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]

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