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) = ps (Nat-elim P pz ps n)

iter : ∀ {ℓ} {A : Type ℓ} → Nat → (A → A) → A → A
iter zero f = id
iter (suc n) f = f ∘ iter n f

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) = ⊥

suc≠zero : {n : Nat} → ¬ suc n ≡ zero
suc≠zero = zero≠suc ∘ sym

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.

pred : Nat → Nat
pred  = 
pred (suc n) = n

suc-inj : {x y : Nat} → suc x ≡ suc y → x ≡ y
suc-inj = ap pred

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:

private module _ where private

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

abstract
  from-prim-eq : ∀ {x y} → So (x == y) → x ≡ y
  from-prim-eq {zero}  {zero}  p = refl
  from-prim-eq {suc x} {suc y} p = ap suc (from-prim-eq p)

  from-prim-eq-refl : ∀ {x p} → from-prim-eq {x} {x} p ≡ refl
  from-prim-eq-refl {zero} = refl
  from-prim-eq-refl {suc x} = ap (ap suc) (from-prim-eq-refl {x})

  {-# REWRITE from-prim-eq-refl #-}

  to-prim-eq : ∀ {x y} → x ≡ y → So (x == y)
  to-prim-eq {zero} {zero} p = oh
  to-prim-eq {zero} {suc y} p = absurd (zero≠suc p)
  to-prim-eq {suc x} {zero} p = absurd (suc≠zero p)
  to-prim-eq {suc x} {suc y} p = to-prim-eq (suc-inj p)

instance
  Discrete-Nat : Discrete Nat
  Discrete-Nat .decide x y with oh? (x == y)
  ... | yes p = yes (from-prim-eq p)
  ... | no ¬p = no (¬p ∘ to-prim-eq)

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

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

instance
  H-Level-Nat : ∀ {n} → H-Level Nat ( + n)
  H-Level-Nat = basic-instance  Nat-is-set

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 appealing to the decision procedure _≤?_.

record _≤_ (x y : Nat) : Type where
  constructor lift
  field
    lower : So (x ≤? y)

We could also define the relation by recursion on the numbers to be compared or as an inductive predicate. However, our definition has the benefit of being a definitional proposition.

≤-is-prop : {x y : Nat} → is-prop (x ≤ y)
≤-is-prop p q = refl

As a further optimization, _≤?_ is implemented using the BUILTIN decision procedure _<?_. This makes it possible to typecheck proofs of _≤_ nearly instantly, even when the numbers involved are quite large.

module _ where private

  _ :  ^  ≤  ^ 
  _ = lift oh

abstract
  s≤s : ∀ {x y} → x ≤ y → suc x ≤ suc y
  s≤s (lift x≤y) = lift x≤y

  0≤x : ∀ {x} → zero ≤ x
  0≤x {x} = lift oh

  ≤-peel : ∀ {x y} → suc x ≤ suc y → x ≤ y
  ≤-peel (lift x≤y) = lift x≤y

  ≤-sucr : ∀ {x y} → x ≤ y → x ≤ suc y
  ≤-sucr {zero} {y} x≤y = 0≤x
  ≤-sucr {suc x} {suc y} x≤y = s≤s (≤-sucr (≤-peel x≤y))

  <-weaken : ∀ {x y} → suc x ≤ y → x ≤ y
  <-weaken {zero} {y} 1+x≤y = 0≤x
  <-weaken {suc x} {suc y} 1+x≤y = s≤s (<-weaken (≤-peel 1+x≤y))

abstract instance
  Leq-zero : ∀ {x} →  ≤ x
  Leq-zero = 0≤x

  Leq-suc-suc : ∀ {x y} → ⦃ x ≤ y ⦄ → suc x ≤ suc y
  Leq-suc-suc ⦃ x≤y ⦄ = s≤s x≤y

  Leq-refl : ∀ {x} → x ≤ x
  Leq-refl {zero} = 0≤x
  Leq-refl {suc x} = s≤s Leq-refl
  {-# INCOHERENT Leq-refl #-}

  Leq-sucr : ∀ {x y} → ⦃ x ≤ y ⦄ → x ≤ suc y
  Leq-sucr ⦃ x≤y ⦄ = ≤-sucr x≤y
  {-# INCOHERENT Leq-sucr #-}

  H-Level-≤ : ∀ {x y n} → H-Level (x ≤ y) (suc n)
  H-Level-≤ = prop-instance (λ _ _ → refl)

¬suc≤0 : ∀ {x} → suc x ≤  → ⊥
¬suc≤0 ()

abstract
  ≤-trans : ∀ {x y z} → x ≤ y → y ≤ z → x ≤ z
  ≤-trans {zero} {y} {z} x≤y y≤z = 0≤x
  ≤-trans {suc x} {suc y} {suc z} x≤y y≤z = s≤s (≤-trans (≤-peel x≤y) (≤-peel y≤z))

factorial : Nat → Nat
factorial zero = 
factorial (suc n) = suc n * factorial n

Positive : Nat → Type
Positive n =  ≤ n

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

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

_>_ : Nat → Nat → Type
x > y = y < x
infix  _>_

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)