open import 1Lab.HLevel.Retracts 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 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 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)