Add properties of non-divisibility to Algebra.Properties.Magma.Divisibility (#2469)

* fix #2306

* blank line

* renaming/deprecation following #2341

* add deprecations to `CHANGELOG`

Author: jamesmckinna

CHANGELOG.md

@@ -30,6 +30,13 @@ Deprecated names
   ∣-factors-≈  ↦  xy≈z⇒x|z∧y|z
   ```
 
+* In `Algebra.Properties.Magma.Divisibility`:
+  ```agda
+  ∣-respˡ   ↦  ∣-respˡ-≈
+  ∣-respʳ   ↦  ∣-respʳ-≈
+  ∣-resp    ↦  ∣-resp-≈
+ ```
+
 * In `Algebra.Solver.CommutativeMonoid`:
   ```agda
   normalise-correct  ↦  Algebra.Solver.CommutativeMonoid.Normal.correct
@@ -89,6 +96,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 `Algebra.Solver.Ring`
   ```agda
   Env : ℕ → Set _

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
 
 ------------------------------------------------------------------------
@@ -23,32 +26,84 @@ 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 z∤x z∣y = contradiction (∣-respʳ-≈ (sym x≈y) z∣y) z∤x
+
+∤-resp-≈ : _∤_ Respects₂ _≈_
+∤-resp-≈ = ∤-respʳ-≈ , ∤-respˡ-≈
 
 ------------------------------------------------------------------------
 -- Properties of mutual divisibility _∣∣_
 
 ∣∣-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ˡ-≈
+
+------------------------------------------------------------------------
+-- 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ˡ-≈
+
+
+------------------------------------------------------------------------
+-- 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. "
+#-}