Commutative and Associative Laws of Addition in Lean

We will prove the commutativity and associativity of addition.

Both commutativity and associativity can be proved using mathematical induction and simp.

-- Commutativity of addition
theorem MyNat.add_comm (m n : MyNat) : m + n = n + m := by
  induction n with
  | zero => simp [ctor_eq_zero]
  | succ n ih =>
    simp [ih]

-- Associativity of addition
theorem MyNat.Int.add_assoc (l m n : MyNat) : l + m + n = l + (m + n) := by
  induction n with
  | zero => rfl
  | succ n ih =>
    simp [ih]

To use commutativity and associativity in a proof, you must specify what they should be applied to.

example (l m n : MyNat) : l + m + n + 3 = m + (l + n) + 3 := calc
  _ = m + l + n + 3 := by rw [MyNat.add_comm l m]
  _ = m + (l + n) + 3 := by rw [MyNat.add_assoc m l n]

However, by registering these properties for the standard library operations as shown below, you can prove the identity using the ac_rfl tactic.

instance : Std.Associative (α := MyNat) (. + .) where
  assoc := MyNat.add_assoc

instance : Std.Commutative (α := MyNat) (. + .) where
  comm := MyNat.add_comm

example (l m n : MyNat) : l + m + n + 3 = m + (l + n) + 3 := by
  ac_rfl