------------------------------------------------------------------------ -- The Agda standard library -- -- Properties satisfied by total orders ------------------------------------------------------------------------ {-# OPTIONS --cubical-compatible --safe #-} open import Relation.Binary.Bundles using (TotalOrder; DecTotalOrder) open import Relation.Binary.Definitions using (Decidable) open import Relation.Binary.Structures using (IsTotalOrder) module Relation.Binary.Properties.TotalOrder {t₁ t₂ t₃} (T : TotalOrder t₁ t₂ t₃) where open TotalOrder T open import Data.Product.Base using (proj₁) open import Data.Sum.Base using (inj₁; inj₂) import Relation.Binary.Construct.Flip.EqAndOrd as EqAndOrd import Relation.Binary.Construct.NonStrictToStrict _≈_ _≤_ as ToStrict import Relation.Binary.Properties.Poset poset as PosetProperties open import Relation.Binary.Consequences ------------------------------------------------------------------------ -- Total orders are almost decidable total orders decTotalOrder : Decidable _≈_ → DecTotalOrder _ _ _ decTotalOrder ≟ = record { isDecTotalOrder = record { isTotalOrder = isTotalOrder ; _≟_ = ≟ ; _≤?_ = total∧dec⇒dec reflexive antisym total ≟ } } ------------------------------------------------------------------------ -- _≥_ - the flipped relation is also a total order open PosetProperties public using ( ≥-refl ; ≥-reflexive ; ≥-trans ; ≥-antisym ; ≥-isPreorder ; ≥-isPartialOrder ; ≥-preorder ; ≥-poset ) ≥-isTotalOrder : IsTotalOrder _≈_ _≥_ ≥-isTotalOrder = EqAndOrd.isTotalOrder isTotalOrder ≥-totalOrder : TotalOrder _ _ _ ≥-totalOrder = record { isTotalOrder = ≥-isTotalOrder } open TotalOrder ≥-totalOrder public using () renaming (total to ≥-total) ------------------------------------------------------------------------ -- _<_ - the strict version is a strict partial order -- Note that total orders can NOT be turned into strict total orders as -- in order to distinguish between the _≤_ and _<_ cases we must have -- decidable equality _≈_. open PosetProperties public using ( _<_ ; <-resp-≈ ; <-respʳ-≈ ; <-respˡ-≈ ; <-irrefl ; <-asym ; <-trans ; <-isStrictPartialOrder ; <-strictPartialOrder ; <⇒≉ ; ≤∧≉⇒< ; <⇒≱ ; ≤⇒≯ ) ------------------------------------------------------------------------ -- _≰_ - the negated order open PosetProperties public using ( ≰-respʳ-≈ ; ≰-respˡ-≈ ) ≰⇒> : ∀ {x y} → x ≰ y → y < x ≰⇒> = ToStrict.≰⇒> Eq.sym reflexive total ≰⇒≥ : ∀ {x y} → x ≰ y → y ≤ x ≰⇒≥ x≰y = proj₁ (≰⇒> x≰y)