🔍

Equations Inline Footnotes

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 renaming (_<_ to _<?_; _≤_ to _≤?_) 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 .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})

  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🔗

Mikan ships with preferred definitions of _+_ and _*_ which are optimised to direct computation on machine integers when applied to literals. These are defined in the built-in module [Prim.Data.Nat].

_ = _+_
_ = _*_

There is no built-in exponentiation operator, but we can define _^_ 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)

Our choice of defining _≤_ as a record wrapping a recursive boolean computation is slightly peculiar from a formalisation perspective. However, it turns out to be pretty much optimal:

• Like an indexed inductive type, but unlike directly computing a type by recursion, a record is definitionally injective in its arguments.

  This means that any function that has _≤_ arguments can take the numbers as implicit arguments.

• Unlike an indexed inductive type, we can arrange for a record type to be a definitional proposition, which means neither us nor the conversion checker need to spend time comparing elements of _≤_.

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

• Finally, we could imagine a record type wrapping a strict proposition computed by recursion. We opted against this for two reasons: first, re-using the wrapper type So limits the amount of code that needs to deal with the “weird” universe SProp.

  Second, a hand-written definition by recursion would have to fully traverse the numbers, in unary, until one of them is zero. Wrapping the built-in decision procedure _≤?_ shortcuts evaluation when the numbers are literals, meaning we don’t lose any type-checking time inspecting very large numeric literals.

_ :  ^  ≤  ^ 
_ = lift oh

_ = SProp

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)