------------------------------------------------------------------------
-- The Agda standard library
--
-- Properties satisfied by decidable total orders
------------------------------------------------------------------------

{-# OPTIONS --cubical-compatible --safe #-}

open import Relation.Binary.Bundles using (DecTotalOrder; StrictTotalOrder)

module Relation.Binary.Properties.DecTotalOrder
  {d₁ d₂ d₃} (DTO : DecTotalOrder d₁ d₂ d₃) where

import Relation.Binary.Construct.Flip.EqAndOrd as EqAndOrd
  using (isDecTotalOrder)
open import Relation.Binary.Structures
  using (IsDecTotalOrder; IsStrictTotalOrder)
open import Relation.Nullary.Negation.Core using (¬_)

open DecTotalOrder DTO hiding (trans)

import Relation.Binary.Properties.TotalOrder totalOrder as TotalOrderProperties
import Relation.Binary.Construct.NonStrictToStrict _≈_ _≤_ as ToStrict

------------------------------------------------------------------------
-- _≥_ - the flipped relation is also a total order

open TotalOrderProperties public
  using
  ( ≥-refl
  ; ≥-reflexive
  ; ≥-trans
  ; ≥-antisym
  ; ≥-total
  ; ≥-isPreorder
  ; ≥-isPartialOrder
  ; ≥-isTotalOrder
  ; ≥-preorder
  ; ≥-poset
  ; ≥-totalOrder
  )

≥-isDecTotalOrder : IsDecTotalOrder _≈_ _≥_
≥-isDecTotalOrder = EqAndOrd.isDecTotalOrder isDecTotalOrder

≥-decTotalOrder : DecTotalOrder _ _ _
≥-decTotalOrder = record
  { isDecTotalOrder = ≥-isDecTotalOrder
  }

open DecTotalOrder ≥-decTotalOrder public
  using () renaming (_≤?_ to _≥?_)

------------------------------------------------------------------------
-- _<_ - the strict version is a strict total order

open TotalOrderProperties public
  using
  ( _<_
  ; <-resp-≈
  ; <-respʳ-≈
  ; <-respˡ-≈
  ; <-irrefl
  ; <-asym
  ; <-trans
  ; <-isStrictPartialOrder
  ; <-strictPartialOrder
  ; <⇒≉
  ; ≤∧≉⇒<
  ; <⇒≱
  ; ≤⇒≯
  )

<-isStrictTotalOrder : IsStrictTotalOrder _≈_ _<_
<-isStrictTotalOrder = ToStrict.<-isStrictTotalOrder₂ isDecTotalOrder

<-strictTotalOrder : StrictTotalOrder _ _ _
<-strictTotalOrder = record
  { isStrictTotalOrder = <-isStrictTotalOrder
  }

open StrictTotalOrder <-strictTotalOrder public
  using (_≮_) renaming (compare to <-compare)

------------------------------------------------------------------------
-- _≰_ - the negated order

open TotalOrderProperties public
  using
  ( ≰-respʳ-≈
  ; ≰-respˡ-≈
  ; ≰⇒>
  ; ≰⇒≥
  )

≮⇒≥ : ∀ {x y} → x ≮ y → y ≤ x
≮⇒≥ = ToStrict.≮⇒≥ Eq.sym _≟_ reflexive total