From e5d1f88fe5cf182186ec3a082c69ea599a2181d7 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Sat, 31 Aug 2024 11:10:46 +0100 Subject: [PATCH 1/4] fix #2306 --- CHANGELOG.md | 11 ++++++ .../Properties/Magma/Divisibility.agda | 35 +++++++++++++++++-- 2 files changed, 44 insertions(+), 2 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 57222329ef..df474147a9 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -48,6 +48,17 @@ New modules Additions to existing modules ----------------------------- +* Properties of non-divisibility in `Algebra.Properties.Magma.Divisibility`: + ```agda + ∤-respˡ : _∤_ Respectsˡ _≈_ + ∤-respʳ : _∤_ Respectsʳ _≈_ + ∤-resp : _∤_ Respects₂ _≈_ + ∤∤-sym : Symmetric _∤∤_ + ∤∤-respˡ : _∤∤_ Respectsˡ _≈_ + ∤∤-respʳ : _∤∤_ Respectsʳ _≈_ + ∤∤-resp : _∤∤_ Respects₂ _≈_ + ``` + * In `Data.List.Properties`: ```agda product≢0 : All NonZero ns → NonZero (product ns) diff --git a/src/Algebra/Properties/Magma/Divisibility.agda b/src/Algebra/Properties/Magma/Divisibility.agda index 629406faa1..7c9cbdccd3 100644 --- a/src/Algebra/Properties/Magma/Divisibility.agda +++ b/src/Algebra/Properties/Magma/Divisibility.agda @@ -7,11 +7,14 @@ {-# OPTIONS --cubical-compatible --safe #-} open import Algebra using (Magma) -open import Data.Product.Base using (_×_; _,_; ∃; map; swap) -open import Relation.Binary.Definitions module Algebra.Properties.Magma.Divisibility {a ℓ} (M : Magma a ℓ) where +open import Data.Product.Base using (_,_; swap) +open import Relation.Binary.Definitions + using (_Respects_; _Respectsˡ_; _Respectsʳ_; _Respects₂_; Symmetric) +open import Relation.Nullary.Negation.Core using (contradiction) + open Magma M ------------------------------------------------------------------------ @@ -38,6 +41,18 @@ x∣yx x y = y , refl xy≈z⇒y∣z : ∀ x y {z} → x ∙ y ≈ z → y ∣ z xy≈z⇒y∣z x y xy≈z = ∣-respʳ xy≈z (x∣yx y x) +------------------------------------------------------------------------ +-- Properties of non-divisibility + +∤-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 = ∤-respʳ , ∤-respˡ + ------------------------------------------------------------------------ -- Properties of mutual divisibility _∣∣_ @@ -52,3 +67,19 @@ xy≈z⇒y∣z x y xy≈z = ∣-respʳ xy≈z (x∣yx y x) ∣∣-resp-≈ : _∣∣_ Respects₂ _≈_ ∣∣-resp-≈ = ∣∣-respʳ-≈ , ∣∣-respˡ-≈ + +------------------------------------------------------------------------ +-- Properties of mutual non-divisibility _∤∤_ + +∤∤-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 z∤∤x z∣∣y = contradiction (∣∣-respʳ-≈ (sym x≈y) z∣∣y) z∤∤x + +∤∤-resp : _∤∤_ Respects₂ _≈_ +∤∤-resp = ∤∤-respʳ , ∤∤-respˡ + From 8f1a1d66d858792a7a3952acd45f5bab4e403c79 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Sat, 31 Aug 2024 11:21:30 +0100 Subject: [PATCH 2/4] blank line --- src/Algebra/Properties/Magma/Divisibility.agda | 1 - 1 file changed, 1 deletion(-) diff --git a/src/Algebra/Properties/Magma/Divisibility.agda b/src/Algebra/Properties/Magma/Divisibility.agda index 7c9cbdccd3..2b366b36d3 100644 --- a/src/Algebra/Properties/Magma/Divisibility.agda +++ b/src/Algebra/Properties/Magma/Divisibility.agda @@ -82,4 +82,3 @@ xy≈z⇒y∣z x y xy≈z = ∣-respʳ xy≈z (x∣yx y x) ∤∤-resp : _∤∤_ Respects₂ _≈_ ∤∤-resp = ∤∤-respʳ , ∤∤-respˡ - From b49b2b0d27761530518e3320a2f9ea5661423528 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Mon, 2 Sep 2024 05:36:57 +0100 Subject: [PATCH 3/4] renaming/deprecation following #2341 --- CHANGELOG.md | 14 ++-- .../Properties/Magma/Divisibility.agda | 71 +++++++++++++------ 2 files changed, 55 insertions(+), 30 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index df474147a9..669e53e509 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -50,13 +50,13 @@ Additions to existing modules * Properties of non-divisibility in `Algebra.Properties.Magma.Divisibility`: ```agda - ∤-respˡ : _∤_ Respectsˡ _≈_ - ∤-respʳ : _∤_ Respectsʳ _≈_ - ∤-resp : _∤_ Respects₂ _≈_ - ∤∤-sym : Symmetric _∤∤_ - ∤∤-respˡ : _∤∤_ Respectsˡ _≈_ - ∤∤-respʳ : _∤∤_ Respectsʳ _≈_ - ∤∤-resp : _∤∤_ Respects₂ _≈_ + ∤-respˡ-≈ : _∤_ Respectsˡ _≈_ + ∤-respʳ-≈ : _∤_ Respectsʳ _≈_ + ∤-resp-≈ : _∤_ Respects₂ _≈_ + ∤∤-sym : Symmetric _∤∤_ + ∤∤-respˡ-≈ : _∤∤_ Respectsˡ _≈_ + ∤∤-respʳ-≈ : _∤∤_ Respectsʳ _≈_ + ∤∤-resp-≈ : _∤∤_ Respects₂ _≈_ ``` * In `Data.List.Properties`: diff --git a/src/Algebra/Properties/Magma/Divisibility.agda b/src/Algebra/Properties/Magma/Divisibility.agda index 2b366b36d3..aa9f4e53c5 100644 --- a/src/Algebra/Properties/Magma/Divisibility.agda +++ b/src/Algebra/Properties/Magma/Divisibility.agda @@ -26,32 +26,32 @@ open import Algebra.Definitions.RawMagma rawMagma public ------------------------------------------------------------------------ -- Properties of divisibility -∣-respʳ : _∣_ Respectsʳ _≈_ -∣-respʳ y≈z (q , qx≈y) = q , trans qx≈y y≈z +∣-respʳ-≈ : _∣_ Respectsʳ _≈_ +∣-respʳ-≈ y≈z (q , qx≈y) = q , trans qx≈y y≈z -∣-respˡ : _∣_ Respectsˡ _≈_ -∣-respˡ x≈z (q , qx≈y) = q , trans (∙-congˡ (sym x≈z)) qx≈y +∣-respˡ-≈ : _∣_ Respectsˡ _≈_ +∣-respˡ-≈ x≈z (q , qx≈y) = q , trans (∙-congˡ (sym x≈z)) qx≈y -∣-resp : _∣_ Respects₂ _≈_ -∣-resp = ∣-respʳ , ∣-respˡ +∣-resp-≈ : _∣_ Respects₂ _≈_ +∣-resp-≈ = ∣-respʳ-≈ , ∣-respˡ-≈ x∣yx : ∀ x y → x ∣ y ∙ x x∣yx x y = y , refl xy≈z⇒y∣z : ∀ x y {z} → x ∙ y ≈ z → y ∣ z -xy≈z⇒y∣z x y xy≈z = ∣-respʳ xy≈z (x∣yx y x) +xy≈z⇒y∣z x y xy≈z = ∣-respʳ-≈ xy≈z (x∣yx y x) ------------------------------------------------------------------------ -- Properties of non-divisibility -∤-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ˡ-≈ ------------------------------------------------------------------------ -- Properties of mutual divisibility _∣∣_ @@ -59,11 +59,11 @@ xy≈z⇒y∣z x y xy≈z = ∣-respʳ xy≈z (x∣yx y x) ∣∣-sym : Symmetric _∣∣_ ∣∣-sym = swap -∣∣-respʳ-≈ : _∣∣_ Respectsʳ _≈_ -∣∣-respʳ-≈ y≈z (x∣y , y∣x) = ∣-respʳ y≈z x∣y , ∣-respˡ y≈z y∣x - ∣∣-respˡ-≈ : _∣∣_ Respectsˡ _≈_ -∣∣-respˡ-≈ x≈z (x∣y , y∣x) = ∣-respˡ x≈z x∣y , ∣-respʳ x≈z y∣x +∣∣-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-≈ = ∣∣-respʳ-≈ , ∣∣-respˡ-≈ @@ -74,11 +74,36 @@ xy≈z⇒y∣z x y xy≈z = ∣-respʳ xy≈z (x∣yx y x) ∤∤-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ˡ-≈ + + +------------------------------------------------------------------------ +-- DEPRECATED NAMES +------------------------------------------------------------------------ +-- Please use the new names as continuing support for the old names is +-- not guaranteed. + +-- Version 2.2 + +∣-respˡ = ∣-respˡ-≈ +{-# WARNING_ON_USAGE ∣-respˡ +"Warning: ∣-respˡ was deprecated in v2.2. +Please use ∣-respˡ-≈ instead. " +#-} +∣-respʳ = ∣-respʳ-≈ +{-# WARNING_ON_USAGE ∣-respʳ +"Warning: ∣-respʳ was deprecated in v2.2. +Please use ∣-respʳ-≈ instead. " +#-} +∣-resp = ∣-resp-≈ +{-# WARNING_ON_USAGE ∣-resp +"Warning: ∣-resp was deprecated in v2.2. +Please use ∣-resp-≈ instead. " +#-} From cf5885a07c1c341b54830ddbe8723bc06c2d695e Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Tue, 3 Sep 2024 04:37:14 +0100 Subject: [PATCH 4/4] add deprecations to `CHANGELOG` --- CHANGELOG.md | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/CHANGELOG.md b/CHANGELOG.md index 669e53e509..a12f842abf 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -24,6 +24,13 @@ Deprecated modules Deprecated names ---------------- +* In `Algebra.Properties.Magma.Divisibility`: + ```agda + ∣-respˡ ↦ ∣-respˡ-≈ + ∣-respʳ ↦ ∣-respʳ-≈ + ∣-resp ↦ ∣-resp-≈ + ``` + * In `Data.Vec.Properties`: ```agda ++-assoc _ ↦ ++-assoc-eqFree