module Data.Nat.Base where

# Natural Numbersπ

The natural numbers are the inductive type generated by `zero`

and closed
under taking `suc`

cessors. 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 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) = β₯

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 instance H-Level-Nat : β {n} β H-Level Nat (2 + n) H-Level-Nat = basic-instance 2 Nat-is-set

## Arithmeticπ

**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 _^_

## 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} β 0 β€ 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 Positive : Nat β Type Positive zero = β₯ Positive (suc n) = β€

We define the strict ordering on `Nat`

as well, re-using the
definition of `_β€_`

.

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

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)