open import 1Lab.Prelude

open import Data.Dec
open import Data.Sum

open import Order.Diagram.Join
open import Order.Diagram.Meet
open import Order.Base

module Order.Total where

open is-join
open is-meet

Total ordersπŸ”—

A total order is a partial order where every pair of elements can be compared.

record is-total-order {o β„“} (P : Poset o β„“) : Type (o βŠ” β„“) where
  open Poset P public

  field
    compare         : βˆ€ x y β†’ (x ≀ y) ⊎ (y ≀ x)
Note

The ordering procedure, compare, is orthogonal from having a decision procedure for the order: if comparing results in we can not, in general, turn this into a proof of

Having a decision procedure for the relative order of two elements allows us to compute meets and joins in a very straightforward way: We test whether and, if that’s the case, then otherwise, The definition of is exactly dual.

module minmax {o β„“} {P : Poset o β„“} (to : is-total-order P) where
  open is-total-order to

  min : (x y : ⌞ P ⌟) β†’ ⌞ P ⌟
  min x y with compare x y
  ... | inl p = x
  ... | inr q = y

The proofs that this is actually the meet of and proceed by doing the comparison again: this β€œunblocks” the computation of 

  abstract
    min-≀l : βˆ€ x y β†’ min x y ≀ x
    min-≀l x y with compare x y
    ... | inl p = ≀-refl
    ... | inr q = q

    min-≀r : βˆ€ x y β†’ min x y ≀ y
    min-≀r x y with compare x y
    ... | inl p = p
    ... | inr q = ≀-refl

    min-univ : βˆ€ x y z β†’ z ≀ x β†’ z ≀ y β†’ z ≀ min x y
    min-univ x y z p q with compare x y
    ... | inl _ = p
    ... | inr _ = q

This is everything we need to prove that we have our hands on a meet.

  min-is-meet : βˆ€ x y β†’ is-meet P x y (min x y)
  min-is-meet x y .meet≀l   = min-≀l x y
  min-is-meet x y .meet≀r   = min-≀r x y
  min-is-meet x y .greatest = min-univ x y

Since the case of maxima is precisely dual, we present it with no further commentary.

  max : (x y : ⌞ P ⌟) β†’ ⌞ P ⌟
  max x y with compare x y
  ... | inl p = y
  ... | inr q = x

  max-≀l : βˆ€ x y β†’ x ≀ max x y
  max-≀l x y with compare x y
  ... | inl p = p
  ... | inr q = ≀-refl

  max-≀r : βˆ€ x y β†’ y ≀ max x y
  max-≀r x y with compare x y
  ... | inl p = ≀-refl
  ... | inr q = q

  max-univ : βˆ€ x y z β†’ x ≀ z β†’ y ≀ z β†’ max x y ≀ z
  max-univ x y z p q with compare x y
  ... | inl _ = q
  ... | inr _ = p

  max-is-join : βˆ€ x y β†’ is-join P x y (max x y)
  max-is-join x y .l≀join = max-≀l x y
  max-is-join x y .r≀join = max-≀r x y
  max-is-join x y .least  = max-univ x y

Decidable total ordersπŸ”—

In particularly nice cases, we can not only decide the relative position of a pair of elements, but whether a pair of elements is related at all: this is a decidable total order.

is-decidable-poset : βˆ€ {o β„“} (P : Poset o β„“) β†’ Type _
is-decidable-poset P = βˆ€ {x y} β†’ Dec (x ≀ y)
  where open Poset P

record is-decidable-total-order {o β„“} (P : Poset o β„“) : Type (o βŠ” β„“) where
  field
    has-is-total : is-total-order P

  open is-total-order has-is-total public

As the name implies, a decidable total order must be a total order; and it must also be decidable:

  field
    ⦃ dec-≀    ⦄ : is-decidable-poset P
    ⦃ discrete ⦄ : Discrete ⌞ P ⌟

Note that we have included a requirement that a decidable total order be discrete, i.e., that its equality is also decidable. This is purely for formalisation reasons β€” allowing the user to specify a more efficient decision procedure for equality β€”, since we can use the decidable ordering to decide equality.

  private
    was-discrete-anyways : Discrete ⌞ P ⌟
    was-discrete-anyways {x} {y} with holds? (x ≀ y) | holds? (y ≀ x)
    ... | yes x≀y | yes y≀x = yes (≀-antisym x≀y y≀x)
    ... | yes x≀y | no Β¬y≀x = no Ξ» x=y β†’ Β¬y≀x (≀-refl' (sym x=y))
    ... | no Β¬x≀y | _       = no Ξ» x=y β†’ Β¬x≀y (≀-refl' x=y)

Note that, if we have a decidable order, then the requirement of totality can be weakened to the property that, for any we have

which we refer to as weak totality.

  from-not-≀ : βˆ€ {x y} β†’ Β¬ (x ≀ y) β†’ y ≀ x
  from-not-≀ {x} {y} Β¬x≀y with compare x y
  ... | inl x≀y = absurd (Β¬x≀y x≀y)
  ... | inr y≀x = y≀x

module _ {o β„“} {P : Poset o β„“} ⦃ _ : Discrete ⌞ P ⌟ ⦄ ⦃ _ : is-decidable-poset P ⦄ where
  open Poset P

  from-weakly-total
    : (wk : βˆ€ {x y} β†’ Β¬ (x ≀ y) β†’ y ≀ x)
    β†’ is-decidable-total-order P
  from-weakly-total wk = record { has-is-total = tot } where

The construction is straightforward: we can test whether and if it holds, we’re done; Otherwise, weak totality lets us conclude that from the computed witness of 

    compare : βˆ€ x y β†’ (x ≀ y) ⊎ (y ≀ x)
    compare x y with holds? (x ≀ y)
    ... | yes x≀y = inl x≀y
    ... | no Β¬x≀y = inr (wk Β¬x≀y)

    tot : is-total-order P
    tot = record { compare = compare }