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.

## 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

## 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 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)