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 0
          ({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.


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


Heads up! The arithmetic properties of operations on the natural numbers are in the module 1Lab.Data.Nat.Properties.

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 = 1
x ^ suc y = x * (x ^ y)

infixr 8 _^_


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 3 _≤_

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

_<_ : Nat  Nat  Type
m < n = suc m  n
infix 3 _<_

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)