Peano numbers in Lean

Peano.lean

/-
# Peano numbers in Lean

Proof that the set of natural numbers under ordinary addition and multiplication
is a commutative semiring using the Peano numbers.

- Peano axioms - Wikipedia: https://en.wikipedia.org/wiki/Peano_axioms
- Semiring - Wikipedia: https://en.wikipedia.org/wiki/Semiring
- Proofs involving the addition of natural numbers - Wikipedia:
  https://en.wikipedia.org/wiki/Proofs_involving_the_addition_of_natural_numbers
-/

inductive Peano : Type
| _0 : Peano
| S : Peano → Peano

open Peano

def _1 := S _0
def _2 := S _1


/-
## Addition
-/

instance : Add Peano where
  add a b := _add a b where
    _add a b := match b with
      | _0 => a
      | S b' => S (_add a b')

theorem one_plus_one_eq_two : _1 + _1 = _2 := by -- no need for 379 pages :)
  calc
    _1 + _1 = S _0 + S _0   := by rfl
    _       = S (S _0 + _0) := by rfl
    _       = S (S _0)      := by rfl
    _       = S _1          := by rfl
    _       = _2            := by rfl

@[simp]
theorem add_associativity (a b c : Peano)
  : (a + b) + c = a + (b + c) := by
    induction c with
    | _0 => rfl
    | S c' ih => calc
      a + b + S c' = S (a + b + c')   := by rfl
      _            = S (a + (b + c')) := by rw [ih]
      _            = a + (b + S c')   := by rfl

@[simp]
theorem right_add_identity (a : Peano) : a + _0 = a := by
  rfl

@[simp]
theorem left_add_identity (a : Peano) : _0 + a = a := by
  induction a with
  | _0 => rfl
  | S a' ih => calc
    _0 + S a' = S (_0 + a') := by rfl
    _         = S a'        := by rw [ih]

@[simp]
theorem add_commutativity_1 (a : Peano) : a + _1 = _1 + a := by
  induction a with
  | _0 => rfl
  | S a' ih => calc
    S a' + _1 = S (a' + _1) := by rfl
    _         = S (_1 + a') := by rw [ih]
    _         = _1 + S a'   := by rfl

@[simp]
theorem add_commutativity (a b : Peano) : a + b = b + a := by
  induction b with
  | _0 => simp
  | S b' ih => calc
    a + S b' = a + b' + _1 := by rfl
    _        = b' + _1 + a := by simp [ih]
    _        = S b' + a    := by rfl


/-
## Multiplication
-/

instance : Mul Peano where
  mul a b := _mul a b where
    _mul a b := match b with
      | _0 => _0
      | S b' => a + _mul a b'

@[simp]
theorem right_mul_identity (a : Peano) : a * _1 = a := by
  rfl

@[simp]
theorem left_mul_identity (a : Peano) : _1 * a = a := by
  induction a with
  | _0 => rfl
  | S a' ih => calc
    _1 * S a' = _1 + _1 * a' := by rfl
    _         = a' + _1      := by rw [ih, add_commutativity]

@[simp]
theorem right_mul_annihilating (a : Peano) : a * _0 = _0 := by
  rfl

@[simp]
theorem left_mul_annihilating (a : Peano) : _0 * a = _0 := by
  induction a with
  | _0 => rfl
  | S a' ih => calc
    _0 * S a' = _0 + _0 * a' := by rfl
    _         = _0 + _0      := by rw [ih]
    _         = _0           := by rfl

@[simp]
theorem right_mul_distributivity (a b c : Peano)
  : (b + c) * a = b * a + c * a := by
    induction a with
    | _0 => simp
    | S a' ih => calc
      (b + c) * S a' = (b + c) + (b + c) * a'      := by rfl
      _              = b + (b * a' + c + c * a')   := by simp [ih]
      _              = (b + b * a') + (c + c * a') := by repeat (rw [add_associativity])
      _              = b * S a' + c * S a'         := by rfl

@[simp]
theorem left_mul_distributivity (a b c : Peano) : a * (b + c) = a * b + a * c := by
  induction a with
  | _0 => simp
  | S a' ih => calc S a' * (b + c)
      = (a' + _1) * (b + c) := by rfl
    _ = a' * (b + c) + _1 * (b + c) := by rw [right_mul_distributivity]
    _ = a' * (b + c) + b + c := by rw [left_mul_identity, add_associativity]
    _ = b + a' * b + c + a' * c := by simp [ih]
    _ = (_1 + a') * b + (_1 + a') * c := by simp only [left_mul_identity, right_mul_distributivity, add_associativity]
    _ = S a' * b + S a' * c := by simp only [add_commutativity]; rfl

@[simp]
theorem mul_associativity (a b c : Peano) : (a * b) * c = a * (b * c) := by
  induction c with
  | _0 => rfl
  | S c' ih => calc
    a * b * S c' = a * b + a * b * c' := by rfl
    _            = a * (b + b * c')   := by simp [ih]
    _            = a * (b * S c')     := by rfl

@[simp]
theorem mul_commutativity (a b: Peano) : a * b = b * a := by
  induction b with
  | _0 => simp
  | S b' ih => calc
    a * S b' = a * (b' + _1)   := by rfl
    _        = a * b' + a * _1 := by rw [left_mul_distributivity]
    _        = _1 * a + b' * a := by simp [ih]
    _        = (b' + _1) * a   := by rw [right_mul_distributivity, add_commutativity]