open import 1Lab.Prelude

open import Data.Nat.Properties
open import Data.Nat.Order
open import Data.Dec.Base
open import Data.Nat.Base
open import Data.Sum.Base

open import Order.Diagram.Bottom
open import Order.Diagram.Join
open import Order.Diagram.Meet
open import Order.Diagram.Top
open import Order.Total
open import Order.Base

module Order.Instances.Nat where


# The usual ordering on natural numbersπ

private module P = Poset
open is-meet
open is-join
open Bottom
open Meet
open Join


This module deals with noting down facts about the usual ordering on the set of natural numbers; most of the proofs are in the modules Data.Nat.Properties and Data.Nat.Order.

We have already shown that the usual ordering (or βnumericβ) ordering on the natural numbers is a poset:

Nat-poset : Poset lzero lzero
Nat-poset .P.Ob        = Nat
Nat-poset .P._β€_       = _β€_
Nat-poset .P.β€-thin    = β€-is-prop
Nat-poset .P.β€-refl    = β€-refl
Nat-poset .P.β€-trans   = β€-trans
Nat-poset .P.β€-antisym = β€-antisym


Weβve also defined procedures for computing the meets and joins of pairs of natural numbers:

Nat-meets : β x y β Meet Nat-poset x y
Nat-meets x y .glb                = min x y
Nat-meets x y .has-meet .meetβ€l   = min-β€l x y
Nat-meets x y .has-meet .meetβ€r   = min-β€r x y
Nat-meets x y .has-meet .greatest = min-univ x y

Nat-joins : β x y β Join Nat-poset x y
Nat-joins x y .lub              = max x y
Nat-joins x y .has-join .lβ€join = max-β€l x y
Nat-joins x y .has-join .rβ€join = max-β€r x y
Nat-joins x y .has-join .least  = max-univ x y


Itβs straightforward to show that this order is bounded below, since we have for any

Nat-bottom : Bottom Nat-poset
Nat-bottom .bot          = 0
Nat-bottom .has-bottom x = 0β€x


However, itβs not bounded above:

Nat-no-top : Β¬ Top Nat-poset
Nat-no-top record { top = greatest ; has-top = is-greatest } =
let
remβ : suc greatest β€ greatest
remβ = is-greatest (suc greatest)
in Β¬sucxβ€x _ remβ


This is also a decidable total order; we show totality by proving weak totality, since we already know that the ordering is decidable.

Nat-is-dec-total : is-decidable-total-order Nat-poset
Nat-is-dec-total = from-weakly-total (β€-is-weakly-total _ _)