unfolding earlier fields

Stream: lean4

[Scott Morrison]

In lean3 I could write:

import algebra.group.defs

def bar (a b : nat) : nat := a * b

@[simp]
lemma foo (a b : nat) : bar a b = a * b := rfl

instance : add_semigroup nat :=
{ add := bar,
  add_assoc := λ f g h,
  begin
    simp, -- `+` has changed to `*`
    sorry
  end }

but in lean4:

import Mathlib.Algebra.Group.Basic

def bar (a b : Nat) : Nat := a * b

@[simp]
lemma foo (a b : Nat) : bar a b = a * b := rfl

instance : AddSemigroup Nat :=
{ add := bar,
  add_assoc := fun f g h => by
    simp -- Nothing happens: `foo` doesn't fire
    sorry }

How is one meant to handle this?

[Gabriel Ebner]

Ooh, I think that's because + is now HAdd.hAdd so there's the indirection HAdd->Add->AddSemigroup which breaks the unfolding here.

[Gabriel Ebner]

I'd do: I wouldn't ever declare an incompatible addition instance for Nat like this:

instance : Add Nat where
  add := bar

theorem Nat.add_def {x y : Nat} : x + y = bar x y := rfl