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 }