diff --git a/CHANGELOG.md b/CHANGELOG.md index 3d99a6eb2b..ac64159887 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -621,7 +621,7 @@ Non-backwards compatible changes raw bundles to `Data.X.Base`, this definition can now be made directly. Knock-on consequences include the need to retain the old constructor name, now introduced as a pattern synonym, and introduction of (a function equivalent to) the former - field name/projection function `proof` as `≤″-proof` in `Data.Nat.Properties`. + field name/projection function `proof` as `≤″-proof` in `Data.Nat.Properties`. * Accordingly, the definition has been changed to: ```agda @@ -842,7 +842,6 @@ Non-backwards compatible changes IO.Effectful IO.Instances ``` - ### (Issue #2096) Introduction of flipped relation symbol for `Relation.Binary.Bundles.Preorder` * Previously, the relation symbol `_∼_` was (notationally) symmetric, so that its @@ -856,9 +855,25 @@ Non-backwards compatible changes Therefore, only _declarations_ of `PartialOrder` records will need their field names updating. -* NB (issues #1214 #2098) the corresponding situation regarding the `flip`ped - relation symbols `_≥_`, `_>_` (and their negated versions!) has not (yet) - been addressed. +### (Issue #1214) Reorganisation of the introduction of negated relation symbols under `Relation.Binary` + +* Previously, negated relation symbols `_≰_` (for `Poset`) and `_≮_` (`TotalOrder`) + were introduced in the corresponding `Relation.Binary.Properties` modules, for re-export. + +* Now they are introduced as definitions in the corresponding `Relation.Binary.Bundles`, + together with, for uniformity's sake, an additional negated symbol `_⋦_` for `Preorder`, + with their (obvious) intended semantics: + ```agda + infix 4 _⋦_ _≰_ _≮_ + Preorder._⋦_ : Rel Carrier _ + StrictPartialOrder._≮_ : Rel Carrier _ + ``` + Additionally, `Poset._≰_` is defined by renaming public export of `Preorder._⋦_` + +* Backwards compatibility has been maintained, with deprecated definitions in the + corresponding `Relation.Binary.Properties` modules, and the corresponding client + client module `import`s being adjusted accordingly. + ### Standardisation of `insertAt`/`updateAt`/`removeAt` @@ -879,12 +894,12 @@ Non-backwards compatible changes ``` _─_ ↦ removeAt ``` - + * In `Data.Vec.Base`: ```agda insert ↦ insertAt remove ↦ removeAt - + updateAt : Fin n → (A → A) → Vec A n → Vec A n ↦ updateAt : Vec A n → Fin n → (A → A) → Vec A n @@ -895,12 +910,12 @@ Non-backwards compatible changes remove : Fin (suc n) → Vector A (suc n) → Vector A n ↦ removeAt : Vector A (suc n) → Fin (suc n) → Vector A n - + updateAt : Fin n → (A → A) → Vector A n → Vector A n ↦ updateAt : Vector A n → Fin n → (A → A) → Vector A n ``` - + * The old names (and the names of all proofs about these functions) have been deprecated appropriately. ### Changes to triple reasoning interface @@ -1658,7 +1673,7 @@ Deprecated names take-drop-id ↦ take++drop≡id map-insert ↦ map-insertAt - + insert-lookup ↦ insertAt-lookup insert-punchIn ↦ insertAt-punchIn remove-PunchOut ↦ removeAt-punchOut @@ -1684,7 +1699,7 @@ Deprecated names updateAt-cong-relative ↦ updateAt-cong-local map-updateAt ↦ map-updateAt-local - + insert-lookup ↦ insertAt-lookup insert-punchIn ↦ insertAt-punchIn remove-punchOut ↦ removeAt-punchOut @@ -1742,11 +1757,6 @@ Deprecated names fromForeign ↦ Foreign.Haskell.Coerce.coerce ``` -* In `Relation.Binary.Bundles.Preorder`: - ``` - _∼_ ↦ _≲_ - ``` - * In `Relation.Binary.Indexed.Heterogeneous.Bundles.Preorder`: ``` _∼_ ↦ _≲_ @@ -1758,6 +1768,15 @@ Deprecated names invPreorder ↦ converse-preorder ``` +* Moved negated relation symbol from `Relation.Binary.Properties.Poset`: + ``` + _≰_ ↦ Relation.Binary.Bundles.Poset._≰_ + ``` + +* Moved negated relation symbol from `Relation.Binary.Properties.TotalOrder`: + ``` + _≮_ ↦ Relation.Binary.Bundles.StrictPartialOrder._≮_ + * In `Relation.Nullary.Decidable.Core`: ``` excluded-middle ↦ ¬¬-excluded-middle @@ -3300,9 +3319,9 @@ Additions to existing modules * Added new proofs to `Relation.Binary.Consequences`: ``` - sym⇒¬-sym : Symmetric _∼_ → Symmetric _≁_ - cotrans⇒¬-trans : Cotransitive _∼_ → Transitive _≁_ - irrefl⇒¬-refl : Reflexive _≈_ → Irreflexive _≈_ _∼_ → Reflexive _≁_ + sym⇒¬-sym : Symmetric _∼_ → Symmetric (¬_ ∘₂ _∼_) + cotrans⇒¬-trans : Cotransitive _∼_ → Transitive (¬_ ∘₂ _∼_) + irrefl⇒¬-refl : Reflexive _≈_ → Irreflexive _≈_ _∼_ → Reflexive (¬_ ∘₂ _∼_) mono₂⇒cong₂ : Symmetric ≈₁ → ≈₁ ⇒ ≤₁ → Antisymmetric ≈₂ ≤₂ → ∀ {f} → f Preserves₂ ≤₁ ⟶ ≤₁ ⟶ ≤₂ → f Preserves₂ ≈₁ ⟶ ≈₁ ⟶ ≈₂ diff --git a/src/Data/List/Sort/MergeSort.agda b/src/Data/List/Sort/MergeSort.agda index 9abab0823e..bded259428 100644 --- a/src/Data/List/Sort/MergeSort.agda +++ b/src/Data/List/Sort/MergeSort.agda @@ -21,7 +21,7 @@ open import Data.List.Relation.Binary.Permutation.Propositional import Data.List.Relation.Binary.Permutation.Propositional.Properties as Perm open import Data.Maybe.Base using (just) open import Relation.Nullary.Decidable using (does) -open import Data.Nat using (_<_; _>_; z_; z ; ≰⇒≥ ) -≮⇒≥ : ∀ {x y} → ¬ (x < y) → y ≤ x +≮⇒≥ : ∀ {x y} → x ≮ y → y ≤ x ≮⇒≥ = ToStrict.≮⇒≥ Eq.sym _≟_ reflexive total diff --git a/src/Relation/Binary/Properties/Poset.agda b/src/Relation/Binary/Properties/Poset.agda index add0e20b28..beb4ddc8aa 100644 --- a/src/Relation/Binary/Properties/Poset.agda +++ b/src/Relation/Binary/Properties/Poset.agda @@ -6,6 +6,7 @@ {-# OPTIONS --cubical-compatible --safe #-} +open import Data.Product.Base using (_,_) open import Function.Base using (flip; _∘_) open import Relation.Binary.Core using (Rel; _Preserves_⟶_) open import Relation.Binary.Bundles using (Poset; StrictPartialOrder) @@ -62,11 +63,6 @@ open Poset ≥-poset public ------------------------------------------------------------------------ -- Negated order -infix 4 _≰_ - -_≰_ : Rel A p₃ -x ≰ y = ¬ (x ≤ y) - ≰-respˡ-≈ : _≰_ Respectsˡ _≈_ ≰-respˡ-≈ x≈y = _∘ ≤-respˡ-≈ (Eq.sym x≈y) @@ -90,7 +86,7 @@ _<_ = ToStrict._<_ } open StrictPartialOrder <-strictPartialOrder public - using ( <-resp-≈; <-respʳ-≈; <-respˡ-≈) + using (_≮_; <-resp-≈; <-respʳ-≈; <-respˡ-≈) renaming ( irrefl to <-irrefl ; asym to <-asym @@ -103,10 +99,10 @@ open StrictPartialOrder <-strictPartialOrder public ≤∧≉⇒< : ∀ {x y} → x ≤ y → x ≉ y → x < y ≤∧≉⇒< = ToStrict.≤∧≉⇒< -<⇒≱ : ∀ {x y} → x < y → ¬ (y ≤ x) +<⇒≱ : ∀ {x y} → x < y → y ≰ x <⇒≱ = ToStrict.<⇒≱ antisym -≤⇒≯ : ∀ {x y} → x ≤ y → ¬ (y < x) +≤⇒≯ : ∀ {x y} → x ≤ y → y ≮ x ≤⇒≯ = ToStrict.≤⇒≯ antisym ------------------------------------------------------------------------ diff --git a/src/Relation/Binary/Properties/StrictPartialOrder.agda b/src/Relation/Binary/Properties/StrictPartialOrder.agda index 7420a2e24f..680323c770 100644 --- a/src/Relation/Binary/Properties/StrictPartialOrder.agda +++ b/src/Relation/Binary/Properties/StrictPartialOrder.agda @@ -17,7 +17,7 @@ import Relation.Binary.Construct.StrictToNonStrict open StrictPartialOrder SPO ------------------------------------------------------------------------ --- The inverse relation is also a strict partial order. +-- The converse relation is also a strict partial order. >-strictPartialOrder : StrictPartialOrder s₁ s₂ s₃ >-strictPartialOrder = EqAndOrd.strictPartialOrder SPO diff --git a/src/Relation/Binary/Properties/StrictTotalOrder.agda b/src/Relation/Binary/Properties/StrictTotalOrder.agda index f8b0062474..e6d34ab8d1 100644 --- a/src/Relation/Binary/Properties/StrictTotalOrder.agda +++ b/src/Relation/Binary/Properties/StrictTotalOrder.agda @@ -18,7 +18,7 @@ import Relation.Binary.Properties.StrictPartialOrder as SPO open import Relation.Binary.Consequences ------------------------------------------------------------------------ --- _<_ - the strict version is a strict total order +-- _<_ - the strict version is a decidable total order decTotalOrder : DecTotalOrder _ _ _ decTotalOrder = record diff --git a/src/Relation/Binary/Properties/TotalOrder.agda b/src/Relation/Binary/Properties/TotalOrder.agda index 540de19905..48f788ab7f 100644 --- a/src/Relation/Binary/Properties/TotalOrder.agda +++ b/src/Relation/Binary/Properties/TotalOrder.agda @@ -59,7 +59,7 @@ open PosetProperties public } open TotalOrder ≥-totalOrder public - using () renaming (total to ≥-total) + using () renaming (total to ≥-total; _≰_ to _≱_) ------------------------------------------------------------------------ -- _<_ - the strict version is a strict partial order @@ -90,8 +90,7 @@ open PosetProperties public open PosetProperties public using - ( _≰_ - ; ≰-respʳ-≈ + ( ≰-respʳ-≈ ; ≰-respˡ-≈ )