Martin Escardo 2011.

\begin{code}

{-# OPTIONS --without-K #-}

module Naturals where

open import SetsAndFunctions hiding (_+_)
open import CurryHoward
open import Equality
open import DiscreteAndSeparated

data  : Set where 
  zero :               
  succ :          

{-# BUILTIN NATURAL  #-}
-- {-# BUILTIN ZERO zero #-}
-- {-# BUILTIN SUC succ #-}


rec : {X : Set}  X  (X  X)  (  X)
rec x f zero = x
rec x f (succ n) = f(rec x f n)

induction : {A :   Prp}  A 0  (∀(k : )  A k  A(succ k))  ∀(n : )  A n 
induction base step 0 = base
induction base step (succ n) = step n (induction base step n)


a-peano-axiom : ∀{n : }  succ n  0
a-peano-axiom ()

pred :   
pred 0 = 0
pred (succ n) = n

succ-injective : ∀{i j : }  succ i  succ j  i  j
succ-injective = cong pred

ℕ-discrete : discrete  
ℕ-discrete 0 0 = ∨-intro₀ refl 
ℕ-discrete 0 (succ n) = ∨-intro₁ (λ())
ℕ-discrete (succ m) 0 = ∨-intro₁ (λ())
ℕ-discrete (succ m) (succ n) =  step(ℕ-discrete m n)
  where 
   step : m  n  (m  n)  succ m  succ n  (succ m  succ n) 
   step (in₀ r) = in₀(cong succ r)
   step (in₁ f) = in₁ s  f(succ-injective s)) 

open import Two
open import DecidableAndDetachable

≡-indicator :  (m : )  Σ \(p :   )  (n : )  (p n    m  n) × (p n    m  n)
≡-indicator m = co-characteristic-function (ℕ-discrete m)

χ≡ :     
χ≡ m = π₀ (≡-indicator m)

χ≡-spec : (m n : )  (χ≡ m n    m  n) × (χ≡ m n    m  n)
χ≡-spec m = π₁ (≡-indicator m)

_≣_ :     Set
m  n = (χ≡ m n  )

infix  30 _≣_

≡-agrees-with-≣ : (m n : )  m  n  m  n
≡-agrees-with-≣ m n =  r  Lemma[b≢₀→b≡₁]  s  π₀(χ≡-spec m n) s r)) , π₁(χ≡-spec m n)

-- We don't need the following anymore:

≢-indicator :  (m : )  Σ \(p :   )  (n : )  (p n    m  n) × (p n    m  n)
≢-indicator m = indicator(ℕ-discrete m)

χ≢ :     
χ≢ m = π₀ (≢-indicator m)

χ≢-spec : (m n : )  (χ≢ m n    m  n) × (χ≢ m n    m  n)
χ≢-spec m = π₁ (≢-indicator m)

_≠_ :     Set
m  n = (χ≢ m n  )

infix  30 _≠_

≠-agrees-with-≢ : (m n : )  m  n  m  n
≠-agrees-with-≢ m n = π₁(χ≢-spec m n) ,  d  Lemma[b≢₀→b≡₁] (contra-positive(π₀(χ≢-spec m n)) d))

-- up to here. But I will keep it anyway.

\end{code}

Sometimes the following injection is useful:

\begin{code}

open import Two

number :   
number  = 0
number  = 1

\end{code}

The following definitions can be shortened:

\begin{code}

infixl 31 _+_

_+_ :     
n + 0 = n
n + (succ m) = succ(n + m)


n-plus-zero-equals-n : ∀(n : )  n + 0  n
n-plus-zero-equals-n n = refl


zero-plus-n-equals-n : ∀(n : )  0 + n  n
zero-plus-n-equals-n = induction base step
  where base : 0 + 0  0
        base = refl

        step : ∀(n : )  0 + n  n  0 + succ n  succ n
        step n IH = goal
          where lemma₀ : 0 + succ n  succ (0 + n)
                lemma₀ = refl

                lemma₁ : succ (0 + n)  succ n
                lemma₁ = cong succ IH

                goal : 0 + succ n  succ n
                goal = trans lemma₀ lemma₁


addition-associativity : ∀(l n m : )  (l + n) + m  l + (n + m)
addition-associativity l n = induction base step
  where base : (l + n) + 0  l + (n + 0)
        base = goal
          where lemma₀ : (l + n) + 0  l + n
                lemma₀ = refl

                lemma₁ : l + n  l + (n + 0)
                lemma₁ = refl

                goal : (l + n) + 0  l + (n + 0)
                goal = trans lemma₀ lemma₁

        step : ∀(m : )  (l + n) + m  l + (n + m)  
                          (l + n) + succ m  l + (n + succ m)
        step m IH = goal
          where lemma₀ : (l + n) + succ m  succ ((l + n) + m)
                lemma₀ = refl

                lemma₁ : succ ((l + n) + m)  succ (l + (n + m))
                lemma₁ = cong succ IH

                lemma₂ : succ (l + (n + m))  l + succ (n + m)
                lemma₂ = refl

                lemma₃ : l + succ (n + m)  l + (n + succ m)
                lemma₃ = refl

                goal : (l + n) + succ m  l + (n + succ m)
                goal = trans lemma₀ (trans lemma₁ 
                      (trans lemma₂ lemma₃))

addition-commutativity : ∀(n m : )  n + m  m + n
addition-commutativity n = induction base step
  where base : n + 0  0 + n
        base = trans (n-plus-zero-equals-n n) 
                            (sym (zero-plus-n-equals-n n))

        step : ∀(m : )  n + m  m + n  n + succ m  succ m + n
        step m IH = goal
          where lemma₀ : ∀(k : )  succ k  1 + k
                lemma₀ = induction base₀ step₀
                  where base₀ : succ 0  1 + 0
                        base₀ = refl

                        step₀ : ∀(k : )  succ k  1 + k 
                                           succ (succ k)  1 + (succ k)
                        step₀ k IH' = goal₀
                          where lemma₀' : 1 + (succ k)  succ (1 + k)
                                lemma₀' = refl

                                lemma₁' : succ (1 + k)  succ (succ k)
                                lemma₁' = cong succ (sym IH')

                                goal₀ : succ (succ k)  1 + (succ k)
                                goal₀ = sym (trans lemma₀' lemma₁')

                lemma₁ : n + succ m  succ (n + m)
                lemma₁ = refl

                lemma₂ : succ (n + m)  succ (m + n)
                lemma₂ = cong succ IH

                lemma₃ : succ (m + n)  1 + (m + n)
                lemma₃ = lemma₀ (m + n)

                lemma₄ : 1 + (m + n)  (1 + m) + n
                lemma₄ = sym (addition-associativity 1 m n)

                lemma₅ : (1 + m) + n  succ m + n
                lemma₅ = cong  x  x + n) (sym (lemma₀ m))

                goal : n + succ m  succ m + n
                goal = trans lemma₁ (trans lemma₂ 
                      (trans lemma₃ (trans lemma₄ lemma₅)))


trivial-addition-rearrangement : ∀(x y z : )  x + y + z  x + z + y
trivial-addition-rearrangement x y z = 
      trans 
        (addition-associativity x y z)
        (trans 
           (cong  t  x + t) (addition-commutativity y z))
           (sym (addition-associativity x z y)))

\end{code}