module Nat where
open import Equality

-- ----------------------------------------------------------------------
-- * The natural numbers

data ℕ : Set where
  zero : ℕ
  succ : ℕ -> ℕ

{-# BUILTIN NATURAL ℕ #-}

infixl 7 _+_

-- ----------------------------------------------------------------------
-- ** Addition

_+_ : ℕ -> ℕ -> ℕ
zero + y = y
(succ x) + y = succ (x + y)

lemma-add-assoc : ∀ (x y z : ℕ) -> (x + y) + z ==  x + (y + z)
lemma-add-assoc zero y z = refl
lemma-add-assoc (succ x) y z = context succ (lemma-add-assoc x y z)

lemma-add-one :  ∀ (n : ℕ) -> n + (succ zero) == succ n
lemma-add-one zero = refl
lemma-add-one (succ n) = context succ (lemma-add-one n)

lemma-add-m-zero : ∀ (m : ℕ) -> m == m + zero
lemma-add-m-zero zero = refl
lemma-add-m-zero (succ m) = context succ ind-hyp
  where
    ind-hyp : m == m + zero
    ind-hyp = lemma-add-m-zero m

lemma-add-succ : ∀ (m n : ℕ) -> succ (m + n) == m + (succ n)
lemma-add-succ zero n = refl
lemma-add-succ (succ m) n = context succ (lemma-add-succ m n)

lemma-add-commutative : ∀ (n : ℕ) -> ∀ (m : ℕ) -> n + m == m + n
lemma-add-commutative zero m = lemma-add-m-zero m
lemma-add-commutative (succ n) m =
  equational succ (n + m)
          by context succ (lemma-add-commutative n m)
      equals succ (m + n)
          by lemma-add-succ m n
      equals m + (succ n)

-- ----------------------------------------------------------------------
-- ** Multiplication

infixl 9 _*_

_*_ : ℕ -> ℕ -> ℕ
zero * m = zero
succ n * m = n * m + m

lemma-mult-zero : ∀ (n : ℕ) ->  n * zero == zero
lemma-mult-zero zero = refl
lemma-mult-zero (succ n) = trans step1 step2
  where
    step1 :  (n * zero) + zero == zero + zero
    step1 = context (λ [-] →  [-] + zero) (lemma-mult-zero n)

    step2 : zero + zero == zero
    step2 = refl

lemma-assoc2 : ∀ a b c d -> (a + b) + (c + d) == (a + c) + (b + d)
lemma-assoc2 a b c d =
  equational (a + b) + (c + d)
    by lemma-add-assoc a b (c + d) 
  equals a + (b + (c + d))
   by  context (\ x -> a + x) (symm (lemma-add-assoc b c d)) 
  equals a + ((b + c) + d)
    by context (\ x -> a + (x + d)) (lemma-add-commutative  b c) 
  equals a + ((c + b) + d)
    by context (\ x -> a + x) (lemma-add-assoc c b d) 
  equals a + (c + (b + d))
    by symm (lemma-add-assoc a c (b + d)) 
  equals (a + c) + (b + d)

lemma-assoc3 : ∀ a b c -> (a + b) + c == (a + c) + b
lemma-assoc3 zero b c = lemma-add-commutative b c
lemma-assoc3 (succ a) b c = context succ (lemma-assoc3 a b c)

theorem-left-distributive : ∀ (n m k : ℕ) -> n * (m + k) == n * m + n * k
theorem-left-distributive zero m k = refl
theorem-left-distributive (succ n) m k = trans step1 step2
  where
    step1 : n * (m + k) + (m + k) == (n * m + n * k) + (m + k)
    step1 = context (λ x → x + (m + k)) (theorem-left-distributive n m k)
    
    step2 : (n * m + n * k) + (m + k) == (n * m + m) + (n * k + k)
    step2 = lemma-assoc2 (n * m) (n * k) m k

theorem-right-distributive : ∀ (n m k : ℕ) -> (n + m) * k == n * k + m * k
theorem-right-distributive zero m k = refl
theorem-right-distributive (succ n) m k = trans step1 step2
  where
    step1 : (n + m) * k + k == (n * k + m * k) + k
    step1 = context (λ x → x + k) (theorem-right-distributive n m k)

    step2 : (n * k + m * k) + k == (n * k + k) + m * k
    step2 = lemma-assoc3 (n * k) (m * k) k

theorem-mult-associative : ∀ n m k -> (n * m) * k == n * (m * k)
theorem-mult-associative zero m k = refl
theorem-mult-associative (succ n) m k = trans step1 step2
  where
    step1 : (n * m + m) * k == (n * m) * k + m * k
    step1 = theorem-right-distributive (n * m) m k

    step2 : (n * m) * k + m * k == n * (m * k) + m * k
    step2 = context (λ x → x + m * k) (theorem-mult-associative n m k)

lemma-mult-one : ∀ (n : ℕ) -> n * (succ zero) == n
lemma-mult-one zero = refl
lemma-mult-one (succ n) = trans step1 step2
  where
    step1 : (n * (succ zero)) + (succ zero) == n + (succ zero)
    step1 = context (λ [-] →  [-] + (succ zero)) (lemma-mult-one n)

    step2 : n + (succ zero) == succ n
    step2 = lemma-add-one n

add-succ-commute : ∀ (n m : ℕ) -> n + (succ m) == m + (succ n)
add-succ-commute n m = trans step1 (trans step2 step3)
  where
    step1 : n + (succ m) == succ (n + m)
    step1 = symm (lemma-add-succ n m)

    step2 : succ (n + m) == succ (m + n)
    step2 = context succ (lemma-add-commutative n m)

    step3 : succ (m + n) ==  m + (succ n)
    step3 = lemma-add-succ m n

lemma-mult-succ : ∀ (n m : ℕ) -> (m * n) + m ==  m * (succ n)
lemma-mult-succ n zero = refl
lemma-mult-succ n (succ m) = trans step1 (trans step2 (trans step3 (trans step4 (trans step5 step6))))
  where
    -- Reflexitity works here because the equation holds
    -- by definition (of the function mult).
    step1 : ((succ m) * n) + (succ m) == ((m * n) + n) + (succ m)
    step1 = refl

    -- Use associativity of addition.
    step2 : ((m * n) + n) + (succ m) == (m * n) + ( n + (succ m))
    step2 = lemma-add-assoc (m * n) n (succ m)

    -- Use C-c C-, to check what needs to be proved. Then use the
    -- appropriate lemma.
    step3 : (m * n) + (n + (succ m)) == (m * n) + (m + (succ n))
    step3 = context (\ y -> (m * n) + y) (add-succ-commute n m)

    -- Use associativity again. Note that the 'symm' is needed to get
    -- the equation in the correct form for lemma-add-assoc.
    step4 : (m * n) + (m + (succ n)) ==  ((m * n) + m) + (succ n)
    step4 = symm (lemma-add-assoc (m * n) m (succ n))

    step5 :  ((m * n) + m) + (succ n) == (m * (succ n)) + (succ n)
    step5 = context (\ x -> x + (succ n)) (lemma-mult-succ n m)

    -- Once again, reflexivity will work here, because the equation
    -- holds by definition of the function mult.
    step6 : (m * (succ n)) + (succ n) == (succ m) * (succ n)
    step6 = refl

theorem-mult-commutative : ∀ (n m : ℕ) -> n * m == m * n
theorem-mult-commutative zero m = symm (lemma-mult-zero m) 
theorem-mult-commutative (succ n) m =
   trans (context (\ x -> x + m) (theorem-mult-commutative n m))
     (lemma-mult-succ n m)