------------------------------------------------------------------------ -- 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 using (tri⇒dec≈; tri⇒dec<; trans∧irr⇒asym) 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 4 _≟_ 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 record IsDecPreorder (_≲_ : Rel A ℓ₂) : Set (a ⊔ ℓ ⊔ ℓ₂) where field isPreorder : IsPreorder _≲_ _≟_ : Decidable _≈_ _≲?_ : Decidable _≲_ open IsPreorder isPreorder public hiding (module Eq) module Eq where isDecEquivalence : IsDecEquivalence isDecEquivalence = record { isEquivalence = isEquivalence ; _≟_ = _≟_ } open IsDecEquivalence isDecEquivalence 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 4 _≟_ _≤?_ field isPartialOrder : IsPartialOrder _≤_ _≟_ : Decidable _≈_ _≤?_ : Decidable _≤_ open IsPartialOrder isPartialOrder public hiding (module Eq) isDecPreorder : IsDecPreorder _≤_ isDecPreorder = record { isPreorder = isPreorder ; _≟_ = _≟_ ; _≲?_ = _≤?_ } open IsDecPreorder isDecPreorder public using (module Eq) 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 4 _≟_ _<?_ 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 4 _≟_ _≤?_ field isTotalOrder : IsTotalOrder _≤_ _≟_ : Decidable _≈_ _≤?_ : Decidable _≤_ open IsTotalOrder isTotalOrder public hiding (module Eq) isDecPartialOrder : IsDecPartialOrder _≤_ isDecPartialOrder = record { isPartialOrder = isPartialOrder ; _≟_ = _≟_ ; _≤?_ = _≤?_ } open IsDecPartialOrder isDecPartialOrder public using (isDecPreorder; module Eq) -- 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 4 _≟_ _<?_ _≟_ : 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)