norm_num for non-semirings

Stream: mathlib4

[Alex J. Best]

Given the new way numerals work in lean 4 it seems to me that goals like 1 + 2 = 3 now make sense and are true in an arbitrary AddMonoidWithOne.
To me this looks in scope for norm_num (though norm_cast works here for now), but it seems norm_num can't currently handle them.
@Mario Carneiro do you think that norm_num should do this? And how hard would it be to extend/modify it to do so?

[Kevin Buzzard]

You don't even want to assume commutativity of addition in your base monoid? Is that really norm_num's job? Maybe...

[Mario Carneiro]

norm_num might be able to handle these, as long as all of the theorems are true for the same typeclass it doesn't matter too much what it is

[Mario Carneiro]

The main theorems we need are Nat.cast_add and Nat.cast_mul

[Mario Carneiro]

...hm, cast_mul is an issue for AddMonoidWithOne

[Gabriel Ebner]

Where does cast_mul come into play here?

[Mario Carneiro]

in the proof of multiplication

[Mario Carneiro]

Actually it wasn't so bad. You have to assume Semiring for multiplication but we already do a similar thing for negation

[Mario Carneiro]

so yes, this works now

section
  variable (α : Type u) [AddMonoidWithOne α]
  example : (1 + 0 : α) = (0 + 1 : α) := by norm_num
  example : (0 + (2 + 3) + 1 : α) = 6 := by norm_num
end