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

[Filippo A. E. Nuccio]

I cannot find in this thread an answer to @Kim Morrison 's question about "how is one meant to handle this". Is there any advance? For instance, in

import Mathlib.GroupTheory.Subgroup.Center

example : Monoid Bool where
  mul := Bool.and
  mul_assoc := by
    intro x y z
    exact Bool.and_assoc ..
  one := true
  one_mul := by
    intro t
    have := Bool.true_and t
    exact this
  mul_one := Bool.and_true

in the second field (mul_assoc) after the three intro I would like to change * to & so that I can realize what lemma to apply (of course in this mwe things are too easy, but if the first field mul was "difficult" it can be handy to be able to "unfold" it).

[Kevin Buzzard]

When I've been in this situation (eg when teaching) I've defined the Mul instance first and written a mul_def lemma, then when making the monoid instance I've written mul := (. * .) (or left it out) and then rewritten mul_def in the proofs

[Filippo A. E. Nuccio]

Yes, I agree that this is the best way out, but I was hoping to be able to work inside the def (and yes, this also comes from teaching needs).

[Kyle Miller]

unfold_projs seems to work here

[Ruben Van de Velde]

Hmm, I had the impression this was no longer an issue, but maybe I'm confused

[Filippo A. E. Nuccio]

Kyle Miller said:

unfold_projs seems to work here

Thanks!

[Riccardo Brasca]

Also dsimp [HMul.hMul] works.