Decidable total orders

Content created by Louis Wasserman, Fredrik Bakke, Egbert Rijke, Julian KG, fernabnor, louismntnu and malarbol.

Created on 2023-05-05.
Last modified on 2025-10-02.

module order-theory.decidable-total-orders where
Imports 
open import foundation.action-on-identifications-functions
open import foundation.binary-relations
open import foundation.coproduct-types
open import foundation.decidable-propositions
open import foundation.dependent-pair-types
open import foundation.empty-types
open import foundation.identity-types
open import foundation.logical-equivalences
open import foundation.propositions
open import foundation.sets
open import foundation.subtypes
open import foundation.transport-along-identifications
open import foundation.universe-levels

open import order-theory.decidable-posets
open import order-theory.decidable-total-preorders
open import order-theory.greatest-lower-bounds-posets
open import order-theory.join-semilattices
open import order-theory.least-upper-bounds-posets
open import order-theory.meet-semilattices
open import order-theory.posets
open import order-theory.preorders
open import order-theory.subposets
open import order-theory.total-orders

Idea

A decidable total order is a total order of which the inequality relation is decidable.

Definitions

The predicate on posets of being decidable total orders

is-decidable-total-prop-Poset : {l1 l2 : Level} → Poset l1 l2 → Prop (l1 ⊔ l2)
is-decidable-total-prop-Poset P =
  product-Prop (is-total-Poset-Prop P) (is-decidable-leq-prop-Poset P)

is-decidable-total-Poset : {l1 l2 : Level} → Poset l1 l2 → UU (l1 ⊔ l2)
is-decidable-total-Poset P = type-Prop (is-decidable-total-prop-Poset P)

is-prop-is-decidable-total-Poset :
  {l1 l2 : Level} (P : Poset l1 l2) → is-prop (is-decidable-total-Poset P)
is-prop-is-decidable-total-Poset P =
  is-prop-type-Prop (is-decidable-total-prop-Poset P)

The type of decidable total orders

Decidable-Total-Order : (l1 l2 : Level) → UU (lsuc l1 ⊔ lsuc l2)
Decidable-Total-Order l1 l2 = Σ (Poset l1 l2) (is-decidable-total-Poset)

module _
  {l1 l2 : Level} (P : Decidable-Total-Order l1 l2)
  where

  poset-Decidable-Total-Order : Poset l1 l2
  poset-Decidable-Total-Order = pr1 P

  is-total-poset-Decidable-Total-Order :
    is-total-Poset (poset-Decidable-Total-Order)
  is-total-poset-Decidable-Total-Order = pr1 (pr2 P)

  total-order-Decidable-Total-Order : Total-Order l1 l2
  total-order-Decidable-Total-Order =
    ( poset-Decidable-Total-Order ,
      is-total-poset-Decidable-Total-Order)

  is-decidable-poset-Decidable-Total-Order :
    is-decidable-leq-Poset (poset-Decidable-Total-Order)
  is-decidable-poset-Decidable-Total-Order = pr2 (pr2 P)

  type-Decidable-Total-Order : UU l1
  type-Decidable-Total-Order = type-Poset poset-Decidable-Total-Order

  leq-Decidable-Total-Order-Prop :
    (x y : type-Decidable-Total-Order) → Prop l2
  leq-Decidable-Total-Order-Prop = leq-prop-Poset poset-Decidable-Total-Order

  leq-Decidable-Total-Order :
    (x y : type-Decidable-Total-Order) → UU l2
  leq-Decidable-Total-Order = leq-Poset poset-Decidable-Total-Order

  is-prop-leq-Decidable-Total-Order :
    (x y : type-Decidable-Total-Order) →
    is-prop (leq-Decidable-Total-Order x y)
  is-prop-leq-Decidable-Total-Order =
    is-prop-leq-Poset poset-Decidable-Total-Order

  le-Decidable-Total-Order-Prop :
    (x y : type-Decidable-Total-Order) → Prop (l1 ⊔ l2)
  le-Decidable-Total-Order-Prop =
    le-prop-Poset poset-Decidable-Total-Order

  le-Decidable-Total-Order :
    (x y : type-Decidable-Total-Order) → UU (l1 ⊔ l2)
  le-Decidable-Total-Order =
    le-Poset poset-Decidable-Total-Order

  is-prop-le-Decidable-Total-Order :
    (x y : type-Decidable-Total-Order) →
    is-prop (le-Decidable-Total-Order x y)
  is-prop-le-Decidable-Total-Order =
    is-prop-le-Poset poset-Decidable-Total-Order

  decidable-poset-Decidable-Total-Order : Decidable-Poset l1 l2
  pr1 decidable-poset-Decidable-Total-Order = poset-Decidable-Total-Order
  pr2 decidable-poset-Decidable-Total-Order =
    is-decidable-poset-Decidable-Total-Order

  leq-total-decidable-poset-decidable-Prop :
    (x y : type-Decidable-Total-Order) → Decidable-Prop l2
  leq-total-decidable-poset-decidable-Prop =
    leq-decidable-poset-decidable-Prop decidable-poset-Decidable-Total-Order

  concatenate-eq-leq-Decidable-Total-Order :
    {x y z : type-Decidable-Total-Order} → x ＝ y →
    leq-Decidable-Total-Order y z → leq-Decidable-Total-Order x z
  concatenate-eq-leq-Decidable-Total-Order =
    concatenate-eq-leq-Poset poset-Decidable-Total-Order

  concatenate-leq-eq-Decidable-Total-Order :
    {x y z : type-Decidable-Total-Order} →
    leq-Decidable-Total-Order x y → y ＝ z → leq-Decidable-Total-Order x z
  concatenate-leq-eq-Decidable-Total-Order =
    concatenate-leq-eq-Poset poset-Decidable-Total-Order

  refl-leq-Decidable-Total-Order : is-reflexive leq-Decidable-Total-Order
  refl-leq-Decidable-Total-Order =
    refl-leq-Poset poset-Decidable-Total-Order

  transitive-leq-Decidable-Total-Order : is-transitive leq-Decidable-Total-Order
  transitive-leq-Decidable-Total-Order =
    transitive-leq-Poset poset-Decidable-Total-Order

  preorder-Decidable-Total-Order : Preorder l1 l2
  preorder-Decidable-Total-Order = preorder-Poset poset-Decidable-Total-Order

  decidable-total-preorder-Decidable-Total-Order :
    Decidable-Total-Preorder l1 l2
  pr1 decidable-total-preorder-Decidable-Total-Order =
    preorder-Decidable-Total-Order
  pr1 (pr2 decidable-total-preorder-Decidable-Total-Order) =
    is-total-poset-Decidable-Total-Order
  pr2 (pr2 decidable-total-preorder-Decidable-Total-Order) =
    is-decidable-poset-Decidable-Total-Order

  leq-or-strict-greater-Decidable-Poset :
    (x y : type-Decidable-Total-Order) → UU (l1 ⊔ l2)
  leq-or-strict-greater-Decidable-Poset =
    leq-or-strict-greater-Decidable-Preorder
      decidable-total-preorder-Decidable-Total-Order

  is-leq-or-strict-greater-Decidable-Total-Order :
    (x y : type-Decidable-Total-Order) →
    leq-or-strict-greater-Decidable-Poset x y
  is-leq-or-strict-greater-Decidable-Total-Order =
    is-leq-or-strict-greater-Decidable-Total-Preorder
      decidable-total-preorder-Decidable-Total-Order

  antisymmetric-leq-Decidable-Total-Order :
    (x y : type-Decidable-Total-Order) →
    leq-Decidable-Total-Order x y → leq-Decidable-Total-Order y x → Id x y
  antisymmetric-leq-Decidable-Total-Order =
    antisymmetric-leq-Poset poset-Decidable-Total-Order

  is-prop-leq-or-strict-greater-Decidable-Total-Order :
    (x y : type-Decidable-Total-Order) →
    is-prop (leq-or-strict-greater-Decidable-Poset x y)
  is-prop-leq-or-strict-greater-Decidable-Total-Order x y =
    is-prop-coproduct
      ( λ p q →
        pr1 q (inv (antisymmetric-leq-Decidable-Total-Order x y p (pr2 q))))
      ( is-prop-leq-Decidable-Total-Order x y)
      ( is-prop-le-Decidable-Total-Order y x)

  is-set-type-Decidable-Total-Order : is-set type-Decidable-Total-Order
  is-set-type-Decidable-Total-Order =
    is-set-type-Poset poset-Decidable-Total-Order

  set-Decidable-Total-Order : Set l1
  set-Decidable-Total-Order = set-Poset poset-Decidable-Total-Order

Properties

Any two elements in a decidable total order have a minimum and maximum

module _
  {l1 l2 : Level}
  (T : Decidable-Total-Order l1 l2)
  where

  min-Decidable-Total-Order :
    type-Decidable-Total-Order T → type-Decidable-Total-Order T →
    type-Decidable-Total-Order T
  min-Decidable-Total-Order =
    min-Total-Order (total-order-Decidable-Total-Order T)

  max-Decidable-Total-Order :
    type-Decidable-Total-Order T → type-Decidable-Total-Order T →
    type-Decidable-Total-Order T
  max-Decidable-Total-Order =
    max-Total-Order (total-order-Decidable-Total-Order T)

The binary minimum is the binary greatest lower bound

module _
  {l1 l2 : Level}
  (T : Decidable-Total-Order l1 l2)
  (x y : type-Decidable-Total-Order T)
  where

  min-is-greatest-binary-lower-bound-Decidable-Total-Order :
    is-greatest-binary-lower-bound-Poset
      ( poset-Decidable-Total-Order T)
      ( x)
      ( y)
      ( min-Decidable-Total-Order T x y)
  min-is-greatest-binary-lower-bound-Decidable-Total-Order =
    min-is-greatest-binary-lower-bound-Total-Order
      ( total-order-Decidable-Total-Order T)
      ( x)
      ( y)

  has-greatest-binary-lower-bound-Decidable-Total-Order :
    has-greatest-binary-lower-bound-Poset (poset-Decidable-Total-Order T) x y
  has-greatest-binary-lower-bound-Decidable-Total-Order =
    has-greatest-binary-lower-bound-Total-Order
      ( total-order-Decidable-Total-Order T)
      ( x)
      ( y)

The minimum of two values is a lower bound

module _
  {l1 l2 : Level}
  (T : Decidable-Total-Order l1 l2)
  (x y : type-Decidable-Total-Order T)
  where

  leq-left-min-Decidable-Total-Order :
    leq-Decidable-Total-Order T (min-Decidable-Total-Order T x y) x
  leq-left-min-Decidable-Total-Order =
    leq-left-min-Total-Order
      ( total-order-Decidable-Total-Order T)
      ( x)
      ( y)

  leq-right-min-Decidable-Total-Order :
    leq-Decidable-Total-Order T (min-Decidable-Total-Order T x y) y
  leq-right-min-Decidable-Total-Order =
    leq-right-min-Total-Order
      ( total-order-Decidable-Total-Order T)
      ( x)
      ( y)

The maximum of two values is their least upper bound

module _
  {l1 l2 : Level}
  (T : Decidable-Total-Order l1 l2)
  (x y : type-Decidable-Total-Order T)
  where

  max-is-least-binary-upper-bound-Decidable-Total-Order :
    is-least-binary-upper-bound-Poset
      ( poset-Decidable-Total-Order T)
      ( x)
      ( y)
      ( max-Decidable-Total-Order T x y)
  max-is-least-binary-upper-bound-Decidable-Total-Order =
    max-is-least-binary-upper-bound-Total-Order
      ( total-order-Decidable-Total-Order T)
      ( x)
      ( y)

  has-least-binary-upper-bound-Decidable-Total-Order :
    has-least-binary-upper-bound-Poset (poset-Decidable-Total-Order T) x y
  pr1 has-least-binary-upper-bound-Decidable-Total-Order =
    max-Decidable-Total-Order T x y
  pr2 has-least-binary-upper-bound-Decidable-Total-Order =
    max-is-least-binary-upper-bound-Decidable-Total-Order

The maximum of two values is an upper bound

module _
  {l1 l2 : Level}
  (T : Decidable-Total-Order l1 l2)
  (x y : type-Decidable-Total-Order T)
  where

  leq-left-max-Decidable-Total-Order :
    leq-Decidable-Total-Order T x (max-Decidable-Total-Order T x y)
  leq-left-max-Decidable-Total-Order =
    leq-left-max-Total-Order
      ( total-order-Decidable-Total-Order T)
      ( x)
      ( y)

  leq-right-max-Decidable-Total-Order :
    leq-Decidable-Total-Order T y (max-Decidable-Total-Order T x y)
  leq-right-max-Decidable-Total-Order =
    leq-right-max-Total-Order
      ( total-order-Decidable-Total-Order T)
      ( x)
      ( y)

The minimum of two values is less than or equal to their maximum

module _
  {l1 l2 : Level}
  (T : Decidable-Total-Order l1 l2)
  (x y : type-Decidable-Total-Order T)
  where

  abstract
    min-leq-max-Decidable-Total-Order :
      leq-Decidable-Total-Order T
        ( min-Decidable-Total-Order T x y)
        ( max-Decidable-Total-Order T x y)
    min-leq-max-Decidable-Total-Order =
      min-leq-max-Total-Order (total-order-Decidable-Total-Order T) x y

Decidable total orders are meet semilattices

module _
  {l1 l2 : Level}
  (T : Decidable-Total-Order l1 l2)
  where

  is-meet-semilattice-Decidable-Total-Order :
    is-meet-semilattice-Poset (poset-Decidable-Total-Order T)
  is-meet-semilattice-Decidable-Total-Order =
    is-meet-semilattice-Total-Order
      ( total-order-Decidable-Total-Order T)

  order-theoretic-meet-semilattice-Decidable-Total-Order :
    Order-Theoretic-Meet-Semilattice l1 l2
  order-theoretic-meet-semilattice-Decidable-Total-Order =
    order-theoretic-meet-semilattice-Total-Order
      ( total-order-Decidable-Total-Order T)

Decidable total orders are join semilattices

module _
  {l1 l2 : Level}
  (T : Decidable-Total-Order l1 l2)
  where

  is-join-semilattice-Decidable-Total-Order :
    is-join-semilattice-Poset (poset-Decidable-Total-Order T)
  is-join-semilattice-Decidable-Total-Order =
    is-join-semilattice-Total-Order
      ( total-order-Decidable-Total-Order T)

  order-theoretic-join-semilattice-Decidable-Total-Order :
    Order-Theoretic-Join-Semilattice l1 l2
  order-theoretic-join-semilattice-Decidable-Total-Order =
    order-theoretic-join-semilattice-Total-Order
      ( total-order-Decidable-Total-Order T)

The binary minimum operation is associative

module _
  {l1 l2 : Level}
  (T : Decidable-Total-Order l1 l2)
  where

  associative-min-Decidable-Total-Order :
    (x y z : type-Decidable-Total-Order T) →
    min-Decidable-Total-Order T (min-Decidable-Total-Order T x y) z ＝
    min-Decidable-Total-Order T x (min-Decidable-Total-Order T y z)
  associative-min-Decidable-Total-Order =
    associative-min-Total-Order
      ( total-order-Decidable-Total-Order T)

The binary maximum operation is associative

module _
  {l1 l2 : Level}
  (T : Decidable-Total-Order l1 l2)
  where

  associative-max-Decidable-Total-Order :
    (x y z : type-Decidable-Total-Order T) →
    max-Decidable-Total-Order T (max-Decidable-Total-Order T x y) z ＝
    max-Decidable-Total-Order T x (max-Decidable-Total-Order T y z)
  associative-max-Decidable-Total-Order =
    associative-max-Total-Order
      ( total-order-Decidable-Total-Order T)

The binary minimum operation is commutative

module _
  {l1 l2 : Level}
  (T : Decidable-Total-Order l1 l2)
  where

  commutative-min-Decidable-Total-Order :
    (x y : type-Decidable-Total-Order T) →
    min-Decidable-Total-Order T x y ＝ min-Decidable-Total-Order T y x
  commutative-min-Decidable-Total-Order =
    commutative-min-Total-Order
      ( total-order-Decidable-Total-Order T)

The binary maximum operation is commutative

module _
  {l1 l2 : Level}
  (T : Decidable-Total-Order l1 l2)
  where

  commutative-max-Decidable-Total-Order :
    (x y : type-Decidable-Total-Order T) →
    max-Decidable-Total-Order T x y ＝ max-Decidable-Total-Order T y x
  commutative-max-Decidable-Total-Order =
    commutative-max-Total-Order
      ( total-order-Decidable-Total-Order T)

The binary minimum operation is idempotent

module _
  {l1 l2 : Level}
  (T : Decidable-Total-Order l1 l2)
  where

  idempotent-min-Decidable-Total-Order :
    (x : type-Decidable-Total-Order T) →
    min-Decidable-Total-Order T x x ＝ x
  idempotent-min-Decidable-Total-Order =
    idempotent-min-Total-Order
      ( total-order-Decidable-Total-Order T)

The binary maximum operation is idempotent

module _
  {l1 l2 : Level}
  (T : Decidable-Total-Order l1 l2)
  where

  idempotent-max-Decidable-Total-Order :
    (x : type-Decidable-Total-Order T) →
    max-Decidable-Total-Order T x x ＝ x
  idempotent-max-Decidable-Total-Order =
    idempotent-max-Total-Order
      ( total-order-Decidable-Total-Order T)

If x is less than or equal to y, the minimum of x and y is x

module _
  {l1 l2 : Level}
  (T : Decidable-Total-Order l1 l2)
  where

  left-leq-right-min-Decidable-Total-Order :
    (x y : type-Decidable-Total-Order T) →
    leq-Decidable-Total-Order T x y → min-Decidable-Total-Order T x y ＝ x
  left-leq-right-min-Decidable-Total-Order =
    left-leq-right-min-Total-Order (total-order-Decidable-Total-Order T)

If y is less than or equal to x, the minimum of x and y is y

module _
  {l1 l2 : Level}
  (T : Decidable-Total-Order l1 l2)
  where

  right-leq-left-min-Decidable-Total-Order :
    (x y : type-Decidable-Total-Order T) →
    leq-Decidable-Total-Order T y x → min-Decidable-Total-Order T x y ＝ y
  right-leq-left-min-Decidable-Total-Order =
    right-leq-left-min-Total-Order (total-order-Decidable-Total-Order T)

If x is less than or equal to y, the maximum of x and y is y

module _
  {l1 l2 : Level}
  (T : Decidable-Total-Order l1 l2)
  where

  left-leq-right-max-Decidable-Total-Order :
    (x y : type-Decidable-Total-Order T) →
    leq-Decidable-Total-Order T x y → max-Decidable-Total-Order T x y ＝ y
  left-leq-right-max-Decidable-Total-Order =
    left-leq-right-max-Total-Order (total-order-Decidable-Total-Order T)

If y is less than or equal to x, the maximum of x and y is x

module _
  {l1 l2 : Level}
  (T : Decidable-Total-Order l1 l2)
  where

  right-leq-left-max-Decidable-Total-Order :
    (x y : type-Decidable-Total-Order T) →
    leq-Decidable-Total-Order T y x → max-Decidable-Total-Order T x y ＝ x
  right-leq-left-max-Decidable-Total-Order =
    right-leq-left-max-Total-Order (total-order-Decidable-Total-Order T)

If a ≤ b and c ≤ d, then min a c ≤ min b d

  min-leq-leq-Decidable-Total-Order :
    (a b c d : type-Decidable-Total-Order T) →
    leq-Decidable-Total-Order T a b → leq-Decidable-Total-Order T c d →
    leq-Decidable-Total-Order
      ( T)
      ( min-Decidable-Total-Order T a c)
      ( min-Decidable-Total-Order T b d)
  min-leq-leq-Decidable-Total-Order =
    min-leq-leq-Total-Order
      ( total-order-Decidable-Total-Order T)

If a ≤ b and c ≤ d, then max a c ≤ max b d

  max-leq-leq-Decidable-Total-Order :
    (a b c d : type-Decidable-Total-Order T) →
    leq-Decidable-Total-Order T a b → leq-Decidable-Total-Order T c d →
    leq-Decidable-Total-Order
      ( T)
      ( max-Decidable-Total-Order T a c)
      ( max-Decidable-Total-Order T b d)
  max-leq-leq-Decidable-Total-Order =
    max-leq-leq-Total-Order
      ( total-order-Decidable-Total-Order T)

Subsets of decidable total orders are decidable total orders

Decidable-Total-Suborder :
  {l1 l2 : Level} (l3 : Level) →
  Decidable-Total-Order l1 l2 →
  UU (l1 ⊔ lsuc l3)
Decidable-Total-Suborder l3 T =
  Subposet l3 (poset-Decidable-Total-Order T)

module _
  {l1 l2 l3 : Level}
  (T : Decidable-Total-Order l1 l2)
  (P : Decidable-Total-Suborder l3 T)
  where

  is-total-leq-Decidable-Total-Suborder :
    is-total-Poset
      (poset-Subposet (poset-Decidable-Total-Order T) P)
  is-total-leq-Decidable-Total-Suborder x y =
    is-total-poset-Decidable-Total-Order
      ( T)
      ( inclusion-subtype P x)
      ( inclusion-subtype P y)

  is-decidable-leq-Decidable-Total-Suborder :
    is-decidable-leq-Poset
      (poset-Subposet (poset-Decidable-Total-Order T) P)
  is-decidable-leq-Decidable-Total-Suborder x y =
    is-decidable-poset-Decidable-Total-Order
      ( T)
      ( inclusion-subtype P x)
      ( inclusion-subtype P y)

  decidable-total-order-Decidable-Total-Suborder :
    Decidable-Total-Order (l1 ⊔ l3) l2
  decidable-total-order-Decidable-Total-Suborder =
    poset-Subposet (poset-Decidable-Total-Order T) P ,
    is-total-leq-Decidable-Total-Suborder ,
    is-decidable-leq-Decidable-Total-Suborder

Recent changes