From 7e00c9219442dd8ccc29e0672cac116e8652f135 Mon Sep 17 00:00:00 2001 From: MatthewDaggitt Date: Sun, 22 Sep 2019 11:26:36 +0800 Subject: [PATCH] Standardised the binary relation hierarchy (#886) --- CHANGELOG.md | 5 + src/Algebra/Solver/Ring.agda | 2 +- src/Axiom/UniquenessOfIdentityProofs.agda | 1 + src/Category/Monad/Partiality.agda | 3 +- src/Data/Rational/Properties.agda | 2 +- src/Relation/Binary.agda | 440 +----------------- src/Relation/Binary/Consequences.agda | 1 + src/Relation/Binary/Core.agda | 242 +--------- src/Relation/Binary/Definitions.agda | 219 +++++++++ .../Binary/Indexed/Heterogeneous/Core.agda | 1 + src/Relation/Binary/Packages.agda | 245 ++++++++++ src/Relation/Binary/Properties/Setoid.agda | 27 +- .../Binary/PropositionalEquality.agda | 34 +- .../Binary/PropositionalEquality/Core.agda | 8 +- src/Relation/Binary/Structures.agda | 252 ++++++++++ src/Relation/Unary/Properties.agda | 3 +- 16 files changed, 786 insertions(+), 699 deletions(-) create mode 100644 src/Relation/Binary/Definitions.agda create mode 100644 src/Relation/Binary/Packages.agda create mode 100644 src/Relation/Binary/Structures.agda diff --git a/CHANGELOG.md b/CHANGELOG.md index a6c828e8b1..f3b841bbda 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -122,6 +122,11 @@ match the one for `Vec`: ``` +#### Other + +* The proofs `isPreorder` and `preorder` have been moved from the `Setoid` + record to the module `Relation.Binary.Properties.Setoid`. + New modules ----------- The following new modules have been added to the library: diff --git a/src/Algebra/Solver/Ring.agda b/src/Algebra/Solver/Ring.agda index 8752ba7944..32ca8600b4 100644 --- a/src/Algebra/Solver/Ring.agda +++ b/src/Algebra/Solver/Ring.agda @@ -19,7 +19,7 @@ open import Algebra open import Algebra.Solver.Ring.AlmostCommutativeRing -open import Relation.Binary.Core using (WeaklyDecidable) +open import Relation.Binary.Definitions using (WeaklyDecidable) module Algebra.Solver.Ring {r₁ r₂ r₃} diff --git a/src/Axiom/UniquenessOfIdentityProofs.agda b/src/Axiom/UniquenessOfIdentityProofs.agda index 91bdb5961b..f8d2904c7c 100644 --- a/src/Axiom/UniquenessOfIdentityProofs.agda +++ b/src/Axiom/UniquenessOfIdentityProofs.agda @@ -11,6 +11,7 @@ module Axiom.UniquenessOfIdentityProofs where open import Data.Empty open import Relation.Nullary hiding (Irrelevant) open import Relation.Binary.Core +open import Relation.Binary.Definitions open import Relation.Binary.PropositionalEquality.Core ------------------------------------------------------------------------ diff --git a/src/Category/Monad/Partiality.agda b/src/Category/Monad/Partiality.agda index fbc3dba0f8..98f7873ec6 100644 --- a/src/Category/Monad/Partiality.agda +++ b/src/Category/Monad/Partiality.agda @@ -18,6 +18,7 @@ open import Function.Core open import Function.Equivalence using (_⇔_; equivalence) open import Level using (_⊔_) open import Relation.Binary as B hiding (Rel) +import Relation.Binary.Properties.Setoid as SetoidProperties open import Relation.Binary.PropositionalEquality as P using (_≡_) open import Relation.Nullary open import Relation.Nullary.Decidable hiding (map) @@ -280,7 +281,7 @@ module _ {a ℓ} {A : Set a} {_∼_ : A → A → Set ℓ} where private preorder′ : IsEquivalence _∼_ → Kind → Preorder _ _ _ preorder′ equiv = - preorder (Setoid.isPreorder (record { isEquivalence = equiv })) + preorder (SetoidProperties.isPreorder (record { isEquivalence = equiv })) -- The two equalities are equivalence relations. diff --git a/src/Data/Rational/Properties.agda b/src/Data/Rational/Properties.agda index 0221417765..07535c48c6 100644 --- a/src/Data/Rational/Properties.agda +++ b/src/Data/Rational/Properties.agda @@ -62,7 +62,7 @@ mkℚ n₁ d₁ _ ≟ mkℚ n₂ d₂ _ with n₁ ℤ.≟ n₂ | d₁ ℕ.≟ d ≡⇒≃ refl = refl ≃⇒≡ : _≃_ ⇒ _≡_ -≃⇒≡ {i = mkℚ n₁ d₁ c₁} {j = mkℚ n₂ d₂ c₂} eq = helper +≃⇒≡ {x = mkℚ n₁ d₁ c₁} {y = mkℚ n₂ d₂ c₂} eq = helper where open ≡-Reasoning diff --git a/src/Relation/Binary.agda b/src/Relation/Binary.agda index 29e3e9814e..bac4d45d17 100644 --- a/src/Relation/Binary.agda +++ b/src/Relation/Binary.agda @@ -8,442 +8,10 @@ module Relation.Binary where -open import Agda.Builtin.Equality using (_≡_) -open import Data.Product -open import Data.Sum -open import Function.Core -open import Level -open import Relation.Nullary using (¬_) -import Relation.Binary.PropositionalEquality.Core as PropEq -open import Relation.Binary.Consequences - ------------------------------------------------------------------------ --- Simple properties and equivalence relations +-- Re-export various components of the binary relation hierarchy open import Relation.Binary.Core public - ------------------------------------------------------------------------- --- Preorders - -record IsPreorder {a ℓ₁ ℓ₂} {A : Set a} - (_≈_ : Rel A ℓ₁) -- The underlying equality. - (_∼_ : Rel A ℓ₂) -- The relation. - : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where - field - isEquivalence : IsEquivalence _≈_ - -- Reflexivity is expressed in terms of an 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ˡ-≈ - -record Preorder c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where - infix 4 _≈_ _∼_ - field - Carrier : Set c - _≈_ : Rel Carrier ℓ₁ -- The underlying equality. - _∼_ : Rel Carrier ℓ₂ -- The relation. - isPreorder : IsPreorder _≈_ _∼_ - - open IsPreorder isPreorder public - - ------------------------------------------------------------------------- --- Partial Setoids - --- Partial Equivalence relations are defined in Relation.Binary.Core. - -record PartialSetoid a ℓ : Set (suc (a ⊔ ℓ)) where - field - Carrier : Set a - _≈_ : Rel Carrier ℓ - isPartialEquivalence : IsPartialEquivalence _≈_ - - _≉_ : Rel Carrier _ - x ≉ y = ¬ (x ≈ y) - - open IsPartialEquivalence isPartialEquivalence public - ------------------------------------------------------------------------- --- Setoids - --- Equivalence relations are defined in Relation.Binary.Core. - -record Setoid c ℓ : Set (suc (c ⊔ ℓ)) where - infix 4 _≈_ - field - Carrier : Set c - _≈_ : Rel Carrier ℓ - isEquivalence : IsEquivalence _≈_ - - _≉_ : Rel Carrier _ - x ≉ y = ¬ (x ≈ y) - - open IsEquivalence isEquivalence public - - isPreorder : IsPreorder _≡_ _≈_ - isPreorder = record - { isEquivalence = PropEq.isEquivalence - ; reflexive = reflexive - ; trans = trans - } - - preorder : Preorder c c ℓ - preorder = record { isPreorder = isPreorder } - - partialSetoid : PartialSetoid c ℓ - partialSetoid = record - { isPartialEquivalence = isPartialEquivalence - } - ------------------------------------------------------------------------- --- Decidable equivalence relations - -record IsDecEquivalence {a ℓ} {A : Set a} - (_≈_ : Rel A ℓ) : Set (a ⊔ ℓ) where - infix 4 _≟_ - field - isEquivalence : IsEquivalence _≈_ - _≟_ : Decidable _≈_ - - open IsEquivalence isEquivalence public - -record DecSetoid c ℓ : Set (suc (c ⊔ ℓ)) where - infix 4 _≈_ - field - Carrier : Set c - _≈_ : Rel Carrier ℓ - isDecEquivalence : IsDecEquivalence _≈_ - - open IsDecEquivalence isDecEquivalence public - - setoid : Setoid c ℓ - setoid = record { isEquivalence = isEquivalence } - - open Setoid setoid public using (preorder) - ------------------------------------------------------------------------- --- Partial orders - -record IsPartialOrder {a ℓ₁ ℓ₂} {A : Set a} - (_≈_ : Rel A ℓ₁) (_≤_ : 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 Poset c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where - infix 4 _≈_ _≤_ - field - Carrier : Set c - _≈_ : Rel Carrier ℓ₁ - _≤_ : Rel Carrier ℓ₂ - isPartialOrder : IsPartialOrder _≈_ _≤_ - - open IsPartialOrder isPartialOrder public - - preorder : Preorder c ℓ₁ ℓ₂ - preorder = record { isPreorder = isPreorder } - ------------------------------------------------------------------------- --- Decidable partial orders - -record IsDecPartialOrder {a ℓ₁ ℓ₂} {A : Set a} - (_≈_ : Rel A ℓ₁) (_≤_ : Rel A ℓ₂) : - Set (a ⊔ ℓ₁ ⊔ ℓ₂) where - infix 4 _≟_ _≤?_ - field - isPartialOrder : IsPartialOrder _≈_ _≤_ - _≟_ : Decidable _≈_ - _≤?_ : Decidable _≤_ - - private - module PO = IsPartialOrder isPartialOrder - open PO public hiding (module Eq) - - module Eq where - - isDecEquivalence : IsDecEquivalence _≈_ - isDecEquivalence = record - { isEquivalence = PO.isEquivalence - ; _≟_ = _≟_ - } - - open IsDecEquivalence isDecEquivalence public - -record DecPoset c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where - infix 4 _≈_ _≤_ - field - Carrier : Set c - _≈_ : Rel Carrier ℓ₁ - _≤_ : Rel Carrier ℓ₂ - isDecPartialOrder : IsDecPartialOrder _≈_ _≤_ - - private - module DPO = IsDecPartialOrder isDecPartialOrder - open DPO public hiding (module Eq) - - poset : Poset c ℓ₁ ℓ₂ - poset = record { isPartialOrder = isPartialOrder } - - open Poset poset public using (preorder) - - module Eq where - - decSetoid : DecSetoid c ℓ₁ - decSetoid = record { isDecEquivalence = DPO.Eq.isDecEquivalence } - - open DecSetoid decSetoid public - ------------------------------------------------------------------------- --- Strict partial orders - -record IsStrictPartialOrder {a ℓ₁ ℓ₂} {A : Set a} - (_≈_ : Rel A ℓ₁) (_<_ : 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-≈ - - asymmetric = asym - {-# WARNING_ON_USAGE asymmetric - "Warning: asymmetric was deprecated in v0.16. - Please use asym instead." - #-} - -record StrictPartialOrder c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where - infix 4 _≈_ _<_ - field - Carrier : Set c - _≈_ : Rel Carrier ℓ₁ - _<_ : Rel Carrier ℓ₂ - isStrictPartialOrder : IsStrictPartialOrder _≈_ _<_ - - open IsStrictPartialOrder isStrictPartialOrder public - ------------------------------------------------------------------------- --- Decidable strict partial orders - -record IsDecStrictPartialOrder {a ℓ₁ ℓ₂} {A : Set a} - (_≈_ : Rel A ℓ₁) (_<_ : Rel A ℓ₂) : - Set (a ⊔ ℓ₁ ⊔ ℓ₂) where - infix 4 _≟_ _ : (¬a : ¬ A) (¬b : ¬ B) ( c : C) → Tri A B C - --- Trichotomy. - -Trichotomous : Rel A ℓ₁ → Rel A ℓ₂ → Set _ -Trichotomous _≈_ _<_ = ∀ x y → Tri (x < y) (x ≈ y) (x > y) - where _>_ = flip _<_ - --- Generalised maximum element. - -Max : REL A B ℓ → B → Set _ -Max _≤_ T = ∀ x → x ≤ T - --- Maximum element. - -Maximum : Rel A ℓ → A → Set _ -Maximum = Max - --- Generalised minimum element. - -Min : REL A B ℓ → A → Set _ -Min R = Max (flip R) - --- Minimum element. - -Minimum : Rel A ℓ → A → Set _ -Minimum = Min - --- Unary relations respecting a binary relation. - -_⟶_Respects_ : (A → Set ℓ₁) → (B → Set ℓ₂) → REL A B ℓ₃ → Set _ -P ⟶ Q Respects _∼_ = ∀ {x y} → x ∼ y → P x → Q y - --- Unary relation respects a binary relation. - -_Respects_ : (A → Set ℓ₁) → Rel A ℓ₂ → Set _ -P Respects _∼_ = P ⟶ P Respects _∼_ - --- Right respecting - relatedness is preserved on the right by equality. - -_Respectsʳ_ : REL A B ℓ₁ → Rel B ℓ₂ → Set _ -_∼_ Respectsʳ _≈_ = ∀ {x} → (x ∼_) Respects _≈_ - --- Left respecting - relatedness is preserved on the left by equality. - -_Respectsˡ_ : REL A B ℓ₁ → Rel A ℓ₂ → Set _ -P Respectsˡ _∼_ = ∀ {y} → (flip P y) Respects _∼_ - --- Respecting - relatedness is preserved on both sides by equality - -_Respects₂_ : Rel A ℓ₁ → Rel A ℓ₂ → Set _ -P Respects₂ _∼_ = (P Respectsʳ _∼_) × (P Respectsˡ _∼_) - --- Substitutivity - any two related elements satisfy exactly the same --- set of unary relations. Note that only the various derivatives --- of propositional equality can satisfy this property. - -Substitutive : Rel A ℓ₁ → (ℓ₂ : Level) → Set _ -Substitutive {A = A} _∼_ p = (P : A → Set p) → P Respects _∼_ - --- Decidability - it is possible to determine whether a given pair of --- elements are related. - -Decidable : REL A B ℓ → Set _ -Decidable _∼_ = ∀ x y → Dec (x ∼ y) - --- Weak decidability - it is sometimes possible to determine if a given --- pair of elements are related. - -WeaklyDecidable : REL A B ℓ → Set _ -WeaklyDecidable _∼_ = ∀ x y → Maybe (x ∼ y) - --- Irrelevancy - all proofs that a given pair of elements are related --- are indistinguishable. - -Irrelevant : REL A B ℓ → Set _ -Irrelevant _∼_ = ∀ {x y} (a b : x ∼ y) → a ≡ b - --- Recomputability - we can rebuild a relevant proof given an --- irrelevant one. - -Recomputable : REL A B ℓ → Set _ -Recomputable _∼_ = ∀ {x y} → .(x ∼ y) → x ∼ y - --- Universal - all pairs of elements are related - -Universal : REL A B ℓ → Set _ -Universal _∼_ = ∀ x y → x ∼ y - --- Non-emptiness - at least one pair of elements are related. - -record NonEmpty {A : Set a} {B : Set b} - (T : REL A B ℓ) : Set (a ⊔ b ⊔ ℓ) where - constructor nonEmpty - field - {x} : A - {y} : B - proof : T x y - ------------------------------------------------------------------------- --- Partial Equivalence relations - --- To preserve backwards compatability, equivalence relations are --- not defined in terms of their partial counterparts. - -record IsPartialEquivalence {A : Set a} (_≈_ : Rel A ℓ) : Set (a ⊔ ℓ) where - field - sym : Symmetric _≈_ - trans : Transitive _≈_ - ------------------------------------------------------------------------- --- Equivalence relations - --- 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. - --- This record is defined here instead of with the rest of the --- structures in `Relation.Binary` due to dependency cyles with --- `Relation.Binary.PropositionalEquality`. - -record IsEquivalence {A : Set a} (_≈_ : Rel A ℓ) : Set (a ⊔ ℓ) where - field - refl : Reflexive _≈_ - sym : Symmetric _≈_ - trans : Transitive _≈_ - - reflexive : _≡_ ⇒ _≈_ - reflexive ≡-refl = refl - - isPartialEquivalence : IsPartialEquivalence _≈_ - isPartialEquivalence = record - { sym = sym - ; trans = trans - } - - - ------------------------------------------------------------------------- --- DEPRECATED NAMES ------------------------------------------------------------------------- --- Please use the new names as continuing support for the old names is --- not guaranteed. - --- Version 1.1 - -Conn = Connex -{-# WARNING_ON_USAGE Conn -"Warning: Conn was deprecated in v1.1. -Please use Connex instead." -#-} +_∙_ Preserves₂ P ⟶ Q ⟶ R = ∀ {x y u v} → P x y → Q u v → R (x ∙ u) (y ∙ v) diff --git a/src/Relation/Binary/Definitions.agda b/src/Relation/Binary/Definitions.agda new file mode 100644 index 0000000000..68fcd1fea5 --- /dev/null +++ b/src/Relation/Binary/Definitions.agda @@ -0,0 +1,219 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Properties of binary relations +------------------------------------------------------------------------ + +-- Note that all the definitions in this file are re-exported by +-- `Relation.Binary`. + +{-# OPTIONS --without-K --safe #-} + +module Relation.Binary.Definitions where + +open import Agda.Builtin.Equality using (_≡_) + +open import Data.Maybe.Base using (Maybe) +open import Data.Product using (_×_) +open import Data.Sum.Base using (_⊎_) +open import Function.Core using (_on_; flip) +open import Level +open import Relation.Binary.Core +open import Relation.Nullary using (Dec; ¬_) + +private + variable + a b c ℓ ℓ₁ ℓ₂ ℓ₃ : Level + A : Set a + B : Set b + C : Set c + +------------------------------------------------------------------------ +-- Definitions +------------------------------------------------------------------------ + +-- Reflexivity - defined without an underlying equality. It could +-- alternatively be defined as `_≈_ ⇒ _∼_` for some equality `_≈_`. + +-- Confusingly the convention in the library is to use the name "refl" +-- for proofs of Reflexive and `reflexive` for proofs of type `_≈_ ⇒ _∼_`, +-- e.g. in the definition of `IsEquivalence` later in this file. This +-- convention is a legacy from the early days of the library. + +Reflexive : Rel A ℓ → Set _ +Reflexive _∼_ = ∀ {x} → x ∼ x + +-- Generalised symmetry. + +Sym : REL A B ℓ₁ → REL B A ℓ₂ → Set _ +Sym P Q = P ⇒ flip Q + +-- Symmetry. + +Symmetric : Rel A ℓ → Set _ +Symmetric _∼_ = Sym _∼_ _∼_ + +-- Generalised transitivity. + +Trans : REL A B ℓ₁ → REL B C ℓ₂ → REL A C ℓ₃ → Set _ +Trans P Q R = ∀ {i j k} → P i j → Q j k → R i k + +-- A flipped variant of generalised transitivity. + +TransFlip : REL A B ℓ₁ → REL B C ℓ₂ → REL A C ℓ₃ → Set _ +TransFlip P Q R = ∀ {i j k} → Q j k → P i j → R i k + +-- Transitivity. + +Transitive : Rel A ℓ → Set _ +Transitive _∼_ = Trans _∼_ _∼_ _∼_ + +-- Generalised antisymmetry + +Antisym : REL A B ℓ₁ → REL B A ℓ₂ → REL A B ℓ₃ → Set _ +Antisym R S E = ∀ {i j} → R i j → S j i → E i j + +-- Antisymmetry. + +Antisymmetric : Rel A ℓ₁ → Rel A ℓ₂ → Set _ +Antisymmetric _≈_ _≤_ = Antisym _≤_ _≤_ _≈_ + +-- Irreflexivity - this is defined terms of the underlying equality. + +Irreflexive : REL A B ℓ₁ → REL A B ℓ₂ → Set _ +Irreflexive _≈_ _<_ = ∀ {x y} → x ≈ y → ¬ (x < y) + +-- Asymmetry. + +Asymmetric : Rel A ℓ → Set _ +Asymmetric _<_ = ∀ {x y} → x < y → ¬ (y < x) + +-- Generalised connex - exactly one of the two relations holds. + +Connex : REL A B ℓ₁ → REL B A ℓ₂ → Set _ +Connex P Q = ∀ x y → P x y ⊎ Q y x + +-- Totality. + +Total : Rel A ℓ → Set _ +Total _∼_ = Connex _∼_ _∼_ + +-- Generalised trichotomy - exactly one of three types has a witness. + +data Tri (A : Set a) (B : Set b) (C : Set c) : Set (a ⊔ b ⊔ c) where + tri< : ( a : A) (¬b : ¬ B) (¬c : ¬ C) → Tri A B C + tri≈ : (¬a : ¬ A) ( b : B) (¬c : ¬ C) → Tri A B C + tri> : (¬a : ¬ A) (¬b : ¬ B) ( c : C) → Tri A B C + +-- Trichotomy. + +Trichotomous : Rel A ℓ₁ → Rel A ℓ₂ → Set _ +Trichotomous _≈_ _<_ = ∀ x y → Tri (x < y) (x ≈ y) (x > y) + where _>_ = flip _<_ + +-- Generalised maximum element. + +Max : REL A B ℓ → B → Set _ +Max _≤_ T = ∀ x → x ≤ T + +-- Maximum element. + +Maximum : Rel A ℓ → A → Set _ +Maximum = Max + +-- Generalised minimum element. + +Min : REL A B ℓ → A → Set _ +Min R = Max (flip R) + +-- Minimum element. + +Minimum : Rel A ℓ → A → Set _ +Minimum = Min + +-- Unary relations respecting a binary relation. + +_⟶_Respects_ : (A → Set ℓ₁) → (B → Set ℓ₂) → REL A B ℓ₃ → Set _ +P ⟶ Q Respects _∼_ = ∀ {x y} → x ∼ y → P x → Q y + +-- Unary relation respects a binary relation. + +_Respects_ : (A → Set ℓ₁) → Rel A ℓ₂ → Set _ +P Respects _∼_ = P ⟶ P Respects _∼_ + +-- Right respecting - relatedness is preserved on the right by equality. + +_Respectsʳ_ : REL A B ℓ₁ → Rel B ℓ₂ → Set _ +_∼_ Respectsʳ _≈_ = ∀ {x} → (x ∼_) Respects _≈_ + +-- Left respecting - relatedness is preserved on the left by equality. + +_Respectsˡ_ : REL A B ℓ₁ → Rel A ℓ₂ → Set _ +P Respectsˡ _∼_ = ∀ {y} → (flip P y) Respects _∼_ + +-- Respecting - relatedness is preserved on both sides by equality + +_Respects₂_ : Rel A ℓ₁ → Rel A ℓ₂ → Set _ +P Respects₂ _∼_ = (P Respectsʳ _∼_) × (P Respectsˡ _∼_) + +-- Substitutivity - any two related elements satisfy exactly the same +-- set of unary relations. Note that only the various derivatives +-- of propositional equality can satisfy this property. + +Substitutive : Rel A ℓ₁ → (ℓ₂ : Level) → Set _ +Substitutive {A = A} _∼_ p = (P : A → Set p) → P Respects _∼_ + +-- Decidability - it is possible to determine whether a given pair of +-- elements are related. + +Decidable : REL A B ℓ → Set _ +Decidable _∼_ = ∀ x y → Dec (x ∼ y) + +-- Weak decidability - it is sometimes possible to determine if a given +-- pair of elements are related. + +WeaklyDecidable : REL A B ℓ → Set _ +WeaklyDecidable _∼_ = ∀ x y → Maybe (x ∼ y) + +-- Irrelevancy - all proofs that a given pair of elements are related +-- are indistinguishable. + +Irrelevant : REL A B ℓ → Set _ +Irrelevant _∼_ = ∀ {x y} (a b : x ∼ y) → a ≡ b + +-- Recomputability - we can rebuild a relevant proof given an +-- irrelevant one. + +Recomputable : REL A B ℓ → Set _ +Recomputable _∼_ = ∀ {x y} → .(x ∼ y) → x ∼ y + +-- Universal - all pairs of elements are related + +Universal : REL A B ℓ → Set _ +Universal _∼_ = ∀ x y → x ∼ y + +-- Non-emptiness - at least one pair of elements are related. + +record NonEmpty {A : Set a} {B : Set b} + (T : REL A B ℓ) : Set (a ⊔ b ⊔ ℓ) where + constructor nonEmpty + field + {x} : A + {y} : B + proof : T x y + + + +------------------------------------------------------------------------ +-- DEPRECATED NAMES +------------------------------------------------------------------------ +-- Please use the new names as continuing support for the old names is +-- not guaranteed. + +-- Version 1.1 + +Conn = Connex +{-# WARNING_ON_USAGE Conn +"Warning: Conn was deprecated in v1.1. +Please use Connex instead." +#-} diff --git a/src/Relation/Binary/Indexed/Heterogeneous/Core.agda b/src/Relation/Binary/Indexed/Heterogeneous/Core.agda index 47e6519917..8f8ad6f98b 100644 --- a/src/Relation/Binary/Indexed/Heterogeneous/Core.agda +++ b/src/Relation/Binary/Indexed/Heterogeneous/Core.agda @@ -13,6 +13,7 @@ module Relation.Binary.Indexed.Heterogeneous.Core where open import Level import Relation.Binary.Core as B +import Relation.Binary.Definitions as B import Relation.Binary.PropositionalEquality.Core as P ------------------------------------------------------------------------ diff --git a/src/Relation/Binary/Packages.agda b/src/Relation/Binary/Packages.agda new file mode 100644 index 0000000000..57b2f7e0e2 --- /dev/null +++ b/src/Relation/Binary/Packages.agda @@ -0,0 +1,245 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Packages for homogeneous binary relations +------------------------------------------------------------------------ + +-- Note that the definitions in this file are all re-exported by +-- `Relation.Binary`. + +{-# OPTIONS --without-K --safe #-} + +module Relation.Binary.Packages where + +open import Level +open import Relation.Nullary using (¬_) +open import Relation.Binary.Core +open import Relation.Binary.Definitions +open import Relation.Binary.Structures + +------------------------------------------------------------------------ +-- Setoids +------------------------------------------------------------------------ + +record PartialSetoid a ℓ : Set (suc (a ⊔ ℓ)) where + field + Carrier : Set a + _≈_ : Rel Carrier ℓ + isPartialEquivalence : IsPartialEquivalence _≈_ + + open IsPartialEquivalence isPartialEquivalence public + + _≉_ : Rel Carrier _ + x ≉ y = ¬ (x ≈ y) + + +record Setoid c ℓ : Set (suc (c ⊔ ℓ)) where + infix 4 _≈_ + field + Carrier : Set c + _≈_ : Rel Carrier ℓ + isEquivalence : IsEquivalence _≈_ + + open IsEquivalence isEquivalence public + + _≉_ : Rel Carrier _ + x ≉ y = ¬ (x ≈ y) + + partialSetoid : PartialSetoid c ℓ + partialSetoid = record + { isPartialEquivalence = isPartialEquivalence + } + + +record DecSetoid c ℓ : Set (suc (c ⊔ ℓ)) where + infix 4 _≈_ + field + Carrier : Set c + _≈_ : Rel Carrier ℓ + isDecEquivalence : IsDecEquivalence _≈_ + + open IsDecEquivalence isDecEquivalence public + + setoid : Setoid c ℓ + setoid = record + { isEquivalence = isEquivalence + } + + +------------------------------------------------------------------------ +-- Preorders +------------------------------------------------------------------------ + +record Preorder c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where + infix 4 _≈_ _∼_ + field + Carrier : Set c + _≈_ : Rel Carrier ℓ₁ -- The underlying equality. + _∼_ : Rel Carrier ℓ₂ -- The relation. + isPreorder : IsPreorder _≈_ _∼_ + + open IsPreorder isPreorder public + + +------------------------------------------------------------------------ +-- Partial orders +------------------------------------------------------------------------ + +record Poset c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where + infix 4 _≈_ _≤_ + field + Carrier : Set c + _≈_ : Rel Carrier ℓ₁ + _≤_ : Rel Carrier ℓ₂ + isPartialOrder : IsPartialOrder _≈_ _≤_ + + open IsPartialOrder isPartialOrder public + + preorder : Preorder c ℓ₁ ℓ₂ + preorder = record + { isPreorder = isPreorder + } + + +record DecPoset c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where + infix 4 _≈_ _≤_ + field + Carrier : Set c + _≈_ : Rel Carrier ℓ₁ + _≤_ : Rel Carrier ℓ₂ + isDecPartialOrder : IsDecPartialOrder _≈_ _≤_ + + private + module DPO = IsDecPartialOrder isDecPartialOrder + open DPO public hiding (module Eq) + + poset : Poset c ℓ₁ ℓ₂ + poset = record + { isPartialOrder = isPartialOrder + } + + open Poset poset public using (preorder) + + module Eq where + + decSetoid : DecSetoid c ℓ₁ + decSetoid = record + { isDecEquivalence = DPO.Eq.isDecEquivalence + } + + open DecSetoid decSetoid public + + +record StrictPartialOrder c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where + infix 4 _≈_ _<_ + field + Carrier : Set c + _≈_ : Rel Carrier ℓ₁ + _<_ : Rel Carrier ℓ₂ + isStrictPartialOrder : IsStrictPartialOrder _≈_ _<_ + + open IsStrictPartialOrder isStrictPartialOrder public + + +record DecStrictPartialOrder c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where + infix 4 _≈_ _<_ + field + Carrier : Set c + _≈_ : Rel Carrier ℓ₁ + _<_ : Rel Carrier ℓ₂ + isDecStrictPartialOrder : IsDecStrictPartialOrder _≈_ _<_ + + private + module DSPO = IsDecStrictPartialOrder isDecStrictPartialOrder + open DSPO hiding (module Eq) + + strictPartialOrder : StrictPartialOrder c ℓ₁ ℓ₂ + strictPartialOrder = record + { isStrictPartialOrder = isStrictPartialOrder + } + + module Eq where + + decSetoid : DecSetoid c ℓ₁ + decSetoid = record + { isDecEquivalence = DSPO.Eq.isDecEquivalence + } + + open DecSetoid decSetoid public + + +------------------------------------------------------------------------ +-- Total orders +------------------------------------------------------------------------ + +record TotalOrder c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where + infix 4 _≈_ _≤_ + field + Carrier : Set c + _≈_ : Rel Carrier ℓ₁ + _≤_ : Rel Carrier ℓ₂ + isTotalOrder : IsTotalOrder _≈_ _≤_ + + open IsTotalOrder isTotalOrder public + + poset : Poset c ℓ₁ ℓ₂ + poset = record + { isPartialOrder = isPartialOrder + } + + open Poset poset public using (preorder) + + +record DecTotalOrder c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where + infix 4 _≈_ _≤_ + field + Carrier : Set c + _≈_ : Rel Carrier ℓ₁ + _≤_ : Rel Carrier ℓ₂ + isDecTotalOrder : IsDecTotalOrder _≈_ _≤_ + + private + module DTO = IsDecTotalOrder isDecTotalOrder + open DTO public hiding (module Eq) + + totalOrder : TotalOrder c ℓ₁ ℓ₂ + totalOrder = record + { isTotalOrder = isTotalOrder + } + + open TotalOrder totalOrder public using (poset; preorder) + + module Eq where + + decSetoid : DecSetoid c ℓ₁ + decSetoid = record + { isDecEquivalence = DTO.Eq.isDecEquivalence + } + + open DecSetoid decSetoid public + + +-- Note that these orders are decidable. The current implementation +-- of `Trichotomous` subsumes irreflexivity and asymmetry. Any reasonable +-- definition capturing these three properties implies decidability +-- as `Trichotomous` necessarily separates out the equality case. + +record StrictTotalOrder c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where + infix 4 _≈_ _<_ + field + Carrier : Set c + _≈_ : Rel Carrier ℓ₁ + _<_ : Rel Carrier ℓ₂ + isStrictTotalOrder : IsStrictTotalOrder _≈_ _<_ + + open IsStrictTotalOrder isStrictTotalOrder public + hiding (module Eq) + + strictPartialOrder : StrictPartialOrder c ℓ₁ ℓ₂ + strictPartialOrder = + record { isStrictPartialOrder = isStrictPartialOrder } + + decSetoid : DecSetoid c ℓ₁ + decSetoid = record { isDecEquivalence = isDecEquivalence } + + module Eq = DecSetoid decSetoid diff --git a/src/Relation/Binary/Properties/Setoid.agda b/src/Relation/Binary/Properties/Setoid.agda index 7ba504eb0e..83d927e9b4 100644 --- a/src/Relation/Binary/Properties/Setoid.agda +++ b/src/Relation/Binary/Properties/Setoid.agda @@ -10,17 +10,36 @@ open import Relation.Binary module Relation.Binary.Properties.Setoid {a ℓ} (S : Setoid a ℓ) where +open Setoid S + open import Function using (_∘_; _$_) open import Relation.Nullary using (¬_) +open import Relation.Binary.PropositionalEquality as P using (_≡_) + +------------------------------------------------------------------------------ +-- Every setoid is a preorder with respect to propositional equality -open Setoid S using (Carrier; _≈_; _≉_; refl; sym; trans) +isPreorder : IsPreorder _≡_ _≈_ +isPreorder = record + { isEquivalence = P.isEquivalence + ; reflexive = reflexive + ; trans = trans + } + +preorder : Preorder a a ℓ +preorder = record + { isPreorder = isPreorder + } + +------------------------------------------------------------------------------ +-- Properties of _≉_ ≉-sym : Symmetric _≉_ -≉-sym {x} {y} x≉y = x≉y ∘ sym +≉-sym x≉y = x≉y ∘ sym ≉-respˡ : _≉_ Respectsˡ _≈_ -≉-respˡ {y} {x} {x'} x≈x' x≉y = x≉y ∘ trans x≈x' +≉-respˡ x≈x' x≉y = x≉y ∘ trans x≈x' ≉-respʳ : _≉_ Respectsʳ _≈_ -≉-respʳ {x} {y} {y'} y≈y' x≉y = (λ x≈y' → x≉y $ trans x≈y' (sym y≈y')) +≉-respʳ y≈y' x≉y x≈y' = x≉y $ trans x≈y' (sym y≈y') diff --git a/src/Relation/Binary/PropositionalEquality.agda b/src/Relation/Binary/PropositionalEquality.agda index 23585e6501..5e76099988 100644 --- a/src/Relation/Binary/PropositionalEquality.agda +++ b/src/Relation/Binary/PropositionalEquality.agda @@ -55,6 +55,23 @@ cong₂ f refl refl = refl ------------------------------------------------------------------------ -- Structure of equality as a binary relation +isEquivalence : IsEquivalence {A = A} _≡_ +isEquivalence = record + { refl = refl + ; sym = sym + ; trans = trans + } + +isPreorder : IsPreorder {A = A} _≡_ _≡_ +isPreorder = record + { isEquivalence = isEquivalence + ; reflexive = id + ; trans = trans + } + +------------------------------------------------------------------------ +-- Packages for equality as a binary relation + setoid : Set a → Setoid _ _ setoid A = record { Carrier = A @@ -71,13 +88,6 @@ decSetoid dec = record } } -isPreorder : IsPreorder {A = A} _≡_ _≡_ -isPreorder = record - { isEquivalence = isEquivalence - ; reflexive = id - ; trans = trans - } - preorder : Set a → Preorder _ _ _ preorder A = record { Carrier = A @@ -207,13 +217,13 @@ cong-≡id {f = f} {x} f≡id = f≡id (f x) ∎ where open ≡-Reasoning; fx≡x = f≡id x; f²x≡x = f≡id (f x) -module _ (_≟_ : Decidable {A = A} _≡_) where +module _ (_≟_ : Decidable {A = A} _≡_) {x y : A} where - ≡-≟-identity : ∀ {x y : A} (eq : x ≡ y) → x ≟ y ≡ yes eq - ≡-≟-identity {x} {y} eq = dec-yes-irr (x ≟ y) (Decidable⇒UIP.≡-irrelevant _≟_) eq + ≡-≟-identity : (eq : x ≡ y) → x ≟ y ≡ yes eq + ≡-≟-identity eq = dec-yes-irr (x ≟ y) (Decidable⇒UIP.≡-irrelevant _≟_) eq - ≢-≟-identity : ∀ {x y : A} → x ≢ y → ∃ λ ¬eq → x ≟ y ≡ no ¬eq - ≢-≟-identity {x} {y} ¬eq = dec-no (x ≟ y) ¬eq + ≢-≟-identity : x ≢ y → ∃ λ ¬eq → x ≟ y ≡ no ¬eq + ≢-≟-identity ¬eq = dec-no (x ≟ y) ¬eq ------------------------------------------------------------------------ -- Any operation forms a magma over _≡_ diff --git a/src/Relation/Binary/PropositionalEquality/Core.agda b/src/Relation/Binary/PropositionalEquality/Core.agda index 2e98e2896a..7f322c92f3 100644 --- a/src/Relation/Binary/PropositionalEquality/Core.agda +++ b/src/Relation/Binary/PropositionalEquality/Core.agda @@ -15,6 +15,7 @@ open import Data.Product using (_,_) open import Function.Core using (_∘_) open import Level open import Relation.Binary.Core +open import Relation.Binary.Definitions open import Relation.Nullary using (¬_) private @@ -56,13 +57,6 @@ respʳ _∼_ refl x∼y = x∼y resp₂ : ∀ (∼ : Rel A ℓ) → ∼ Respects₂ _≡_ resp₂ _∼_ = respʳ _∼_ , respˡ _∼_ -isEquivalence : IsEquivalence {A = A} _≡_ -isEquivalence = record - { refl = refl - ; sym = sym - ; trans = trans - } - ------------------------------------------------------------------------ -- Various equality rearrangement lemmas diff --git a/src/Relation/Binary/Structures.agda b/src/Relation/Binary/Structures.agda new file mode 100644 index 0000000000..f735342f49 --- /dev/null +++ b/src/Relation/Binary/Structures.agda @@ -0,0 +1,252 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Structures for homogeneous binary relations +------------------------------------------------------------------------ + +-- Note that the definitions in this file are all re-exported by +-- `Relation.Binary`. + +{-# OPTIONS --without-K --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 using (proj₁; proj₂; _,_) +open import Level using (Level; _⊔_) +open import Relation.Nullary using (¬_) +open import Relation.Binary.PropositionalEquality.Core as P 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 P.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ˡ-≈ + +------------------------------------------------------------------------ +-- 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) + + 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-≈ + + asymmetric = asym + {-# WARNING_ON_USAGE asymmetric + "Warning: asymmetric was deprecated in v0.16. + Please use asym instead." + #-} + + +record IsDecStrictPartialOrder (_<_ : Rel A ℓ₂) : Set (a ⊔ ℓ ⊔ ℓ₂) where + infix 4 _≟_ _