tpil_ch8.lean

namespace hidden

open nat (zero succ)

def add : ℕ → ℕ → ℕ
| n zero        := n
| n (succ m) := succ (add n m)

set_option trace.app_builder true

@[simp]
theorem succ_both_sides {n m : ℕ} (h : n = m) : succ n = succ m :=
by rw h

@[simp]
theorem add_zero (n : ℕ) : add n zero = n := rfl
@[simp]
theorem add_of_of_succ (n m : ℕ) : add n (succ m) = succ (add n m) := rfl

@[simp]
theorem zero_add : Π (n : ℕ), add zero n = n
| zero := rfl
| (succ n) := by simp [zero_add n]

@[simp]
theorem add_of_succ_of : Π (n m : ℕ), add (succ n) m = succ (add n m)
| n zero := by simp
| n (succ m) := by simp [add_of_succ_of n m]

@[simp]
theorem add_comm : Π (n m : ℕ), add n m = add m n
| n zero := by simp
| n (succ m) := by simp [add_comm n m]

@[simp]
theorem add_assoc : Π (a b c : ℕ), add a (add b c) = add (add a b) c
| zero b c := by simp
| (succ a) b c := by simp [add_assoc a b c]

def mul : ℕ → ℕ → ℕ
| n zero     := zero
| n (succ m) := add n (mul n m)

@[simp]
theorem mul_zero (n : ℕ) : mul n zero = zero := rfl
@[simp]
theorem mul_one (n : ℕ) : mul n 1 = n := rfl

@[simp]
theorem mul_of_of_succ (n m : ℕ) : mul n (succ m) = add n (mul n m) := rfl
@[simp]
theorem zero_mul : Π (n : ℕ), mul zero n = zero
| zero := by simp
| (succ n) := by simp [zero_mul n]

@[simp]
theorem mul_of_succ_of : Π (n m : ℕ), mul (succ n) m = add m (mul n m)
| n zero := by simp
| n (succ m) := by simp [mul_of_succ_of n m]

@[simp]
theorem mul_comm : Π (a b : ℕ), mul a b = mul b a
| n zero := by simp
| n (succ m) := by simp [mul_comm n m]

@[simp]
theorem mul_over_add : Π (a b c : ℕ), mul (add a b) c = add (mul a c) (mul b c)
| a b zero := by simp
| a b (succ c) := begin
simp only [mul_of_of_succ],
simp only [mul_over_add a b c],
simp only [add_assoc],
simp only [add_comm],
rw add_comm a b,
rw ← add_assoc,
end
end hidden