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 $x, y$ results in $x \leq y,$ we can not, in general, turn this into a proof of $y \neq \leq x .$

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 $x \leq y,$ and, if that’s the case, then $min (x, y) = x;$ otherwise, $min (x, y) = y .$ The definition of $max$ 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 $x$ and $y$ proceed by doing the comparison again: this “unblocks” the computation of $min .$

  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 .decide 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 $x, y,$ we have

(x \neq \leq y) \to (y \leq x),

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 $x \leq y,$ and if it holds, we’re done; Otherwise, weak totality lets us conclude that $y \leq x$ from the computed witness of $x \neq \leq y .$

    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 }