open import 1Lab.Reflection hiding (absurd; [_])

open import 1Lab.Prelude
open import Data.Sum
open import Data.Dec

import Data.Nat as Nat

module StringLab.Order.Trichotomous where

Trichotomous orders🔗

In classical mathematics, there is no distinction between non-strict orders (EG: orders defined via $\le \text{)}$ and strict orders (EG: orders defined via $<\text{);}$ we can freely interchange between the two by taking $<$ to be $x\le y\wedge x\ne y$ or $x\le y$ to be $x<y\vee x=y\text{.}$

The situation is more complicated constructively. In particular, disjunctions are quite strong in constructive mathematics: not only do we know that one side of a disjunction is true, we have an algorithm that is able to tell us which side it is! This property is what lets us interpret proofs-as-programs and vice versa, but it does cause definitions to bifurcate. In particular, the statement $x<y\vee x=y$ is extremely strong constructively, as it means that we have an algorithm for deciding equality of a type.

Conversely, negations are much weaker constructively, as we do not have double-negation elimination. This makes it hard to “get out” from underneath a negation; from a computational perspective, a proof of $\neg A$ is a program that takes an element of $A$ and runs forever: it is very hard to extract information out of such a program! Turning our attention back to orders, strict orders are inherently about negation; this makes proofs of $x<y$ much easier to come by, but much less useful¹.

Though it may seem appealing to use the more general notion of order, we need to use the strongest one possible. In particular, we are writing programs that actually do computations, so they need to branch on whether or not two things are (in)equal! This means that we can ignore most of these constructivity questions, and chose the absolutely strongest form of order possible. This leads us to the following definition:

data Tri {o ℓ} {A : Type o} (_<_ : A → A → Type ℓ) (x y : A) : Type (o ⊔ ℓ) where
  lt : x < y → ¬ (x ≡ y) → ¬ (y < x) → Tri _<_ x y
  eq : ¬ (x < y) → x ≡ y → ¬ (y < x) → Tri _<_ x y
  gt : ¬ (x < y) → ¬ (x ≡ y) → y < x → Tri _<_ x y

record Trichotomous (o ℓ : Level) : Type (lsuc o ⊔ lsuc ℓ) where
  field
    Ob  : Type o
    _<_ : Ob → Ob → Type ℓ

    <-trans  : ∀ {x y z} → x < y → y < z → x < z
    <-tri    : ∀ x y → Tri _<_ x y

    <-is-prop : ∀ {x y} → is-prop (x < y)

This seemingly innocous definition is quite strong! First, note that we immediately have irreflexivity and asymmetry, as only one of $x<y\text{,}$ $x=y\text{,}$ or $y<x$ can be true.

  <-irrefl' : ∀ {x y} → x < y → x ≡ y → ⊥
  <-irrefl' {x} {y} x<y x=y with <-tri x y
  ... | lt _ x≠y _ = x≠y x=y
  ... | eq x≮y _ _ = x≮y x<y
  ... | gt _ x≠y _ = x≠y x=y

  <-irrefl : ∀ {x} → ¬ (x < x)
  <-irrefl x<x = <-irrefl' x<x refl

  <-asym : ∀ {x y} → x < y → y < x → ⊥
  <-asym x<y y<x = <-irrefl (<-trans x<y y<x)

Moreover, note that we can decide if $x<y\text{,}$ and we can decide equality (or, in other words, that the underlying type of the order is discrete).

  instance
    Discrete-Ob : Discrete Ob
    Discrete-Ob {x} {y} with <-tri x y
    ... | lt _ x≠y _ = no x≠y
    ... | eq _ x=y _ = yes x=y
    ... | gt _ x≠y _ = no x≠y

  instance
    Dec-< : ∀ {x y} → Dec (x < y)
    Dec-< {x} {y} with <-tri x y
    ... | lt x<y _ _ = yes x<y
    ... | eq _ x=y _ = no (flip <-irrefl' x=y)
    ... | gt _ _ y<x = no (<-asym y<x)

Hedberg’s theorem means that the underlying type of a trichotomous order must be a set.

  abstract
    Ob-is-set : is-set Ob
    Ob-is-set = Discrete→is-set Discrete-Ob

Weak linearity and connectivity are also immediate consequences of trichotomy.

  <-linear : ∀ {x z} → x < z → (y : Ob) → (x < y) ⊎ (y < z)
  <-linear {x} {z} x<z y with <-tri x y
  ... | lt x<y x₂ x₃ = inl x<y
  ... | eq _ x=y _ = inr (subst _ x=y x<z)
  ... | gt x≮y x≠y y<x = inr (<-trans y<x x<z)

  <-conn : ∀ {x y} → ¬ (x < y) → ¬ (y < x) → x ≡ y
  <-conn {x} {y} x≮y y≮x with <-tri x y
  ... | lt x<y _ _ = absurd (x≮y x<y)
  ... | eq _ x=y _ = x=y
  ... | gt _ _ y<x = absurd (y≮x y<x)

Earlier, we noted that $x<y\vee x=y$ is quite strong in constructive foundations. However, our earlier decidability results make this definition of $\le$ well-behaved.

  _≤_ : Ob → Ob → Type _
  x ≤ y = x < y ⊎ x ≡ y

  ≤-<-trans : ∀ {x y z} → x ≤ y → y < z → x < z
  ≤-<-trans {z = z} (inl x<y) y<z = <-trans x<y y<z
  ≤-<-trans {z = z} (inr x=y) y<z = subst (_< z) (sym x=y) y<z

  <-≤-trans : ∀ {x y z} → x < y → y ≤ z → x < z
  <-≤-trans {x = x} x<y (inl y<z) = <-trans x<y y<z
  <-≤-trans {x = x} x<y (inr y=z) = subst (x <_) y=z x<y

  ≤-trans : ∀ {x y z} → x ≤ y → y ≤ z → x ≤ z
  ≤-trans {z = z} (inr x=y) (inr y=z) = inr (x=y ∙ y=z)
  ≤-trans {z = z} (inr x=y) (inl y<z) = inl (subst (_< z) (sym x=y) y<z)
  ≤-trans {z = z} (inl x<y) y≤z = inl (<-≤-trans x<y y≤z)

  instance
    Dec-≤ : ∀ {x y} → Dec (x ≤ y)
    Dec-≤ {x} {y} with <-tri x y
    ... | lt x<y _ _ = yes (inl x<y)
    ... | eq _ x=y _ = yes (inr x=y)
    ... | gt _ _ y<x = no [ <-asym y<x , <-irrefl' y<x ∘ sym ]
    {-# OVERLAPS Dec-≤ #-}

In particular, negations of $\le$ give us proofs of $<\text{,}$ and vice versa.

  ¬≥→< : ∀ (x y : Ob) → ¬ (y ≤ x) → x < y
  ¬≥→< x y ¬y≤x with <-tri x y
  ... | lt x<y _ _ = x<y
  ... | eq _ x=y _ = absurd (¬y≤x (inr (sym x=y)))
  ... | gt _ _ y<x = absurd (¬y≤x (inl y<x))

  ¬>→≤ : ∀ (x y : Ob) → ¬ (y < x) → x ≤ y
  ¬>→≤ x y ¬y<x with <-tri x y
  ... | lt x<y _ _ = inl x<y
  ... | eq _ x=y _ = inr x=y
  ... | gt _ _ y<x = absurd (¬y<x y<x)

  <→¬≥ : ∀ (x y : Ob) → x < y → ¬ (y ≤ x)
  <→¬≥ x y x<y (inl y<x) = <-asym x<y y<x
  <→¬≥ x y x<y (inr y=x) = <-irrefl' x<y (sym y=x)

Max and min are also definable in every trichotomous order, so we have binary meets and binary joins.

  max : Ob → Ob → Ob
  max x y with <-tri x y
  ... | lt _ _ _ = y
  ... | eq _ _ _ = x
  ... | gt _ _ _ = x

  min : Ob → Ob → Ob
  min x y with <-tri x y
  ... | lt _ _ _ = x
  ... | eq _ _ _ = x
  ... | gt _ _ _ = y

  max-≤l : ∀ x y → x ≤ max x y
  max-≤l x y with <-tri x y
  ... | lt x<y _ _ = inl x<y
  ... | eq _ x=y _ = inr refl
  ... | gt _ _ y<x = inr refl

  max-≤r : ∀ x y → y ≤ max x y
  max-≤r x y with <-tri x y
  ... | lt x<y _ _ = inr refl
  ... | eq _ x=y _ = inr (sym x=y)
  ... | gt _ _ y<x = inl y<x

  max-lub : ∀ {x y z} → x ≤ z → y ≤ z → max x y ≤ z
  max-lub {x = x} {y = y} {z = z} x≤z y≤z with <-tri x y
  ... | lt x<y _ _ = y≤z
  ... | eq _ x=y _ = x≤z
  ... | gt _ _ y<x = x≤z

  min-≤l : ∀ x y → min x y ≤ x
  min-≤l x y with <-tri x y
  ... | lt x<y _ _ = inr refl
  ... | eq _ x=y _ = inr refl
  ... | gt _ _ y<x = inl y<x

  min-≤r : ∀ x y → min x y ≤ y
  min-≤r x y with <-tri x y
  ... | lt x<y _ _ = inl x<y
  ... | eq _ x=y _ = inr x=y
  ... | gt _ _ y<x = inr refl

  min-lub : ∀ {x y z} → z ≤ x → z ≤ y → z ≤ min x y
  min-lub {x = x} {y = y} {z = z} x≤z y≤z with <-tri x y
  ... | lt x<y _ _ = x≤z
  ... | eq _ x=y _ = x≤z
  ... | gt _ _ y<x = y≤z

open hlevel-projection

instance
  Underlying-Trichotomous : ∀ {o ℓ} → Underlying (Trichotomous o ℓ)
  Underlying-Trichotomous = record { ⌞_⌟ = Trichotomous.Ob }

  Trichotomous-ob-hlevel-proj : hlevel-projection (quote Trichotomous.Ob)
  Trichotomous-ob-hlevel-proj .has-level = quote Trichotomous.Ob-is-set
  Trichotomous-ob-hlevel-proj .get-level _ = pure (lit (nat ))
  Trichotomous-ob-hlevel-proj .get-argument (_ ∷ _ ∷ arg _ t ∷ _) = pure t
  {-# CATCHALL #-}
  Trichotomous-ob-hlevel-proj .get-argument _ = typeError []

  Trichotomous-<-hlevel-proj : hlevel-projection (quote Trichotomous._<_)
  Trichotomous-<-hlevel-proj .has-level = quote Trichotomous.<-is-prop
  Trichotomous-<-hlevel-proj .get-level _ = pure (lit (nat ))
  Trichotomous-<-hlevel-proj .get-argument (_ ∷ _ ∷ arg _ t ∷ _) = pure t
  {-# CATCHALL #-}
  Trichotomous-<-hlevel-proj .get-argument _ = typeError []

Examples🔗

The canonical example of a trichotomous order is the natural numbers.

Nat-trichotomous : Trichotomous lzero lzero
Nat-trichotomous .Trichotomous.Ob = Nat
Nat-trichotomous .Trichotomous._<_ = Nat._<_
Nat-trichotomous .Trichotomous.<-trans = Nat.<-trans _ _ _
Nat-trichotomous .Trichotomous.<-tri x y with holds? (x Nat.< y)
... | yes x<y = lt x<y (λ x=y → Nat.<-irrefl x=y x<y) (Nat.<-asym x<y)
... | no ¬x<y with holds? (y Nat.< x)
... | yes y<x = gt ¬x<y (λ x=y → Nat.<-irrefl (sym x=y) y<x) y<x
... | no ¬y<x = eq ¬x<y (Nat.≤-antisym (Nat.≤-from-not-< y x ¬y<x) (Nat.≤-from-not-< x y ¬x<y)) ¬y<x
Nat-trichotomous .Trichotomous.<-is-prop = Nat.≤-is-prop