1+1 = 2

Stream: mathlib4

[Ruben Van de Velde]

What typeclasses do we need in mathlib4 to prove that 1+1 is 2? It only needs has_one and has_add in mathlib3, but it seems like that doesn't work anymore

[Mario Carneiro]

that depends on what you mean by 1, and +, and 2 :)

[Yaël Dillies]

Probably whatever we currently need for docs#nat.cast_add

[Mario Carneiro]

instance [Add α] [OfNat α 1] : OfNat α 2 := ⟨1 + 1⟩
example [Add α] [OfNat α 1] : 1 + 1 = 2 := rfl

look ma, no semirings

[Mario Carneiro]

The usual class expected by norm_num to handle numeral terms sensibly is AddMonoidWithOne

[Ruben Van de Velde]

Okay, AddMonoidWithOne works - but now for two_mul [has_add α] [mul_one_class α] [right_distrib_class α] : 2 * n = n + n I need to combine it with something that also implies 1 * n = n

[Ruben Van de Velde]

(this is for mathib4#655, btw)

[Mario Carneiro]

that looks like a semiring theorem

[Moritz Doll]

less cheating than Mario's version:

import Mathlib.Data.Nat.Cast.Defs

example [One α] [AddZeroClass α] : (1 : α) + 1 = (2 : ℕ).unaryCast := by
  change 1 + 1 = (0 + 1) + 1
  rw [zero_add 1]

[Moritz Doll]

oh no, I actually might need to add this lemma to mathlib (for mathlib4#664)