Qualified imports in Data.Integer.Divisibility fixing #2280 (#2294)

* fixing #2280

* re-export constructor via pattern synonym

* updated `README`

* refactor: better disambiguation; added a note in `CHANGELOG`

Author: jamesmckinna

CHANGELOG.md

@@ -127,6 +127,11 @@ Additions to existing modules
   nonZeroIndex : Fin n → ℕ.NonZero n
   ```
 
+* In `Data.Integer.Divisisbility`: introduce `divides` as an explicit pattern synonym
+  ```agda
+  pattern divides k eq = Data.Nat.Divisibility.divides k eq
+  ```
+
 * In `Data.List.Relation.Unary.All.Properties`:
   ```agda
   All-catMaybes⁺ : All (Maybe.All P) xs → All P (catMaybes xs)

doc/README/Data/Integer.agda

@@ -33,29 +33,29 @@ ex₃ = + 1  +  + 3 * - + 2  -  + 4
 -- Propositional equality and some related properties can be found
 -- in Relation.Binary.PropositionalEquality.
 
-open import Relation.Binary.PropositionalEquality as P using (_≡_)
+open import Relation.Binary.PropositionalEquality as ≡ using (_≡_)
 
 ex₄ : ex₃ ≡ - + 9
-ex₄ = P.refl
+ex₄ = ≡.refl
 
 -- Data.Integer.Properties contains a number of properties related to
 -- integers. Algebra defines what a commutative ring is, among other
 -- things.
 
-import Data.Integer.Properties as ℤₚ
+import Data.Integer.Properties as ℤ
 
 ex₅ : ∀ i j → i * j ≡ j * i
-ex₅ i j = ℤₚ.*-comm i j
+ex₅ i j = ℤ.*-comm i j
 
 -- The module ≡-Reasoning in Relation.Binary.PropositionalEquality
 -- provides some combinators for equational reasoning.
 
-open P.≡-Reasoning
+open ≡.≡-Reasoning
 
 ex₆ : ∀ i j → i * (j + + 0) ≡ j * i
 ex₆ i j = begin
-  i * (j + + 0)  ≡⟨ P.cong (i *_) (ℤₚ.+-identityʳ j) ⟩
-  i * j          ≡⟨ ℤₚ.*-comm i j ⟩
+  i * (j + + 0)  ≡⟨ ≡.cong (i *_) (ℤ.+-identityʳ j) ⟩
+  i * j          ≡⟨ ℤ.*-comm i j ⟩
   j * i          ∎
 
 -- The module RingSolver in Data.Integer.Solver contains a solver
@@ -67,4 +67,4 @@ open +-*-Solver
 
 ex₇ : ∀ i j → i * - j - j * i ≡ - + 2 * i * j
 ex₇ = solve 2 (λ i j → i :* :- j :- j :* i  :=  :- con (+ 2) :* i :* j)
-              P.refl
+              ≡.refl

src/Data/Integer/Divisibility.agda

@@ -14,42 +14,42 @@ open import Function.Base using (_on_; _$_)
 open import Data.Integer.Base
 open import Data.Integer.Properties
 import Data.Nat.Base as ℕ
-import Data.Nat.Divisibility as ℕᵈ
+import Data.Nat.Divisibility as ℕ
 open import Level
 open import Relation.Binary.Core using (Rel; _Preserves_⟶_)
-open import Relation.Binary.PropositionalEquality
+
 
 ------------------------------------------------------------------------
 -- Divisibility
 
 infix 4 _∣_
 
 _∣_ : Rel ℤ 0ℓ
-_∣_ = ℕᵈ._∣_ on ∣_∣
+_∣_ = ℕ._∣_ on ∣_∣
 
-open ℕᵈ public using (divides)
+pattern divides k eq  = ℕ.divides k eq
 
 ------------------------------------------------------------------------
 -- Properties of divisibility
 
 *-monoʳ-∣ : ∀ k → (k *_) Preserves _∣_ ⟶ _∣_
 *-monoʳ-∣ k {i} {j} i∣j = begin
   ∣ k * i ∣       ≡⟨ abs-* k i ⟩
-  ∣ k ∣ ℕ.* ∣ i ∣ ∣⟨ ℕᵈ.*-monoʳ-∣ ∣ k ∣ i∣j ⟩
-  ∣ k ∣ ℕ.* ∣ j ∣ ≡⟨ sym (abs-* k j) ⟩
+  ∣ k ∣ ℕ.* ∣ i ∣ ∣⟨ ℕ.*-monoʳ-∣ ∣ k ∣ i∣j ⟩
+  ∣ k ∣ ℕ.* ∣ j ∣ ≡⟨ abs-* k j ⟨
   ∣ k * j ∣       ∎
-  where open ℕᵈ.∣-Reasoning
+  where open ℕ.∣-Reasoning
 
 *-monoˡ-∣ : ∀ k → (_* k) Preserves _∣_ ⟶ _∣_
 *-monoˡ-∣ k {i} {j} rewrite *-comm i k | *-comm j k = *-monoʳ-∣ k
 
 *-cancelˡ-∣ : ∀ k {i j} .{{_ : NonZero k}} → k * i ∣ k * j → i ∣ j
-*-cancelˡ-∣ k {i} {j} k*i∣k*j = ℕᵈ.*-cancelˡ-∣ ∣ k ∣ $ begin
-  ∣ k ∣ ℕ.* ∣ i ∣  ≡⟨ sym (abs-* k i) ⟩
+*-cancelˡ-∣ k {i} {j} k*i∣k*j = ℕ.*-cancelˡ-∣ ∣ k ∣ $ begin
+  ∣ k ∣ ℕ.* ∣ i ∣  ≡⟨ abs-* k i ⟨
   ∣ k * i ∣        ∣⟨ k*i∣k*j ⟩
   ∣ k * j ∣        ≡⟨ abs-* k j ⟩
   ∣ k ∣ ℕ.* ∣ j ∣  ∎
-  where open ℕᵈ.∣-Reasoning
+  where open ℕ.∣-Reasoning
 
 *-cancelʳ-∣ : ∀ k {i j} .{{_ : NonZero k}} → i * k ∣ j * k → i ∣ j
 *-cancelʳ-∣ k {i} {j} rewrite *-comm i k | *-comm j k = *-cancelˡ-∣ k

src/Data/Integer/Divisibility/Signed.agda

@@ -11,9 +11,7 @@ module Data.Integer.Divisibility.Signed where
 open import Function.Base using (_⟨_⟩_; _$_; _$′_; _∘_; _∘′_)
 open import Data.Integer.Base
 open import Data.Integer.Properties
-open import Data.Integer.Divisibility as Unsigned
-  using (divides)
-  renaming (_∣_ to _∣ᵤ_)
+import Data.Integer.Divisibility as Unsigned
 import Data.Nat.Base as ℕ
 import Data.Nat.Divisibility as ℕ
 import Data.Nat.Coprimality as ℕ
@@ -45,9 +43,9 @@ open _∣_ using (quotient) public
 ------------------------------------------------------------------------
 -- Conversion between signed and unsigned divisibility
 
-∣ᵤ⇒∣ : ∀ {k i} → k ∣ᵤ i → k ∣ i
-∣ᵤ⇒∣ {k} {i} (divides 0           eq) = divides (+ 0) (∣i∣≡0⇒i≡0 eq)
-∣ᵤ⇒∣ {k} {i} (divides q@(ℕ.suc _) eq) with k ≟ +0
+∣ᵤ⇒∣ : ∀ {k i} → k Unsigned.∣ i → k ∣ i
+∣ᵤ⇒∣ {k} {i} (Unsigned.divides 0           eq) = divides (+ 0) (∣i∣≡0⇒i≡0 eq)
+∣ᵤ⇒∣ {k} {i} (Unsigned.divides q@(ℕ.suc _) eq) with k ≟ +0
 ... | yes refl = divides +0 (∣i∣≡0⇒i≡0 (trans eq (ℕ.*-zeroʳ q)))
 ... | no  neq  = divides (sign i Sign.* sign k ◃ q) (◃-cong sign-eq abs-eq)
   where
@@ -85,8 +83,8 @@ open _∣_ using (quotient) public
     ∣ i ∣              ∎
     where open ≡-Reasoning
 
-∣⇒∣ᵤ : ∀ {k i} → k ∣ i → k ∣ᵤ i
-∣⇒∣ᵤ {k} {i} (divides q eq) = divides ∣ q ∣ $′ begin
+∣⇒∣ᵤ : ∀ {k i} → k ∣ i → k Unsigned.∣ i
+∣⇒∣ᵤ {k} {i} (divides q eq) = Unsigned.divides ∣ q ∣ $′ begin
   ∣ i ∣           ≡⟨ cong ∣_∣ eq ⟩
   ∣ q * k ∣       ≡⟨ abs-* q k ⟩
   ∣ q ∣ ℕ.* ∣ k ∣ ∎

src/Data/Integer/GCD.agda

@@ -11,10 +11,9 @@ module Data.Integer.GCD where
 open import Data.Integer.Base
 open import Data.Integer.Divisibility
 open import Data.Integer.Properties
-open import Data.Nat.Base
 import Data.Nat.GCD as ℕ
 open import Data.Product.Base using (_,_)
-open import Relation.Binary.PropositionalEquality
+open import Relation.Binary.PropositionalEquality.Core using (_≡_; cong)
 
 open import Algebra.Definitions {A = ℤ} _≡_ as Algebra
   using (Associative; Commutative; LeftIdentity; RightIdentity; LeftZero; RightZero; Zero)

src/Data/Integer/LCM.agda

@@ -11,9 +11,8 @@ module Data.Integer.LCM where
 open import Data.Integer.Base
 open import Data.Integer.Divisibility
 open import Data.Integer.GCD
-open import Data.Nat.Base using (ℕ)
 import Data.Nat.LCM as ℕ
-open import Relation.Binary.PropositionalEquality
+open import Relation.Binary.PropositionalEquality.Core using (_≡_; cong)
 
 ------------------------------------------------------------------------
 -- Definition