Added remaining flipped and negated relations to binary relation bundles (agda#2162)

Author: MatthewDaggitt

CHANGELOG.md

@@ -852,18 +852,24 @@ Non-backwards compatible changes
   IO.Instances
   ```
 
-### (Issue #2096) Introduction of flipped relation symbol for `Relation.Binary.Bundles.Preorder`
-
-* Previously, the relation symbol `_∼_`  was (notationally) symmetric, so that its
-  converse relation could only be discussed *semantically* in terms of `flip _∼_`
-  in `Relation.Binary.Properties.Preorder`, `Relation.Binary.Construct.Flip.{Ord|EqAndOrd}`
-
-* Now, the symbol `_∼_` has been renamed to a new symbol `_≲_`, with `_≳_`
-  introduced as a definition in `Relation.Binary.Bundles.Preorder` whose properties
-  in `Relation.Binary.Properties.Preorder` now refer to it. Partial backwards compatible
-  has been achieved by redeclaring a deprecated version of the old name in the record.
-  Therefore, only _declarations_ of `PartialOrder` records will need their field names
-  updating.
+### (Issue #2096) Introduction of flipped and negated relation symbols to bundles in `Relation.Binary.Bundles`
+
+* Previously, bundles such as `Preorder`, `Poset`, `TotalOrder` etc. did not have the flipped 
+  and negated versions of the operators exposed. In some cases they could obtained by opening the
+  relevant `Relation.Binary.Properties.X` file but usually they had to be redefined every time.
+  
+* To fix this, these bundles now all export all 4 versions of the operator: normal, converse, negated,
+  converse-negated. Accordingly they are no longer exported from the corresponding `Properties` file.
+
+* To make this work for `Preorder`, it was necessary to change the name of the relation symbol.
+  Previously, the symbol was `_∼_`  which is (notationally) symmetric, so that its
+  converse relation could only be discussed *semantically* in terms of `flip _∼_`.
+
+* Now, the `Preorder` record field `_∼_` has been renamed to `_≲_`, with `_≳_`
+  introduced as a definition in `Relation.Binary.Bundles.Preorder`. 
+  Partial backwards compatible has been achieved by redeclaring a deprecated version 
+  of the old symbol in the record. Therefore, only _declarations_ of `PartialOrder` records will 
+  need their field names updating.
 
 ### (Issue #1214) Reorganisation of the introduction of negated relation symbols under `Relation.Binary`
 

README/Design/Hierarchies.agda

@@ -249,6 +249,43 @@ record Semigroup : Set (suc (a ⊔ ℓ)) where
 -- differently, as a function with an unknown domain an codomain is
 -- of little use.
 
+-------------------------
+-- Bundle re-exporting --
+-------------------------
+
+-- In general ensuring that bundles re-export everything in their
+-- sub-bundles can get a little tricky.
+
+-- Imagine we have the following general scenario where bundle A is a
+-- direct refinement of bundle C (i.e. the record `IsA` has a `IsC` field)
+-- but is also morally a refinement of bundles B and D.
+
+--   Structures               Bundles
+--   ==========               =======
+--       IsA                     A
+--    /  ||   \               /  ||  \
+-- IsB   IsC   IsD          B    C    D
+ 
+-- The procedure for re-exports in the bundles is as follows:
+
+-- 1. `open IsA isA public using (IsC, M)` where `M` is everything
+--    exported by `IsA` that is not exported by `IsC`.
+
+-- 2. Construct `c : C` via the `isC` obtained in step 1.
+
+-- 3. `open C c public hiding (N)` where `N` is the list of fields
+--    shared by both `A` and `C`.
+
+-- 4. Construct `b : B` via the `isB` obtained in step 1.
+
+-- 5. `open B b public using (O)` where `O` is everything exported
+--    by `B` but not exported by `IsA`.
+ 
+-- 6. Construct `d : D` via the `isC` obtained in step 1.
+
+-- 7. `open D d public using (P)` where `P` is everything exported
+--    by `D` but not exported by `IsA`
+
 ------------------------------------------------------------------------
 -- Other hierarchy modules
 ------------------------------------------------------------------------

src/Algebra/Lattice/Properties/Semilattice.agda

@@ -27,8 +27,8 @@ import Relation.Binary.Construct.NaturalOrder.Left _≈_ _∧_
 poset : Poset c ℓ ℓ
 poset = LeftNaturalOrder.poset isSemilattice
 
-open Poset poset using (_≤_; isPartialOrder)
-open PosetProperties poset using (_≥_; ≥-isPartialOrder)
+open Poset poset using (_≤_; _≥_; isPartialOrder)
+open PosetProperties poset using (≥-isPartialOrder)
 
 ------------------------------------------------------------------------
 -- Every algebraic semilattice can be turned into an order-theoretic one.

src/Data/Product/Relation/Binary/Lex/Strict.agda

@@ -240,7 +240,7 @@ module _ {_≈₁_ : Rel A ℓ₁} {_<₁_ : Rel A ℓ₂}
                           (isEquivalence pre₁) (isEquivalence pre₂)
       ; reflexive     = ×-reflexive _≈₁_ _<₁_ _<₂_ (reflexive pre₂)
       ; trans         = ×-transitive {_<₂_ = _<₂_}
-                          (isEquivalence pre₁) (∼-resp-≈ pre₁)
+                          (isEquivalence pre₁) (≲-resp-≈ pre₁)
                           (trans pre₁) (trans pre₂)
       }
     where open IsPreorder

src/Relation/Binary/Bundles.agda

@@ -43,13 +43,15 @@ record Setoid c ℓ : Set (suc (c ⊔ ℓ)) where
     isEquivalence : IsEquivalence _≈_
 
   open IsEquivalence isEquivalence public
+    using (refl; reflexive; isPartialEquivalence)
 
   partialSetoid : PartialSetoid c ℓ
   partialSetoid = record
     { isPartialEquivalence = isPartialEquivalence
     }
 
-  open PartialSetoid partialSetoid public using (_≉_)
+  open PartialSetoid partialSetoid public
+    hiding (Carrier; _≈_; isPartialEquivalence)
 
 
 record DecSetoid c ℓ : Set (suc (c ⊔ ℓ)) where
@@ -60,14 +62,15 @@ record DecSetoid c ℓ : Set (suc (c ⊔ ℓ)) where
     isDecEquivalence : IsDecEquivalence _≈_
 
   open IsDecEquivalence isDecEquivalence public
+    using (_≟_; isEquivalence)
 
   setoid : Setoid c ℓ
   setoid = record
     { isEquivalence = isEquivalence
     }
 
-  open Setoid setoid public using (partialSetoid; _≉_)
-
+  open Setoid setoid public
+    hiding (Carrier; _≈_; isEquivalence)
 
 ------------------------------------------------------------------------
 -- Preorders
@@ -99,6 +102,9 @@ record Preorder c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
   infix 4 _≳_
   _≳_ = flip _≲_
 
+  infix 4 _⋧_
+  _⋧_ = flip _⋦_
+
   -- Deprecated.
   infix 4 _∼_
   _∼_ = _≲_
@@ -117,14 +123,15 @@ record TotalPreorder c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
     isTotalPreorder : IsTotalPreorder _≈_ _≲_
 
   open IsTotalPreorder isTotalPreorder public
-    hiding (module Eq)
+    using (total; isPreorder)
 
   preorder : Preorder c ℓ₁ ℓ₂
-  preorder = record { isPreorder = isPreorder }
+  preorder = record
+    { isPreorder = isPreorder
+    }
 
   open Preorder preorder public
-    using (module Eq; _≳_; _⋦_)
-
+    hiding (Carrier; _≈_; _≲_; isPreorder)
 
 ------------------------------------------------------------------------
 -- Partial orders
@@ -139,16 +146,21 @@ record Poset c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
     isPartialOrder : IsPartialOrder _≈_ _≤_
 
   open IsPartialOrder isPartialOrder public
-    hiding (module Eq)
+    using (antisym; isPreorder)
 
   preorder : Preorder c ℓ₁ ℓ₂
   preorder = record
     { isPreorder = isPreorder
     }
 
   open Preorder preorder public
-    using (module Eq)
-    renaming (_⋦_ to _≰_)
+    hiding (Carrier; _≈_; _≲_; isPreorder)
+    renaming
+    ( _⋦_ to _≰_; _≳_ to _≥_; _⋧_ to _≱_
+    ; ≲-respˡ-≈ to ≤-respˡ-≈
+    ; ≲-respʳ-≈ to ≤-respʳ-≈
+    ; ≲-resp-≈  to ≤-resp-≈
+    )
 
 
 record DecPoset c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
@@ -159,17 +171,18 @@ record DecPoset c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
     _≤_               : Rel Carrier ℓ₂
     isDecPartialOrder : IsDecPartialOrder _≈_ _≤_
 
-  private
-    module DPO = IsDecPartialOrder isDecPartialOrder
-  open DPO public hiding (module Eq)
+  private module DPO = IsDecPartialOrder isDecPartialOrder
+
+  open DPO public
+    using (_≟_; _≤?_; isPartialOrder)
 
   poset : Poset c ℓ₁ ℓ₂
   poset = record
     { isPartialOrder = isPartialOrder
     }
 
   open Poset poset public
-    using (preorder; _≰_)
+    hiding (Carrier; _≈_; _≤_; isPartialOrder; module Eq)
 
   module Eq where
     decSetoid : DecSetoid c ℓ₁
@@ -203,6 +216,12 @@ record StrictPartialOrder c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂))
   _≮_ : Rel Carrier _
   x ≮ y = ¬ (x < y)
 
+  infix 4 _>_
+  _>_ = flip _<_
+
+  infix 4 _≯_
+  _≯_ = flip _≮_
+
 
 record DecStrictPartialOrder c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
   infix 4 _≈_ _<_
@@ -212,17 +231,18 @@ record DecStrictPartialOrder c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂
     _<_                     : Rel Carrier ℓ₂
     isDecStrictPartialOrder : IsDecStrictPartialOrder _≈_ _<_
 
-  private
-    module DSPO = IsDecStrictPartialOrder isDecStrictPartialOrder
-  open DSPO public hiding (module Eq)
+  private module DSPO = IsDecStrictPartialOrder isDecStrictPartialOrder
+
+  open DSPO public
+    using (_<?_; _≟_; isStrictPartialOrder)
 
   strictPartialOrder : StrictPartialOrder c ℓ₁ ℓ₂
   strictPartialOrder = record
     { isStrictPartialOrder = isStrictPartialOrder
     }
 
   open StrictPartialOrder strictPartialOrder public
-    using (_≮_)
+    hiding (Carrier; _≈_; _<_; isStrictPartialOrder; module Eq)
 
   module Eq where
 
@@ -247,15 +267,15 @@ record TotalOrder c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
     isTotalOrder : IsTotalOrder _≈_ _≤_
 
   open IsTotalOrder isTotalOrder public
-    hiding (module Eq)
+    using (total; isPartialOrder; isTotalPreorder)
 
   poset : Poset c ℓ₁ ℓ₂
   poset = record
     { isPartialOrder = isPartialOrder
     }
 
   open Poset poset public
-    using (module Eq; preorder; _≰_)
+    hiding (Carrier; _≈_; _≤_; isPartialOrder)
 
   totalPreorder : TotalPreorder c ℓ₁ ℓ₂
   totalPreorder = record
@@ -271,17 +291,18 @@ record DecTotalOrder c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
     _≤_             : Rel Carrier ℓ₂
     isDecTotalOrder : IsDecTotalOrder _≈_ _≤_
 
-  private
-    module DTO = IsDecTotalOrder isDecTotalOrder
-  open DTO public hiding (module Eq)
+  private module DTO = IsDecTotalOrder isDecTotalOrder
+
+  open DTO public
+    using (_≟_; _≤?_; isTotalOrder; isDecPartialOrder)
 
   totalOrder : TotalOrder c ℓ₁ ℓ₂
   totalOrder = record
     { isTotalOrder = isTotalOrder
     }
 
   open TotalOrder totalOrder public
-    using (poset; preorder; _≰_)
+    hiding (Carrier; _≈_; _≤_; isTotalOrder; module Eq)
 
   decPoset : DecPoset c ℓ₁ ℓ₂
   decPoset = record
@@ -306,25 +327,37 @@ record StrictTotalOrder c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) wh
     isStrictTotalOrder : IsStrictTotalOrder _≈_ _<_
 
   open IsStrictTotalOrder isStrictTotalOrder public
-    hiding (module Eq)
+    using
+    ( _≟_; _<?_; compare; isStrictPartialOrder
+    ; isDecStrictPartialOrder; isDecEquivalence
+    )
 
   strictPartialOrder : StrictPartialOrder c ℓ₁ ℓ₂
   strictPartialOrder = record
     { isStrictPartialOrder = isStrictPartialOrder
     }
 
   open StrictPartialOrder strictPartialOrder public
-    using (module Eq; _≮_)
+    hiding (Carrier; _≈_; _<_; isStrictPartialOrder; module Eq)
+
+  decStrictPartialOrder : DecStrictPartialOrder c ℓ₁ ℓ₂
+  decStrictPartialOrder = record
+    { isDecStrictPartialOrder = isDecStrictPartialOrder
+    }
+
+  open DecStrictPartialOrder decStrictPartialOrder public
+    using (module Eq)
 
   decSetoid : DecSetoid c ℓ₁
   decSetoid = record
-    { isDecEquivalence = isDecEquivalence
+    { isDecEquivalence = Eq.isDecEquivalence
     }
   {-# WARNING_ON_USAGE decSetoid
   "Warning: decSetoid was deprecated in v1.3.
   Please use Eq.decSetoid instead."
   #-}
 
+
 record DenseLinearOrder c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
   infix 4 _≈_ _<_
   field
@@ -342,6 +375,7 @@ record DenseLinearOrder c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) wh
     }
 
   open StrictTotalOrder strictTotalOrder public
+    hiding (Carrier; _≈_; _<_; isStrictTotalOrder)
 
 
 ------------------------------------------------------------------------

src/Relation/Binary/Properties/DecTotalOrder.agda

@@ -26,8 +26,7 @@ open import Relation.Nullary.Negation using (¬_)
 
 open TotalOrderProperties public
   using
-  ( _≥_
-  ; ≥-refl
+  ( ≥-refl
   ; ≥-reflexive
   ; ≥-trans
   ; ≥-antisym

src/Relation/Binary/Properties/Poset.agda

@@ -30,11 +30,6 @@ open Eq using (_≉_)
 ------------------------------------------------------------------------
 -- The _≥_ relation is also a poset.
 
-infix 4 _≥_
-
-_≥_ : Rel A p₃
-x ≥ y = y ≤ x
-
 open PreorderProperties public
   using () renaming
   ( converse-isPreorder to ≥-isPreorder

src/Relation/Binary/Properties/TotalOrder.agda

@@ -39,8 +39,7 @@ decTotalOrder ≟ = record
 
 open PosetProperties public
   using
-  ( _≥_
-  ; ≥-refl
+  ( ≥-refl
   ; ≥-reflexive
   ; ≥-trans
   ; ≥-antisym
@@ -59,7 +58,7 @@ open PosetProperties public
   }
 
 open TotalOrder ≥-totalOrder public
-  using () renaming (total to ≥-total; _≰_ to _≱_)
+  using () renaming (total to ≥-total)
 
 ------------------------------------------------------------------------
 -- _<_ - the strict version is a strict partial order