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}