open import 1Lab.HLevel.Sets
open import 1Lab.Type.Dec
open import 1Lab.HLevel
open import 1Lab.Path
open import 1Lab.Type

module Data.Nat.Base where

Natural Numbers🔗

The natural numbers are the inductive type generated by zero and closed under taking successors. Thus, they satisfy the following induction principle, which is familiar:

Nat-elim : ∀ {ℓ} (P : Nat → Type ℓ)
         → P 
         → ({n : Nat} → P n → P (suc n))
         → (n : Nat) → P n
Nat-elim P pz ps zero    = pz
Nat-elim P pz ps (suc n) = Nat-elim (λ z → P (suc z)) (ps pz) ps n

Translating from type theoretic notation to mathematical English, the type of Nat-elim says that if a predicate P holds of zero, and the truth of P(suc n) follows from P(n), then P is true for every natural number.

Discreteness🔗

An interesting property of the natural numbers, type-theoretically, is that they are discrete: given any pair of natural numbers, there is an algorithm that can tell you whether or not they are equal. First, observe that we can distinguish zero from successor:

zero≠suc : {n : Nat} → zero ≡ suc n → ⊥
zero≠suc path = subst distinguish path tt where
  distinguish : Nat → Type
  distinguish zero = ⊤
  distinguish (suc x) = ⊥

The idea behind this proof is that we can write a predicate which is true for zero, and false for any successor. Since we know that ⊤ is inhabited (by tt), we can transport that along the claimed path to get an inhabitant of ⊥, i.e., a contradiction.

suc-inj : {x y : Nat} → suc x ≡ suc y → x ≡ y
suc-inj = ap pred where
  pred : Nat → Nat
  pred (suc x) = x
  pred zero = zero

Furthermore, observe that the successor operation is injective, i.e., we can “cancel” it on paths. Putting these together, we get a proof that equality for the natural numbers is decidable:

Discrete-Nat : Discrete Nat
Discrete-Nat zero zero    = yes refl
Discrete-Nat zero (suc y) = no λ zero≡suc → absurd (zero≠suc zero≡suc)
Discrete-Nat (suc x) zero = no λ suc≡zero → absurd (zero≠suc (sym suc≡zero))
Discrete-Nat (suc x) (suc y) with Discrete-Nat x y
... | yes x≡y = yes (ap suc x≡y)
... | no ¬x≡y = no λ sucx≡sucy → ¬x≡y (suc-inj sucx≡sucy)

Hedberg’s theorem implies that Nat is a set, i.e., it only has trivial paths.

Nat-is-set : is-set Nat
Nat-is-set = Discrete→is-set Discrete-Nat

Arithmetic🔗

Agda already comes with definitions for addition and multiplication of natural numbers. They are reproduced below, using different names, for the sake of completeness:

plus : Nat → Nat → Nat
plus zero y = y
plus (suc x) y = suc (plus x y)

times : Nat → Nat → Nat
times zero y = zero
times (suc x) y = y + times x y

These match up with the built-in definitions of _+_ and _*_:

plus≡+ : plus ≡ _+_
plus≡+ i zero y = y
plus≡+ i (suc x) y = suc (plus≡+ i x y)

times≡* : times ≡ _*_
times≡* i zero y = zero
times≡* i (suc x) y = y + (times≡* i x y)

The exponentiation operator ^ is defined by recursion on the exponent.

_^_ : Nat → Nat → Nat
x ^ zero = 
x ^ suc y = x * (x ^ y)

infixr  _^_

Ordering🔗

We define the order relation _≤_ on the natural numbers by recursion:

_≤_ : Nat → Nat → Type
zero ≤ zero = ⊤
zero ≤ suc y = ⊤
suc x ≤ zero = ⊥
suc x ≤ suc y = x ≤ y
infix  _≤_

We define the strict ordering on Nat as well, re-using the definition of _≤_.

_<_ : Nat → Nat → Type
m < n = suc m ≤ n
infix  _<_

Then we can prove it is reflexive, transitive and antisymmetric.

≤-refl : (x : Nat) → x ≤ x
≤-refl zero = tt
≤-refl (suc x) = ≤-refl x

0≤x : (x : Nat) → zero ≤ x
0≤x zero = tt
0≤x (suc x) = tt

≤-trans : (x y z : Nat) → x ≤ y → y ≤ z → x ≤ z
≤-trans zero zero zero _ _          = tt
≤-trans zero zero (suc z) _ _       = tt
≤-trans zero (suc y) z p q          = 0≤x z
≤-trans (suc x) (suc y) (suc z) p q = ≤-trans x y z p q

≤-antisym : (x y : Nat) → x ≤ y → y ≤ x → x ≡ y
≤-antisym zero zero p q = refl
≤-antisym (suc x) (suc y) p q = ap suc (≤-antisym x y p q)

A simple inductive argument proves that _≤_ always takes values in propositions, i.e. any “two” proofs that x ≤ y are identical:

≤-prop : (x y : Nat) → is-prop (x ≤ y)
≤-prop zero zero p q = refl
≤-prop zero (suc y) p q = refl
≤-prop (suc x) (suc y) p q = ≤-prop x y p q

Furthermore, _≤_ is decidable:

≤-flip : (x y : Nat) → (x ≤ y → ⊥) → y ≤ x
≤-flip zero zero ¬x≤y = tt
≤-flip zero (suc y) ¬x≤y = ¬x≤y tt
≤-flip (suc x) zero ¬x≤y = tt
≤-flip (suc x) (suc y) ¬x≤y = ≤-flip x y ¬x≤y

≤-dec : (x y : Nat) → Dec (x ≤ y)
≤-dec zero zero = yes tt
≤-dec zero (suc y) = yes tt
≤-dec (suc x) zero = no (λ z → z)
≤-dec (suc x) (suc y) = ≤-dec x y

As an “ordering combinator”, we can define the maximum of two natural numbers by recursion: The maximum of zero and a successor (on either side) is the successor, and the maximum of successors is the successor of their maximum.

max : Nat → Nat → Nat
max zero zero = zero
max zero (suc y) = suc y
max (suc x) zero = suc x
max (suc x) (suc y) = suc (max x y)

Similarly, we can define the minimum of two numbers:

min : Nat → Nat → Nat
min zero zero = zero
min zero (suc y) = zero
min (suc x) zero = zero
min (suc x) (suc y) = suc (min x y)