From 0cccb39f17232ce628c29c90467ad1739b1db7e8 Mon Sep 17 00:00:00 2001 From: jamesmckinna <31931406+jamesmckinna@users.noreply.github.com> Date: Thu, 23 Jan 2025 12:29:13 +0000 Subject: [PATCH] =?UTF-8?q?[=20refactor=20]=20rename=20`=E2=88=A3=E2=88=A3?= =?UTF-8?q?`=20to=20`=E2=88=A5`,=20`=E2=88=A4=E2=88=A4`=20to=20`=E2=88=A6`?= =?UTF-8?q?=20throughout=20`Algebra.Definitions.RawMagma`=20and=20`Algebra?= =?UTF-8?q?.Properties.*.Divisibility`=20(#2562)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit * refactor: rename `∣∣` to `∥`, `∤∤` to `∦` throughout * doc: added note to `style-guide` --- CHANGELOG.md | 30 +++++++ doc/style-guide.md | 5 +- src/Algebra/Definitions/RawMagma.agda | 35 ++++++-- .../Properties/Magma/Divisibility.agda | 79 ++++++++++++++----- .../Properties/Monoid/Divisibility.agda | 45 ++++++++--- .../Properties/Semigroup/Divisibility.agda | 21 ++++- 6 files changed, 176 insertions(+), 39 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index fc1ff57b1d..f16ed00b65 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -21,6 +21,36 @@ Deprecated modules Deprecated names ---------------- +* In `Algebra.Definitions.RawMagma`: + ```agda + _∣∣_ ↦ _∥_ + _∤∤_ ↦ _∦_ + ``` + +* In `Algebra.Properties.Magma.Divisibility`: + ```agda + ∣∣-sym ↦ ∥-sym + ∣∣-respˡ-≈ ↦ ∥-respˡ-≈ + ∣∣-respʳ-≈ ↦ ∥-respʳ-≈ + ∣∣-resp-≈ ↦ ∥-resp-≈ + ∤∤-sym -≈ ↦ ∦-sym + ∤∤-respˡ-≈ ↦ ∦-respˡ-≈ + ∤∤-respʳ-≈ ↦ ∦-respʳ-≈ + ∤∤-resp-≈ ↦ ∦-resp-≈ + ``` + +* In `Algebra.Properties.Monoid.Divisibility`: + ```agda + ∣∣-refl ↦ ∥-refl + ∣∣-reflexive ↦ ∥-reflexive + ∣∣-isEquivalence ↦ ∥-isEquivalence + ``` + +* In `Algebra.Properties.Semigroup.Divisibility`: + ```agda + ∣∣-trans ↦ ∥-trans + ``` + New modules ----------- diff --git a/doc/style-guide.md b/doc/style-guide.md index 6f19e064b2..7da14eb7f5 100644 --- a/doc/style-guide.md +++ b/doc/style-guide.md @@ -571,8 +571,9 @@ word within a compound word is capitalized except for the first word. * Likewise, standard infix symbols for eg, divisibility on numeric datatypes/algebraic structure, should be written `\|`, NOT the - unmarked `|` character. An exception to this is the *strict* - ordering relation, written using `<`, NOT `\<` as might be expected. + unmarked `|` character. Ditto. mutual divisibility `\||` etc. An + exception to this is the *strict* ordering relation, written using + `<`, NOT `\<` as might be expected. * Since v2.0, the `Algebra` hierarchy systematically introduces consistent symbolic notation for the negated versions of the usual diff --git a/src/Algebra/Definitions/RawMagma.agda b/src/Algebra/Definitions/RawMagma.agda index b8591e7ad2..bb4e67e39d 100644 --- a/src/Algebra/Definitions/RawMagma.agda +++ b/src/Algebra/Definitions/RawMagma.agda @@ -11,7 +11,7 @@ {-# OPTIONS --cubical-compatible --safe #-} open import Algebra.Bundles.Raw using (RawMagma) -open import Data.Product.Base using (_×_; ∃) +open import Data.Product.Base using (_×_) open import Level using (_⊔_) open import Relation.Binary.Core using (Rel) open import Relation.Nullary.Negation.Core using (¬_) @@ -25,7 +25,7 @@ open RawMagma M renaming (Carrier to A) ------------------------------------------------------------------------ -- Divisibility -infix 5 _∣ˡ_ _∤ˡ_ _∣ʳ_ _∤ʳ_ _∣_ _∤_ _∣∣_ _∤∤_ +infix 5 _∣ˡ_ _∤ˡ_ _∣ʳ_ _∤ʳ_ _∣_ _∤_ _∥_ _∦_ -- Divisibility from the left. -- @@ -34,7 +34,7 @@ infix 5 _∣ˡ_ _∤ˡ_ _∣ʳ_ _∤ʳ_ _∣_ _∤_ _∣∣_ _∤∤_ -- make the use of pattern synonyms more ergonomic (see #2216 for -- further details). The record field names are not designed to be -- used explicitly and indeed aren't re-exported publicly by --- `Algebra.X.Properties.Divisibility` modules. +-- `Algebra.Properties.X.Divisibility` modules. record _∣ˡ_ (x y : A) : Set (a ⊔ ℓ) where constructor _,_ @@ -79,8 +79,29 @@ x ∤ y = ¬ x ∣ y -- Example: for ℕ this is equivalent to x ≡ y, -- for ℤ this is equivalent to (x ≡ y or x ≡ - y). -_∣∣_ : Rel A (a ⊔ ℓ) -x ∣∣ y = x ∣ y × y ∣ x +_∥_ : Rel A (a ⊔ ℓ) +x ∥ y = x ∣ y × y ∣ x + +_∦_ : Rel A (a ⊔ ℓ) +x ∦ y = ¬ x ∥ y + + +------------------------------------------------------------------------ +-- DEPRECATED NAMES +------------------------------------------------------------------------ +-- Please use the new names as continuing support for the old names is +-- not guaranteed. + +-- Version 2.3 + +_∣∣_ = _∥_ +{-# WARNING_ON_USAGE _∣∣_ +"Warning: _∣∣_ was deprecated in v2.3. +Please use _∥_ instead." +#-} +_∤∤_ = _∦_ +{-# WARNING_ON_USAGE _∤∤_ +"Warning: _∤∤_ was deprecated in v2.3. +Please use _∦_ instead." +#-} -_∤∤_ : Rel A (a ⊔ ℓ) -x ∤∤ y = ¬ x ∣∣ y diff --git a/src/Algebra/Properties/Magma/Divisibility.agda b/src/Algebra/Properties/Magma/Divisibility.agda index aa9f4e53c5..d2e0091a12 100644 --- a/src/Algebra/Properties/Magma/Divisibility.agda +++ b/src/Algebra/Properties/Magma/Divisibility.agda @@ -21,7 +21,7 @@ open Magma M -- Re-export divisibility relations publicly open import Algebra.Definitions.RawMagma rawMagma public - using (_∣_; _∤_; _∣∣_; _∤∤_; _∣ˡ_; _∤ˡ_; _∣ʳ_; _∤ʳ_; _,_) + using (_∣_; _∤_; _∥_; _∦_; _∣ˡ_; _∤ˡ_; _∣ʳ_; _∤ʳ_; _,_) ------------------------------------------------------------------------ -- Properties of divisibility @@ -54,34 +54,34 @@ xy≈z⇒y∣z x y xy≈z = ∣-respʳ-≈ xy≈z (x∣yx y x) ∤-resp-≈ = ∤-respʳ-≈ , ∤-respˡ-≈ ------------------------------------------------------------------------ --- Properties of mutual divisibility _∣∣_ +-- Properties of mutual divisibility _∥_ -∣∣-sym : Symmetric _∣∣_ -∣∣-sym = swap +∥-sym : Symmetric _∥_ +∥-sym = swap -∣∣-respˡ-≈ : _∣∣_ Respectsˡ _≈_ -∣∣-respˡ-≈ x≈z (x∣y , y∣x) = ∣-respˡ-≈ x≈z x∣y , ∣-respʳ-≈ x≈z y∣x +∥-respˡ-≈ : _∥_ Respectsˡ _≈_ +∥-respˡ-≈ x≈z (x∣y , y∣x) = ∣-respˡ-≈ x≈z x∣y , ∣-respʳ-≈ x≈z y∣x -∣∣-respʳ-≈ : _∣∣_ Respectsʳ _≈_ -∣∣-respʳ-≈ y≈z (x∣y , y∣x) = ∣-respʳ-≈ y≈z x∣y , ∣-respˡ-≈ y≈z y∣x +∥-respʳ-≈ : _∥_ Respectsʳ _≈_ +∥-respʳ-≈ y≈z (x∣y , y∣x) = ∣-respʳ-≈ y≈z x∣y , ∣-respˡ-≈ y≈z y∣x -∣∣-resp-≈ : _∣∣_ Respects₂ _≈_ -∣∣-resp-≈ = ∣∣-respʳ-≈ , ∣∣-respˡ-≈ +∥-resp-≈ : _∥_ Respects₂ _≈_ +∥-resp-≈ = ∥-respʳ-≈ , ∥-respˡ-≈ ------------------------------------------------------------------------ -- Properties of mutual non-divisibility _∤∤_ -∤∤-sym : Symmetric _∤∤_ -∤∤-sym x∤∤y y∣∣x = contradiction (∣∣-sym y∣∣x) x∤∤y +∦-sym : Symmetric _∦_ +∦-sym x∦y y∥x = contradiction (∥-sym y∥x) x∦y -∤∤-respˡ-≈ : _∤∤_ Respectsˡ _≈_ -∤∤-respˡ-≈ x≈y x∤∤z y∣∣z = contradiction (∣∣-respˡ-≈ (sym x≈y) y∣∣z) x∤∤z +∦-respˡ-≈ : _∦_ Respectsˡ _≈_ +∦-respˡ-≈ x≈y x∦z y∥z = contradiction (∥-respˡ-≈ (sym x≈y) y∥z) x∦z -∤∤-respʳ-≈ : _∤∤_ Respectsʳ _≈_ -∤∤-respʳ-≈ x≈y z∤∤x z∣∣y = contradiction (∣∣-respʳ-≈ (sym x≈y) z∣∣y) z∤∤x +∦-respʳ-≈ : _∦_ Respectsʳ _≈_ +∦-respʳ-≈ x≈y z∦x z∥y = contradiction (∥-respʳ-≈ (sym x≈y) z∥y) z∦x -∤∤-resp-≈ : _∤∤_ Respects₂ _≈_ -∤∤-resp-≈ = ∤∤-respʳ-≈ , ∤∤-respˡ-≈ +∦-resp-≈ : _∦_ Respects₂ _≈_ +∦-resp-≈ = ∦-respʳ-≈ , ∦-respˡ-≈ ------------------------------------------------------------------------ @@ -107,3 +107,46 @@ Please use ∣-respʳ-≈ instead. " "Warning: ∣-resp was deprecated in v2.2. Please use ∣-resp-≈ instead. " #-} + +-- Version 2.3 + +∣∣-sym = ∥-sym +{-# WARNING_ON_USAGE ∣∣-sym +"Warning: ∣∣-sym was deprecated in v2.3. +Please use ∥-sym instead. " +#-} +∣∣-respˡ-≈ = ∥-respˡ-≈ +{-# WARNING_ON_USAGE ∣∣-respˡ-≈ +"Warning: ∣∣-respˡ-≈ was deprecated in v2.3. +Please use ∥-respˡ-≈ instead. " +#-} +∣∣-respʳ-≈ = ∥-respʳ-≈ +{-# WARNING_ON_USAGE ∣∣-respʳ-≈ +"Warning: ∣∣-respʳ-≈ was deprecated in v2.3. +Please use ∥-respʳ-≈ instead. " +#-} +∣∣-resp-≈ = ∥-resp-≈ +{-# WARNING_ON_USAGE ∣∣-resp-≈ +"Warning: ∣∣-resp-≈ was deprecated in v2.3. +Please use ∥-resp-≈ instead. " +#-} +∤∤-sym = ∦-sym +{-# WARNING_ON_USAGE ∤∤-sym +"Warning: ∤∤-sym was deprecated in v2.3. +Please use ∦-sym instead. " +#-} +∤∤-respˡ-≈ = ∦-respˡ-≈ +{-# WARNING_ON_USAGE ∤∤-respˡ-≈ +"Warning: ∤∤-respˡ-≈ was deprecated in v2.3. +Please use ∦-respˡ-≈ instead. " +#-} +∤∤-respʳ-≈ = ∦-respʳ-≈ +{-# WARNING_ON_USAGE ∤∤-respʳ-≈ +"Warning: ∤∤-respʳ-≈ was deprecated in v2.3. +Please use ∦-respʳ-≈ instead. " +#-} +∤∤-resp-≈ = ∦-resp-≈ +{-# WARNING_ON_USAGE ∤∤-resp-≈ +"Warning: ∤∤-resp-≈ was deprecated in v2.3. +Please use ∦-resp-≈ instead. " +#-} diff --git a/src/Algebra/Properties/Monoid/Divisibility.agda b/src/Algebra/Properties/Monoid/Divisibility.agda index c0f4c40af9..b081fbaa19 100644 --- a/src/Algebra/Properties/Monoid/Divisibility.agda +++ b/src/Algebra/Properties/Monoid/Divisibility.agda @@ -52,15 +52,42 @@ infix 4 ε∣_ ------------------------------------------------------------------------ -- Properties of mutual divisibiity -∣∣-refl : Reflexive _∣∣_ -∣∣-refl = ∣-refl , ∣-refl +∥-refl : Reflexive _∥_ +∥-refl = ∣-refl , ∣-refl -∣∣-reflexive : _≈_ ⇒ _∣∣_ -∣∣-reflexive x≈y = ∣-reflexive x≈y , ∣-reflexive (sym x≈y) +∥-reflexive : _≈_ ⇒ _∥_ +∥-reflexive x≈y = ∣-reflexive x≈y , ∣-reflexive (sym x≈y) -∣∣-isEquivalence : IsEquivalence _∣∣_ -∣∣-isEquivalence = record - { refl = λ {x} → ∣∣-refl {x} - ; sym = λ {x} {y} → ∣∣-sym {x} {y} - ; trans = λ {x} {y} {z} → ∣∣-trans {x} {y} {z} +∥-isEquivalence : IsEquivalence _∥_ +∥-isEquivalence = record + { refl = λ {x} → ∥-refl {x} + ; sym = λ {x} {y} → ∥-sym {x} {y} + ; trans = λ {x} {y} {z} → ∥-trans {x} {y} {z} } + + +------------------------------------------------------------------------ +-- DEPRECATED NAMES +------------------------------------------------------------------------ +-- Please use the new names as continuing support for the old names is +-- not guaranteed. + +-- Version 2.3 + +∣∣-refl = ∥-refl +{-# WARNING_ON_USAGE ∣∣-refl +"Warning: ∣∣-refl was deprecated in v2.3. +Please use ∥-refl instead. " +#-} + +∣∣-reflexive = ∥-reflexive +{-# WARNING_ON_USAGE ∣∣-reflexive +"Warning: ∣∣-reflexive was deprecated in v2.3. +Please use ∥-reflexive instead. " +#-} + +∣∣-isEquivalence = ∥-isEquivalence +{-# WARNING_ON_USAGE ∣∣-isEquivalence +"Warning: ∣∣-isEquivalence was deprecated in v2.3. +Please use ∥-isEquivalence instead. " +#-} diff --git a/src/Algebra/Properties/Semigroup/Divisibility.agda b/src/Algebra/Properties/Semigroup/Divisibility.agda index 76eaaa6edf..93616742c9 100644 --- a/src/Algebra/Properties/Semigroup/Divisibility.agda +++ b/src/Algebra/Properties/Semigroup/Divisibility.agda @@ -28,7 +28,22 @@ open import Algebra.Properties.Magma.Divisibility magma public q ∙ p , trans (assoc q p _) (trans (∙-congˡ px≈y) qy≈z) ------------------------------------------------------------------------ --- Properties of _∣∣_ +-- Properties of _∥_ -∣∣-trans : Transitive _∣∣_ -∣∣-trans (x∣y , y∣x) (y∣z , z∣y) = ∣-trans x∣y y∣z , ∣-trans z∣y y∣x +∥-trans : Transitive _∥_ +∥-trans (x∣y , y∣x) (y∣z , z∣y) = ∣-trans x∣y y∣z , ∣-trans z∣y y∣x + + +------------------------------------------------------------------------ +-- DEPRECATED NAMES +------------------------------------------------------------------------ +-- Please use the new names as continuing support for the old names is +-- not guaranteed. + +-- Version 2.3 + +∣∣-trans = ∥-trans +{-# WARNING_ON_USAGE ∣∣-trans +"Warning: ∣∣-trans was deprecated in v2.3. +Please use ∥-trans instead. " +#-}