optimal instance design for structure wrappers

Stream: lean4

[Matthew Ballard]

See the example below. Are there any advantages to the foo instance over bar? (Edited to focus on automation)

universe u

variable (α : Type u) [Add α]

class AddSemigroup (α : Type u) extends Add α where
  add_assoc : ∀ (a b c : α), a + b + c = a + (b + c)

structure Wrapper (α : Type u) where
  val : α

namespace Foo

scoped instance foo : Add (Wrapper α) where
  add x y := ⟨x.val + y.val⟩

end Foo

namespace Bar

scoped instance bar : Add (Wrapper α) where
  add := fun ⟨x⟩ ⟨y⟩ => ⟨x + y⟩

end Bar

section

open Foo AddSemigroup

variable (β : Type u) [AddSemigroup β]

instance : AddSemigroup (Wrapper β) where
  add_assoc a b c := congrArg Wrapper.mk (by
    fail_if_success simp [add_assoc] -- no good
    sorry)

end

section

open Bar AddSemigroup

variable (β : Type u) [AddSemigroup β]

instance : AddSemigroup (Wrapper β) where
  add_assoc _ _ _ := congrArg Wrapper.mk (by
    simp [add_assoc]) -- tots good
end

[Matthew Ballard]

Here are each #printed

def Foo.foo.{u} : (α : Type u) → [inst : Add α] → Add (Wrapper α) :=
fun α [Add α] => { add := fun x y => { val := x.val + y.val } }

def Bar.bar.{u} : (α : Type u) → [inst : Add α] → Add (Wrapper α) :=
fun α [Add α] =>
  {
    add := fun x x_1 =>
      match x with
      | { val := x } =>
        match x_1 with
        | { val := y } => { val := x + y } }

[Matthew Ballard]

The term

add_assoc _ _ _ := congrArg Wrapper.mk <| add_assoc _ _ _

is fine for both for comparison

[James Gallicchio]

wait, it's actually very interesting/surprising to me that they behave differently here. it seems to me like simp is unfolding the wrapper + when it is the term being inspected by a match, but not when it is a term on which you're calling .val?

[James Gallicchio]

(not sure how relevant this is, but forcing Lean to unify everything Just Works:tm: for both variants)

instance : AddSemigroup (Wrapper β) where
  add_assoc a b c := congrArg Wrapper.mk (add_assoc ..)

[Eric Wieser]

simp is irrelevant here, the unfolding is caused by the congrArg

[Eric Wieser]

Once you write the lemmas that distribute val, the two cases end up equivalent:

universe u

variable (α : Type u) [Add α]

class AddSemigroup (α : Type u) extends Add α where
  add_assoc : ∀ (a b c : α), a + b + c = a + (b + c)

structure Wrapper (α : Type u) where
  val : α

namespace Foo

scoped instance foo : Add (Wrapper α) where
  add x y := ⟨x.val + y.val⟩

-- `simps` can generate this
@[simp] theorem val_add (x y : Wrapper α) : (x + y).val = x.val + y.val := rfl

end Foo

namespace Bar

scoped instance bar : Add (Wrapper α) where
  add := fun ⟨x⟩ ⟨y⟩ => ⟨x + y⟩

-- `simps` can generate this
@[simp] theorem val_add (x y : Wrapper α) : (x + y).val = x.val + y.val := rfl

end Bar

section

open Foo AddSemigroup

variable (β : Type u) [AddSemigroup β]

instance : AddSemigroup (Wrapper β) where
  add_assoc a b c := congrArg Wrapper.mk (by
    simp [add_assoc]) -- fine

end

section

open Bar AddSemigroup

variable (β : Type u) [AddSemigroup β]

instance : AddSemigroup (Wrapper β) where
  add_assoc a b c := congrArg Wrapper.mk (by
    simp [add_assoc]) -- fine
end