Chuangjie Xu 2014

\begin{code}

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

module Preliminaries.NaturalNumber where

open import Preliminaries.SetsAndFunctions renaming (_+_ to _∨_)
open import Preliminaries.HSet

\end{code}

Natural numbers, basic operations and properties

\begin{code}

data  : Set where
zero :
succ :

{-# BUILTIN NATURAL  #-}

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

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

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

ℕ-discrete : discrete
ℕ-discrete  0        0       = inl refl
ℕ-discrete  0       (succ m) = inr  ())
ℕ-discrete (succ n)  0       = inr  ())
ℕ-discrete (succ n) (succ m) = step (ℕ-discrete n m)
where
step : decidable(n  m)  decidable (succ n  succ m)
step (inl r) = inl (ap succ r)
step (inr f) = inr  s  f (succ-injective s))

ℕ-hset : hset
ℕ-hset = discrete-is-hset ℕ-discrete

\end{code}

\begin{code}

infixl 30 _+_

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

Lemma[0+m=m] : ∀(m : )  0 + m  m
Lemma[0+m=m] 0 = refl
Lemma[0+m=m] (succ m) = ap succ (Lemma[0+m=m] m)

Lemma[n+1+m=n+m+1] : ∀(n m : )  succ n + m  n + succ m
Lemma[n+1+m=n+m+1] n 0 = refl
Lemma[n+1+m=n+m+1] n (succ m) = ap succ (Lemma[n+1+m=n+m+1] n m)

Lemma[n+m=m+n] : ∀(n m : )  n + m  m + n
Lemma[n+m=m+n] n 0        = (Lemma[0+m=m] n)⁻¹
Lemma[n+m=m+n] n (succ m) = (ap succ (Lemma[n+m=m+n] n m)) · (Lemma[n+1+m=n+m+1] m n)⁻¹

Lemma[n≡0∨n≡m+1] : ∀(n : )  n  0  (Σ \(m : )  n  succ m)
Lemma[n≡0∨n≡m+1] 0        = inl refl
Lemma[n≡0∨n≡m+1] (succ n) = inr (n , refl)

\end{code}

Inequality

\begin{code}

infix 30 _≤_
infix 30 _<_
infix 30 _≰_
infix 30 _≮_

data _≤_ :     Set where
≤-zero : ∀{n : }  0  n
≤-succ : ∀{m n : }  m  n  succ m  succ n

_<_ :     Set
m < n = succ m  n

_≰_ :     Set
m  n = ¬ (m  n)

_≮_ :     Set
m  n = ¬ (m < n)

≤-refl : {n : }  n  n
≤-refl {0}      = ≤-zero
≤-refl {succ n} = ≤-succ ≤-refl

≤-pred : {n m : }  succ n  succ m  n  m
≤-pred (≤-succ r) = r

≤-trans : {a b c : }  a  b  b  c  a  c
≤-trans ≤-zero     v          = ≤-zero
≤-trans (≤-succ u) (≤-succ v) = ≤-succ (≤-trans u v)

≤-r-succ : {n m : }  n  m  n  succ m
≤-r-succ ≤-zero     = ≤-zero
≤-r-succ (≤-succ r) = ≤-succ (≤-r-succ r)

Lemma[≤-hprop] : ∀{m n : }  ∀(r r' : m  n)  r  r'
Lemma[≤-hprop] {0}      {n}      ≤-zero ≤-zero = refl
Lemma[≤-hprop] {succ m} {0}      ()     ()
Lemma[≤-hprop] {succ m} {succ n} (≤-succ r) (≤-succ r') = ap ≤-succ (Lemma[≤-hprop] r r')

Lemma[a≤b-decidable] : ∀{a b : }  decidable (a  b)
Lemma[a≤b-decidable] {0}      {0}      = inl ≤-zero
Lemma[a≤b-decidable] {0}      {succ b} = inl ≤-zero
Lemma[a≤b-decidable] {succ a} {0}      = inr  ())
Lemma[a≤b-decidable] {succ a} {succ b} = cases c₀ c₁ IH
where
IH : decidable (a  b)
IH = Lemma[a≤b-decidable] {a} {b}
c₀ : a  b  succ a  succ b
c₀ r = ≤-succ r
c₁ : ¬ (a  b)  ¬ (succ a  succ b)
c₁ f sr = ∅-elim (f (≤-pred sr))

Lemma[n≤n+1] : ∀(n : )  n  succ n
Lemma[n≤n+1] 0        = ≤-zero
Lemma[n≤n+1] (succ n) = ≤-succ (Lemma[n≤n+1] n)

Lemma[m+1≤n+1→m≤n] : ∀{m n : }  succ m  succ n  m  n
Lemma[m+1≤n+1→m≤n] (≤-succ r) = r

Lemma[m≮n→n≤m] : ∀{m n : }  m  n  n  m
Lemma[m≮n→n≤m] {m}      {0}      f = ≤-zero
Lemma[m≮n→n≤m] {0}      {succ n} f = ∅-elim (f (≤-succ ≤-zero))
Lemma[m≮n→n≤m] {succ m} {succ n} f = ≤-succ (Lemma[m≮n→n≤m] (f  ≤-succ))

Lemma[m<n→m≠n] : ∀{m n : }  m < n  m  n
Lemma[m<n→m≠n] {0}      {0}      ()
Lemma[m<n→m≠n] {0}      {succ n} r          = λ ()
Lemma[m<n→m≠n] {succ m} {0}      r          = λ ()
Lemma[m<n→m≠n] {succ m} {succ n} (≤-succ r) = λ e  Lemma[m<n→m≠n] r (succ-injective e)

Lemma[a≤b→a+c≤b+c] : ∀(a b c : )  a  b  a + c  b + c
Lemma[a≤b→a+c≤b+c] a b 0        r = r
Lemma[a≤b→a+c≤b+c] a b (succ c) r = ≤-succ (Lemma[a≤b→a+c≤b+c] a b c r)

Lemma[a<b→a+c<b+c] : ∀(a b c : )  a < b  a + c < b + c
Lemma[a<b→a+c<b+c] a b c r = transport  n  n  b + c) (lemma a c) (Lemma[a≤b→a+c≤b+c] (succ a) b c r)
where
lemma : ∀(n m : )  (succ n) + m  succ (n + m)
lemma n 0 = refl
lemma n (succ m) = ap succ (lemma n m)

Lemma[a≤a+b] : ∀(a b : )  a  a + b
Lemma[a≤a+b] a 0 = ≤-refl
Lemma[a≤a+b] a (succ b) = ≤-trans (Lemma[a≤a+b] a b) (Lemma[n≤n+1] (a + b))

Lemma[m≤n∧n≤m→m=n] : ∀{m n : }  m  n  n  m  m  n
Lemma[m≤n∧n≤m→m=n] {0}      {0}      ≤-zero     ≤-zero      = refl
Lemma[m≤n∧n≤m→m=n] {0}      {succ n} ≤-zero     ()
Lemma[m≤n∧n≤m→m=n] {succ m} {0}      ()         ≤-zero
Lemma[m≤n∧n≤m→m=n] {succ m} {succ n} (≤-succ r) (≤-succ r') = ap succ (Lemma[m≤n∧n≤m→m=n] r r')

Lemma[n≤m+1→n≤m∨n≡m+1] : {n m : }  n  succ m  (n  m)  (n  succ m)
Lemma[n≤m+1→n≤m∨n≡m+1] {0}      {m}      r = inl ≤-zero
Lemma[n≤m+1→n≤m∨n≡m+1] {succ 0} {0}      r = inr refl
Lemma[n≤m+1→n≤m∨n≡m+1] {succ (succ n)} {0} (≤-succ ())
Lemma[n≤m+1→n≤m∨n≡m+1] {succ n} {succ m} (≤-succ r) = cases c₀ c₁ IH
where
c₀ : n  m  succ n  succ m
c₀ = ≤-succ
c₁ : n  succ m  succ n  succ (succ m)
c₁ = ap succ
IH : (n  m)  (n  succ m)
IH = Lemma[n≤m+1→n≤m∨n≡m+1] {n} {m} r

Lemma[n≰m→m<n] : {n m : }  ¬(n  m)  m < n
Lemma[n≰m→m<n] {0}      {m}      f = ∅-elim (f ≤-zero)
Lemma[n≰m→m<n] {succ n} {0}      f = ≤-succ ≤-zero
Lemma[n≰m→m<n] {succ n} {succ m} f = ≤-succ (Lemma[n≰m→m<n] (f  ≤-succ))

Lemma[≤-Σ] : ∀(a b : )  a  b  Σ \(c : )  a + c  b
Lemma[≤-Σ] 0 b ≤-zero = b , Lemma[0+m=m] b
Lemma[≤-Σ] (succ a) 0 ()
Lemma[≤-Σ] (succ a) (succ b) (≤-succ r) = c , (Lemma[n+1+m=n+m+1] a c) · (ap succ eq)
where
c :
c = pr₁ (Lemma[≤-Σ] a b r)
eq : a + c  b
eq = pr₂ (Lemma[≤-Σ] a b r)

\end{code}

Maximum

\begin{code}

max :
max 0 m = m
max n 0 = n
max (succ n) (succ m) = succ (max n m)

max-spec₀ : (n m : )  n  max n m
max-spec₀ 0        m        = ≤-zero
max-spec₀ (succ n) 0        = ≤-refl
max-spec₀ (succ n) (succ m) = ≤-succ (max-spec₀ n m)

max-spec₁ : (n m : )  m  max n m
max-spec₁ 0        m        = ≤-refl
max-spec₁ (succ n) 0        = ≤-zero
max-spec₁ (succ n) (succ m) = ≤-succ (max-spec₁ n m)

\end{code}

The type of "there exists a least number n such that P n"

\begin{code}

Σ-min : (  Set)  Set
Σ-min P = Σ \(n : )  (P n) × (∀(n' : )  P n'  n  n')

re-pair : {P :   Set}  Σ-min P  Σ P
re-pair (n , p , _) = (n , p)

Σ-min-≡ : {P :   Set}{w₀ w₁ : Σ-min P}  w₀  w₁  re-pair w₀  re-pair w₁
Σ-min-≡ {P} {w} {.w} refl = refl

\end{code}

Primitive and course-of-value inductions

\begin{code}

primitive-induction : {P :   Set}
P 0  (∀ n  P n  P(succ n))   n  P n
primitive-induction base step 0        = base
primitive-induction base step (succ n) = step n (primitive-induction base step n)

CoV-induction : {P :   Set}
(∀ n  (∀ m  m < n  P m)  P n)   n  P n
CoV-induction {P} step n = step n (claim n)
where
Q :   Set
Q n =  m  succ m  n  P m
qbase : Q 0
-- ∀ m → succ m ≤ 0 → P m
qbase m ()
qstep :  n  Q n  Q(succ n)
-- ∀ n → (∀ m → succ m ≤ n → P m) → ∀ m → succ m ≤ succ n → P m
qstep n qn m (≤-succ r) = step m  k u  qn k (≤-trans u r))
claim :  n  Q n
-- ∀ n → ∀ m → succ m ≤ n → P m
claim = primitive-induction qbase qstep

\end{code}