open import 1Lab.Path.IdentitySystem
open import 1Lab.HLevel.Closure
open import 1Lab.HLevel
open import 1Lab.Path
open import 1Lab.Type

open import Data.Bool.Base
open import Data.Dec.Base

module Data.Nat.Base where

open import Prim.Data.Nat hiding (_<_) public

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 {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 (suc≠zero 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)

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 {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 as an inductive predicate. We could also define the relation by recursion on the numbers to be compared, but the inductive version has much better properties when it comes to type inference.

data _≤_ : Nat → Nat → Type where
  instance
    0≤x : ∀ {x} →  ≤ x
  s≤s : ∀ {x y} → x ≤ y → suc x ≤ suc y

instance
  s≤s' : ∀ {x y} → ⦃ x ≤ y ⦄ → suc x ≤ suc y
  s≤s' ⦃ x ⦄ = s≤s x

  x≤x : ∀ {x} → x ≤ x
  x≤x {zero}  = 0≤x
  x≤x {suc x} = s≤s x≤x

  x≤sucy : ∀ {x y} ⦃ p : x ≤ y ⦄ → x ≤ suc y
  x≤sucy {.} {y} ⦃ 0≤x ⦄ = 0≤x
  x≤sucy {.(suc _)} {.(suc _)} ⦃ s≤s p ⦄ = s≤s (x≤sucy ⦃ p ⦄)

  {-# INCOHERENT x≤x x≤sucy #-}

≤-peel : ∀ {x y : Nat} → suc x ≤ suc y → x ≤ y
≤-peel (s≤s p) = p

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

≤-trans : ∀ {x y z} → x ≤ y → y ≤ z → x ≤ z
≤-trans 0≤x     0≤x     = 0≤x
≤-trans 0≤x     (s≤s q) = 0≤x
≤-trans (s≤s p) (s≤s q) = s≤s (≤-trans p q)

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

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

<-weaken : ∀ {x y} → x < y → x ≤ y
<-weaken {x} {suc y} p = ≤-sucr (≤-peel p)

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)