natural_number_game.lean

-- https://www.ma.imperial.ac.uk/~buzzard/xena/natural_number_game/

-- 1. TUTORIAL
-- world=1&level=1 "using refl"
example : forall x : Nat, x = x := by
  intro x
  exact Eq.refl x

-- world=1&level=2 "using rw"
example
  (x y : Nat)
  (h₁ : y = x + 7)
:
  2 * y = 2 * (x + 7)
:= by
  rw [h₁]

-- world=1&level=3 "using succ"
example
  (a b : Nat)
  (h₁ : b = Nat.succ a)
:
  (Nat.succ (Nat.succ a)) = (Nat.succ b)
:= by
  rw [h₁]

-- world=1&level=4 "reusing proof"
theorem add_succ
  (a d : Nat)
:
  a + Nat.succ d = Nat.succ (a + d)
:= by rfl
  
example
  (a : Nat)
:
  a + Nat.succ 0 = Nat.succ a
:= by
  rw [add_succ]

-- 2. ADDITION
-- world=2&level=1 "induction"
theorem zero_add
  (n: Nat)
:
  0 + n = n
:= by
  induction n with
  | zero => rfl
  | succ n' hn' =>
    rw [add_succ]
    rw [hn']

-- world=2&level=2 "induction practice"
theorem add_assoc
  (a b c : Nat)
:
  (a + b) + c = a + (b + c)
:= by
  induction c with
  | zero => rfl
  | succ c' hc' =>
    rw [add_succ]
    rw [hc']
    rfl

-- world=2&level=3 "induction practice"
theorem succ_add
  (a b : Nat)
:
  (Nat.succ a) + b = Nat.succ (a + b)
:= by
  rw [← add_succ]
  induction b with
  | zero => rfl
  | succ b' hb' =>
    rw [add_succ]
    rw [hb']
    rfl

-- world=2&level=4 "induction practice"
theorem add_comm
  (a b : Nat)
:
  a + b = b + a
:= by
  induction a with
  | zero => rw [zero_add]; rfl
  | succ a' ha' =>
    rw [succ_add]
    rw [add_succ, ha']
    
-- world=2&level=5 "useful theorems involving 1"
theorem one_eq_succ_zero : 1 = Nat.succ 0 := by rfl
theorem succ_eq_add_one
  (n : Nat)
:
  Nat.succ n = n + 1
:= by rfl

-- world=2&level=6 "specific rw"
theorem add_right_comm
  (a b c : Nat)
:
  (a + b) + c = a + c + b
:= by
  rw [add_comm a b]
  rw [add_assoc]
  rw [add_comm]