Fix #2216 by making divisibility definitions records (#2217)

* Fix #2216 by making divisibility definitions records

* remove spurious/ambiguous `import`

---------

Co-authored-by: jamesmckinna <[email protected]>

Author: 2 people

CHANGELOG.md

@@ -1048,6 +1048,10 @@ Non-backwards compatible changes
 
 * In `Algebra.Core` the operations `Opₗ` and `Opᵣ` have moved to `Algebra.Module.Core`.
 
+* In `Algebra.Definitions.RawMagma.Divisibility` the definitions for `_∣ˡ_` and `_∣ʳ_`
+  have been changed from being defined as raw products to being defined as records. However,
+  the record constructors are called `_,_` so the changes required are minimal.
+
 * In `Codata.Guarded.Stream` the following functions have been modified to have simpler definitions:
   * `cycle`
   * `interleave⁺`

src/Algebra/Definitions/RawMagma.agda

@@ -27,18 +27,31 @@ open RawMagma M renaming (Carrier to A)
 
 infix 5 _∣ˡ_ _∤ˡ_ _∣ʳ_ _∤ʳ_ _∣_ _∤_
 
--- Divisibility from the left
-
-_∣ˡ_ : Rel A (a ⊔ ℓ)
-x ∣ˡ y = ∃ λ q → (x ∙ q) ≈ y
+-- Divisibility from the left.
+--
+-- This and, the definition of right divisibility below, are defined as
+-- records rather than in terms of the base product type in order to
+-- 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.
+
+record _∣ˡ_ (x y : A) : Set (a ⊔ ℓ) where
+  constructor _,_
+  field
+    quotient : A
+    equality : x ∙ quotient ≈ y
 
 _∤ˡ_ : Rel A (a ⊔ ℓ)
 x ∤ˡ y = ¬ x ∣ˡ y
 
 -- Divisibility from the right
 
-_∣ʳ_ : Rel A (a ⊔ ℓ)
-x ∣ʳ y = ∃ λ q → (q ∙ x) ≈ y
+record _∣ʳ_ (x y : A) : Set (a ⊔ ℓ) where
+  constructor _,_
+  field
+    quotient : A
+    equality : quotient ∙ x ≈ y
 
 _∤ʳ_ : Rel A (a ⊔ ℓ)
 x ∤ʳ y = ¬ x ∣ʳ y

src/Algebra/Properties/Magma/Divisibility.agda

@@ -18,7 +18,7 @@ open Magma M
 -- Re-export divisibility relations publicly
 
 open import Algebra.Definitions.RawMagma rawMagma public
-  using (_∣_; _∤_; _∣∣_; _∤∤_; _∣ˡ_; _∤ˡ_; _∣ʳ_; _∤ʳ_)
+  using (_∣_; _∤_; _∣∣_; _∤∤_; _∣ˡ_; _∤ˡ_; _∣ʳ_; _∤ʳ_; _,_)
 
 ------------------------------------------------------------------------
 -- Properties of divisibility

src/Data/Nat/Base.agda

@@ -12,10 +12,9 @@
 module Data.Nat.Base where
 
 open import Algebra.Bundles.Raw using (RawMagma; RawMonoid; RawNearSemiring; RawSemiring)
-open import Algebra.Definitions.RawMagma using (_∣ˡ_)
+open import Algebra.Definitions.RawMagma using (_∣ˡ_; _,_)
 open import Data.Bool.Base using (Bool; true; false; T; not)
 open import Data.Parity.Base using (Parity; 0ℙ; 1ℙ)
-open import Data.Product.Base using (_,_)
 open import Level using (0ℓ)
 open import Relation.Binary.Core using (Rel)
 open import Relation.Binary.PropositionalEquality.Core