------------------------------------------------------------------------
-- The Agda standard library
--
-- Structures for homogeneous binary relations
------------------------------------------------------------------------
 
-- The contents of this module should be accessed via `Relation.Binary`.
 
{-# OPTIONS --cubical-compatible --safe #-}
 
open import Relation.Binary.Core
 
module Relation.Binary.Structures
  {a ℓ} {A : Set a} -- The underlying set
  (_≈_ : Rel A ℓ)   -- The underlying equality relation
  where
 
open import Data.Product.Base using (proj₁; proj₂; _,_)
open import Level using (Level; _⊔_)
open import Relation.Nullary.Negation.Core using (¬_)
open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_)
open import Relation.Binary.Consequences
open import Relation.Binary.Definitions
 
private
  variable
    ℓ₂ : Level
 
------------------------------------------------------------------------
-- Equivalences
------------------------------------------------------------------------
-- Note all the following equivalences refer to the equality provided
-- as a module parameter at the top of this file.
 
record IsPartialEquivalence : Set (a ⊔ ℓ) where
  field
    sym   : Symmetric _≈_
    trans : Transitive _≈_
 
-- The preorders of this library are defined in terms of an underlying
-- equivalence relation, and hence equivalence relations are not
-- defined in terms of preorders.
 
-- To preserve backwards compatability, equivalence relations are
-- not defined in terms of their partial counterparts.
 
record IsEquivalence : Set (a ⊔ ℓ) where
  field
    refl  : Reflexive _≈_
    sym   : Symmetric _≈_
    trans : Transitive _≈_
 
  reflexive : _≡_ ⇒ _≈_
  reflexive ≡.refl = refl
 
  isPartialEquivalence : IsPartialEquivalence
  isPartialEquivalence = record
    { sym = sym
    ; trans = trans
    }
 
 
record IsDecEquivalence : Set (a ⊔ ℓ) where
  infix  _≟_
  field
    isEquivalence : IsEquivalence
    _≟_           : Decidable _≈_
 
  open IsEquivalence isEquivalence public
 
 
------------------------------------------------------------------------
-- Preorders
------------------------------------------------------------------------
 
record IsPreorder (_≲_ : Rel A ℓ₂) : Set (a ⊔ ℓ ⊔ ℓ₂) where
  field
    isEquivalence : IsEquivalence
    -- Reflexivity is expressed in terms of the underlying equality:
    reflexive     : _≈_ ⇒ _≲_
    trans         : Transitive _≲_
 
  module Eq = IsEquivalence isEquivalence
 
  refl : Reflexive _≲_
  refl = reflexive Eq.refl
 
  ≲-respˡ-≈ : _≲_ Respectsˡ _≈_
  ≲-respˡ-≈ x≈y x∼z = trans (reflexive (Eq.sym x≈y)) x∼z
 
  ≲-respʳ-≈ : _≲_ Respectsʳ _≈_
  ≲-respʳ-≈ x≈y z∼x = trans z∼x (reflexive x≈y)
 
  ≲-resp-≈ : _≲_ Respects₂ _≈_
  ≲-resp-≈ = ≲-respʳ-≈ , ≲-respˡ-≈
 
  ∼-respˡ-≈ = ≲-respˡ-≈
  {-# WARNING_ON_USAGE ∼-respˡ-≈
  "Warning: ∼-respˡ-≈ was deprecated in v2.0.
  Please use ≲-respˡ-≈ instead. "
  #-}
  ∼-respʳ-≈ = ≲-respʳ-≈
  {-# WARNING_ON_USAGE ∼-respʳ-≈
  "Warning: ∼-respʳ-≈ was deprecated in v2.0.
  Please use ≲-respʳ-≈ instead. "
  #-}
  ∼-resp-≈ = ≲-resp-≈
  {-# WARNING_ON_USAGE ∼-resp-≈
  "Warning: ∼-resp-≈ was deprecated in v2.0.
  Please use ≲-resp-≈ instead. "
  #-}
 
 
record IsTotalPreorder (_≲_ : Rel A ℓ₂) : Set (a ⊔ ℓ ⊔ ℓ₂) where
  field
    isPreorder : IsPreorder _≲_
    total      : Total _≲_
 
  open IsPreorder isPreorder public
 
 
------------------------------------------------------------------------
-- Partial orders
------------------------------------------------------------------------
 
record IsPartialOrder (_≤_ : Rel A ℓ₂) : Set (a ⊔ ℓ ⊔ ℓ₂) where
  field
    isPreorder : IsPreorder _≤_
    antisym    : Antisymmetric _≈_ _≤_
 
  open IsPreorder isPreorder public
    renaming
    ( ∼-respˡ-≈ to ≤-respˡ-≈
    ; ∼-respʳ-≈ to ≤-respʳ-≈
    ; ∼-resp-≈  to ≤-resp-≈
    )
 
 
record IsDecPartialOrder (_≤_ : Rel A ℓ₂) : Set (a ⊔ ℓ ⊔ ℓ₂) where
  infix  _≟_ _≤?_
  field
    isPartialOrder : IsPartialOrder _≤_
    _≟_            : Decidable _≈_
    _≤?_           : Decidable _≤_
 
  open IsPartialOrder isPartialOrder public
    hiding (module Eq)
 
  module Eq where
 
    isDecEquivalence : IsDecEquivalence
    isDecEquivalence = record
      { isEquivalence = isEquivalence
      ; _≟_           = _≟_
      }
 
    open IsDecEquivalence isDecEquivalence public
 
 
record IsStrictPartialOrder (_<_ : Rel A ℓ₂) : Set (a ⊔ ℓ ⊔ ℓ₂) where
  field
    isEquivalence : IsEquivalence
    irrefl        : Irreflexive _≈_ _<_
    trans         : Transitive _<_
    <-resp-≈      : _<_ Respects₂ _≈_
 
  module Eq = IsEquivalence isEquivalence
 
  asym : Asymmetric _<_
  asym {x} {y} = trans∧irr⇒asym Eq.refl trans irrefl {x = x} {y}
 
  <-respʳ-≈ : _<_ Respectsʳ _≈_
  <-respʳ-≈ = proj₁ <-resp-≈
 
  <-respˡ-≈ : _<_ Respectsˡ _≈_
  <-respˡ-≈ = proj₂ <-resp-≈
 
 
record IsDecStrictPartialOrder (_<_ : Rel A ℓ₂) : Set (a ⊔ ℓ ⊔ ℓ₂) where
  infix  _≟_ _<?_
  field
    isStrictPartialOrder : IsStrictPartialOrder _<_
    _≟_                  : Decidable _≈_
    _<?_                 : Decidable _<_
 
  private
    module SPO = IsStrictPartialOrder isStrictPartialOrder
 
  open SPO public hiding (module Eq)
 
  module Eq where
 
    isDecEquivalence : IsDecEquivalence
    isDecEquivalence = record
      { isEquivalence = SPO.isEquivalence
      ; _≟_           = _≟_
      }
 
    open IsDecEquivalence isDecEquivalence public
 
 
------------------------------------------------------------------------
-- Total orders
------------------------------------------------------------------------
 
record IsTotalOrder (_≤_ : Rel A ℓ₂) : Set (a ⊔ ℓ ⊔ ℓ₂) where
  field
    isPartialOrder : IsPartialOrder _≤_
    total          : Total _≤_
 
  open IsPartialOrder isPartialOrder public
 
  isTotalPreorder : IsTotalPreorder _≤_
  isTotalPreorder = record
    { isPreorder = isPreorder
    ; total      = total
    }
 
 
record IsDecTotalOrder (_≤_ : Rel A ℓ₂) : Set (a ⊔ ℓ ⊔ ℓ₂) where
  infix  _≟_ _≤?_
  field
    isTotalOrder : IsTotalOrder _≤_
    _≟_          : Decidable _≈_
    _≤?_         : Decidable _≤_
 
  open IsTotalOrder isTotalOrder public
    hiding (module Eq)
 
  isDecPartialOrder : IsDecPartialOrder _≤_
  isDecPartialOrder = record
    { isPartialOrder = isPartialOrder
    ; _≟_            = _≟_
    ; _≤?_           = _≤?_
    }
 
  module Eq where
 
    isDecEquivalence : IsDecEquivalence
    isDecEquivalence = record
      { isEquivalence = isEquivalence
      ; _≟_           = _≟_
      }
 
    open IsDecEquivalence isDecEquivalence public
 
 
-- Note that these orders are decidable. The current implementation
-- of `Trichotomous` subsumes irreflexivity and asymmetry. See
-- `Relation.Binary.Structures.Biased` for ways of constructing this
-- record without having to prove `isStrictPartialOrder`.
 
record IsStrictTotalOrder (_<_ : Rel A ℓ₂) : Set (a ⊔ ℓ ⊔ ℓ₂) where
  field
    isStrictPartialOrder : IsStrictPartialOrder _<_
    compare              : Trichotomous _≈_ _<_
 
  open IsStrictPartialOrder isStrictPartialOrder public
    hiding (module Eq)
 
  -- `Trichotomous` necessarily separates out the equality case so
  --  it implies decidability.
  infix  _≟_ _<?_
 
  _≟_ : Decidable _≈_
  _≟_ = tri⇒dec≈ compare
 
  _<?_ : Decidable _<_
  _<?_ = tri⇒dec< compare
 
  isDecStrictPartialOrder : IsDecStrictPartialOrder _<_
  isDecStrictPartialOrder = record
    { isStrictPartialOrder = isStrictPartialOrder
    ; _≟_                  = _≟_
    ; _<?_                 = _<?_
    }
 
  -- Redefine the `Eq` module to include decidability proofs
  module Eq where
 
    isDecEquivalence : IsDecEquivalence
    isDecEquivalence = record
      { isEquivalence = isEquivalence
      ; _≟_           = _≟_
      }
 
    open IsDecEquivalence isDecEquivalence public
 
  isDecEquivalence : IsDecEquivalence
  isDecEquivalence = record
    { isEquivalence = isEquivalence
    ; _≟_           = _≟_
    }
  {-# WARNING_ON_USAGE isDecEquivalence
  "Warning: isDecEquivalence was deprecated in v2.0.
  Please use Eq.isDecEquivalence instead. "
  #-}
 
record IsDenseLinearOrder (_<_ : Rel A ℓ₂) : Set (a ⊔ ℓ ⊔ ℓ₂) where
  field
    isStrictTotalOrder : IsStrictTotalOrder _<_
    dense              : Dense _<_
 
  open IsStrictTotalOrder isStrictTotalOrder public
 
 
------------------------------------------------------------------------
-- Apartness relations
------------------------------------------------------------------------
 
record IsApartnessRelation (_#_ : Rel A ℓ₂) : Set (a ⊔ ℓ ⊔ ℓ₂) where
  field
    irrefl  : Irreflexive _≈_ _#_
    sym     : Symmetric _#_
    cotrans : Cotransitive _#_
 
  _¬#_ : A → A → Set _
  x ¬# y = ¬ (x # y)