open import 1Lab.Prelude

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

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 x≀yx \le y is a partial order, so it deserves the name ≀\le: 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 x≀yx \le y and (1+x)≀(1+y)(1 + x) \le (1 + y).

≀-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:

≀-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 })

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

<-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 (zero≠suc (sym 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 N{\mathbb{N}} is that it is, in some sense, generated by the max operator: We have x≀yx \le y iff max(x,y)=ymax(x,y) = y. 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))

Well-orderingπŸ”—

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 N{\mathbb{N}} 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 (n,p)(n, p) and one (k,qβ€²)(k, q'), we have that n=kn = k since both are minimal (so k≀nk \le n and n≀kn \le k), but we do not1 automatically have that p=qp = q.

module _ {β„“} {P : Nat β†’ Prop β„“} where
  private
    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 (Ξ» y β†’ hlevel!) (≀-antisym (n-min _ pk) (k-min _ pn))

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

    min-suc
      : βˆ€ {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)

    wo-suc
      : βˆ€ {P : Nat β†’ Type β„“} n
      β†’ P (suc n) β†’ Dec (P 0) β†’ minimal-solution (Ξ» n β†’ P (suc n))
      β†’ minimal-solution P
    wo-suc n psn (yes p0) (a , pa , x) = 0 , p0 , Ξ» k _ β†’ 0≀x
    wo-suc {P} n psn (no Β¬p0) (a , pa , x) = suc a , pa , min-suc {P} a Β¬p0 x

  β„•-minimal-solution
    : βˆ€ (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 = wo-suc n p (decp zero)
    (β„•-minimal-solution (Ξ» x β†’ P (suc x)) (Ξ» x β†’ decp (suc x)) n p)

  β„•-well-ordered
    : (βˆ€ 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 p,q:P(n)p, q : P(n)β†©οΈŽ