module Data.Nat.Order where

Properties of ordering on ℕ🔗

We establish the basic properties of ordering on the natural numbers. These are properties of the order itself, and not how it interacts with the semiring structure. For that, see Data.Nat.Properties. The first thing we establish is that is a partial order, so it deserves the name It is reflexive, transitive, antisymmetric, and takes values in propositions. In all cases, save for reflexivity, the induction happens on the witnesses of ordering, and Agda handles inducting on the naturals automatically.

≤-refl :  {x : Nat}  x  x
≤-refl {zero}  = 0≤x
≤-refl {suc x} = s≤s ≤-refl

≤-trans :  {x y z}  x  y  y  z  x  z
≤-trans 0≤x     0≤x     = 0≤x
≤-trans 0≤x     (s≤s q) = 0≤x
≤-trans (s≤s p) (s≤s q) = s≤s (≤-trans p q)

≤-antisym :  {x y : Nat}  x  y  y  x  x  y
≤-antisym 0≤x     0≤x     = refl
≤-antisym (s≤s p) (s≤s q) = ap suc (≤-antisym p q)

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

As a minor convenience, we prove that the constructor s≤s is an equivalence between and

≤-peel :  {x y : Nat}  suc x  suc y  x  y
≤-peel (s≤s p) = p

≤-sucr :  {x y : Nat}  x  y  x  suc y
≤-sucr 0≤x = 0≤x
≤-sucr (s≤s p) = s≤s (≤-sucr p)

≤-ascend :  {x}  x  suc x
≤-ascend = ≤-sucr ≤-refl

Furthermore, __ is decidable, and weakly total:

≤-dec : (x y : Nat)  Dec (x  y)
≤-dec zero zero = yes 0≤x
≤-dec zero (suc y) = yes 0≤x
≤-dec (suc x) zero = no λ { () }
≤-dec (suc x) (suc y) with ≤-dec x y
... | yes x≤y = yes (s≤s x≤y)
... | no ¬x≤y = no  { (s≤s x≤y)  ¬x≤y x≤y })

≤-is-weakly-total :  x y  ¬ (x  y)  y  x
≤-is-weakly-total zero    zero    _    = 0≤x
≤-is-weakly-total zero    (suc y) ¬0≤s = absurd (¬0≤s 0≤x)
≤-is-weakly-total (suc x) zero    _    = 0≤x
≤-is-weakly-total (suc x) (suc y) ¬s≤s = s≤s $
  ≤-is-weakly-total x y λ z  ¬s≤s (s≤s z)

We also have that a successor is never smaller than the number it succeeds:

¬sucx≤x : (x : Nat)  ¬ (suc x  x)
¬sucx≤x (suc x) (s≤s ord) = ¬sucx≤x x ord

We can do proofs on pairs of natural numbers by splitting into cases of their strict ordering:

≤-split :  (x y : Nat)  (x < y)  (y < x)  (x  y)
≤-split x y with ≤-dec (suc x) y
≤-split x y | yes x<y = inl x<y
≤-split x y | no x≥y with ≤-dec (suc y) x
≤-split x y | no x≥y | yes y<x = inr (inl y<x)
≤-split x y | no x≥y | no y≥x  = inr (inr (go x y x≥y y≥x)) where
  go :  x y  ¬ (suc x  y)  ¬ (suc y  x)  x  y
  go zero zero p q          = refl
  go zero (suc zero) p q    = absurd (p (s≤s 0≤x))
  go zero (suc (suc y)) p q = absurd (p (s≤s 0≤x))
  go (suc zero) zero p q    = absurd (q (s≤s 0≤x))
  go (suc (suc x)) zero p q = absurd (q (s≤s 0≤x))
  go (suc x) (suc y) p q    = ap suc (go x y  { a  p (s≤s a) }) λ { a  q (s≤s a) })

Properties of the strict order🔗

<-≤-asym :  {x y}  x < y  ¬ (y  x)
<-≤-asym {.(suc _)} {.(suc _)} (s≤s p) (s≤s q) = <-≤-asym p q

<-asym :  {x y}  x < y  ¬ (y < x)
<-asym {.(suc _)} {.(suc _)} (s≤s p) (s≤s q) = <-asym p q

<-not-equal :  {x y}  x < y  ¬ x  y
<-not-equal {zero} (s≤s p) q = absurd (zero≠suc q)
<-not-equal {suc x} (s≤s p) q = <-not-equal p (suc-inj q)

<-irrefl :  {x y}  x  y  ¬ (x < y)
<-irrefl {suc x} {zero}  p      q  = absurd (suc≠zero p)
<-irrefl {zero}  {suc y} p      _  = absurd (zero≠suc p)
<-irrefl {suc x} {suc y} p (s≤s q) = <-irrefl (suc-inj p) q

weaken-< :  {x y}  x < y  x  y
weaken-< {x} {suc y} p = ≤-sucr (≤-peel p)

Nat is a lattice🔗

An interesting tidbit about the ordering on is that it is, in some sense, generated by the max operator: We have iff It can also be generated by the min operator, but we don’t establish that here (it is a more general fact about lattices).

≤-iff-max :  {x y}  (x  y)  (y  max x y)
≤-iff-max = prop-ext! to from where
  to :  {x y}  x  y  y  max x y
  to {.0} {zero} 0≤x = refl
  to {.0} {suc y} 0≤x = refl
  to {x} {y} (s≤s p) = ap suc (to p)

  from :  {x y}  y  max x y  x  y
  from {zero} p = 0≤x
  from {suc x} {zero} p = absurd (zero≠suc p)
  from {suc x} {suc y} p = s≤s (from (suc-inj p))


In classical mathematics, the well-ordering principle states that every nonempty subset of the natural numbers has a minimal element. In constructive mathematics, there are subsets of which only have a minimal elements if excluded middle holds. The LEM-agnostic statement is that every inhabited complemented subset of the natural numbers has a minimal element. Note that for a complemented subset, inhabitation is the same as nonemptiness, but we prefer the stronger phrasing since it makes the proof one step shorter.

The “subset” part only comes in at the start: To get out from under the truncation, we need the fact that minimal solutions are unique. Given a minimal solution and one we have that since both are minimal (so and but we do not1 automatically have that

module _ {} {P : Nat  Prop } where
    minimal-solution :  {} (P : Nat  Type )  Type _
    minimal-solution P = Σ[ n  Nat ] (P n × (∀ k  P k  n  k))

    minimal-solution-unique : is-prop (minimal-solution λ x   P x )
    minimal-solution-unique (n , pn , n-min) (k , pk , k-min) =
      Σ-prop-path! (≤-antisym (n-min _ pk) (k-min _ pn))

The step of the code that actually finds a minimal solution does not need to be a predicate: we only need that for actually searching for an inhabited subset.

      :  {P : Nat  Type }   n  ¬ P 0
       (∀ k  P (suc k)  n  k)
        k  P k  suc n  k
    min-suc n ¬p0 nmins zero pk           = absurd (¬p0 pk)
    min-suc zero ¬p0 nmins (suc k) psk    = s≤s 0≤x
    min-suc (suc n) ¬p0 nmins (suc k) psk = s≤s (nmins k psk)

    :  (P : Nat  Type )
     (∀ n  Dec (P n))
     (n : Nat)  P n
     minimal-solution P
  ℕ-minimal-solution P decp zero p = 0 , p , λ k _  0≤x
  ℕ-minimal-solution P decp (suc n) p = case decp zero of λ where
    (yes p0)  0 , p0 , λ k _  0≤x
    (no ¬p0) 
      let (a , pa , x) = ℕ-minimal-solution (P  suc) (decp  suc) n p
       in suc a , pa , min-suc {P} a ¬p0 x

    : (∀ n  Dec  P n )
     ∃[ n  Nat ]  P n 
     Σ[ n  Nat ] ( P n  × (∀ k   P k   n  k))
  ℕ-well-ordered P-dec wit = ∥-∥-rec minimal-solution-unique
     { (n , p)  ℕ-minimal-solution _ P-dec n p }) wit

  1. We’re implicitly appealing to path induction to reduce this to the case where ↩︎