Mul.mul does not match operator for rewriting

Stream: lean4

[David A]

I was playing around with Agda-style definitions for algebraic properties, like

variable (α : Type u)
def Op₂ := α → α → α
def IsCommutative {α} (op : Op₂ α) := (a b : α) → op a b = op b a

class CommMagma extends Mul α where
  mul_comm : IsCommutative mul

However, mul_comm cannot be used to rewrite because Mul.mul a b doesn't match a * b. A standalone minimal repro of the issue is:

example (a b : Nat) (h : Mul.mul a b = 2) : a * b + a * b = 4 :=
  by rw [h]

Replacing the function with HMul.hMul does work; even in the full class example. I think the problem is that Mul.mul is not definitionally equal to HMul.hMul, and/or that the instance for Nat isn't reducible, or maybe the definition isn't reducible, idk.

Is there any solution for this other than redefining the operators to use the Mul typeclass? In particular what I want to get working is to be able to refer to the operation as mul (or some other short term that correctly supplies the α needed by the elaborator) in the class field types, but have this still rewrite the symbolic operator.

[Henrik Böving]

a * b is always implemented as HMul as you noticed correctly, however usually we have a default instance that uses Mul.mul instead so what you can do is:

example (a b : Nat) (h : Mul.mul a b = 2) : a * b + a * b = 4 :=
  by simp [HMul.hMul, h]

[David A]

Unfortunately that would not be very practical in more complex situations.

I found an interesting minimal pair for this issue. This rewrite fails:

def IsCommutative {α} (op : Op₂ α) := (a b : α) → op a b = op b a

variable (α)

class Magma extends HMul α α α where

abbrev Magma.mul [Magma α] : α → α → α := Magma.toHMul.1

class CommMagma extends Magma α where
  mul_comm : IsCommutative toMagma.mul

example [CommMagma α] (a b c : α) : a * b * c = b * a * c :=
  by rw [CommMagma.mul_comm a b]

But if I inline the abbrev, the rewrite succeeds:

  mul_comm : IsCommutative toMagma.toHMul.hMul

That is very counter-intuitive to me as I thought rewrites should not be sensitive to the presence of reducible names.

[Henrik Böving]

I don't think rewrites will (or should) automatically unfold definitions when they are searching for the pattern to apply their theorem to? The point of rewrite to me has always been that you can explicitly control such stuff.