[fixes #1711] Refactoring Data.Nat.Divisibility and Data.Nat.DivMod

CHANGELOG.md

@@ -21,15 +21,20 @@ Deprecated modules
 Deprecated names
 ----------------
 
+* In `Data.Nat.Divisibility.Core`:
+  ```agda
+  *-pres-∣  ↦  Data.Nat.Divisibility.*-pres-∣
+  ```
+
 New modules
 -----------
 
 Additions to existing modules
 -----------------------------
 
-* In `Data.Maybe.Relation.Binary.Pointwise`:
+* In `Data.Fin.Properties`:
   ```agda
-  pointwise⊆any : Pointwise R (just x) ⊆ Any (R x)
+  nonZeroIndex : Fin n → ℕ.NonZero n
   ```
 
 * In `Data.List.Relation.Unary.All.Properties`:
@@ -39,7 +44,39 @@ Additions to existing modules
   ```
 
 * In `Data.List.Relation.Unary.AllPairs.Properties`:
-  ```
+  ```agda
   catMaybes⁺ : AllPairs (Pointwise R) xs → AllPairs R (catMaybes xs)
   tabulate⁺-< : (i < j → R (f i) (f j)) → AllPairs R (tabulate f)
   ```
+
+* In `Data.Maybe.Relation.Binary.Pointwise`:
+  ```agda
+  pointwise⊆any : Pointwise R (just x) ⊆ Any (R x)
+  ```
+
+* In `Data.Nat.Divisibility`:
+  ```agda
+  quotient≢0       : m ∣ n → .{{NonZero n}} → NonZero quotient
+
+  m|n⇒n≡quotient*m : m ∣ n → n ≡ quotient * m
+  m|n⇒n≡m*quotient : m ∣ n → n ≡ m * quotient
+  quotient-∣       : m ∣ n → quotient ∣ n
+  quotient>1       : m ∣ n → m < n → 1 < quotient
+  quotient-<       : m ∣ n → .{{NonTrivial m}} → .{{NonZero n}} → quotient < n
+  n/m≡quotient     : m ∣ n → .{{_ : NonZero m}} → n / m ≡ quotient
+
+  m/n≡0⇒m<n    : .{{_ : NonZero n}} → m / n ≡ 0 → m < n
+  m/n≢0⇒n≤m    : .{{_ : NonZero n}} → m / n ≢ 0 → n ≤ m
+
+  nonZeroDivisor : DivMod dividend divisor → NonZero divisor
+  ```
+
+* Added new proofs in `Data.Nat.Properties`:
+  ```agda
+  m≤n+o⇒m∸n≤o : ∀ m n {o} → m ≤ n + o → m ∸ n ≤ o
+  m<n+o⇒m∸n<o : ∀ m n {o} → .{{NonZero o}} → m < n + o → m ∸ n < o
+  pred-cancel-≤ : pred m ≤ pred n → (m ≡ 1 × n ≡ 0) ⊎ m ≤ n
+  pred-cancel-< : pred m < pred n → m < n
+  pred-injective : .{{NonZero m}} → .{{NonZero n}} → pred m ≡ pred n → m ≡ n
+  pred-cancel-≡ : pred m ≡ pred n → ((m ≡ 0 × n ≡ 1) ⊎ (m ≡ 1 × n ≡ 0)) ⊎ m ≡ n
+  ```

src/Data/Digit.agda

@@ -55,11 +55,8 @@ toNatDigits base@(suc (suc _)) n = aux (<-wellFounded-fast n) []
   aux : {n : ℕ} → Acc _<_ n → List ℕ → List ℕ
   aux {zero}        _      xs =  (0 ∷ xs)
   aux {n@(suc _)} (acc wf) xs with does (0 <? n / base)
-  ... | false = (n % base) ∷ xs
-  ... | true  = aux (wf q<n) ((n % base) ∷ xs)
-    where
-    q<n : n / base < n
-    q<n = m/n<m n base (s<s z<s)
+  ... | false = (n % base) ∷ xs -- Could this more simply be n ∷ xs here?
+  ... | true  = aux (wf (m/n<m n base sz<ss)) ((n % base) ∷ xs)
 
 ------------------------------------------------------------------------
 -- Converting between `ℕ` and expansions of `Digit base`

src/Data/Fin/Properties.agda

@@ -65,6 +65,9 @@ private
 ¬Fin0 : ¬ Fin 0
 ¬Fin0 ()
 
+nonZeroIndex : Fin n → ℕ.NonZero n
+nonZeroIndex {n = suc _} _ = _
+
 ------------------------------------------------------------------------
 -- Bundles
 

src/Data/Nat/Coprimality.agda

@@ -21,7 +21,7 @@ open import Function.Base using (_∘_)
 open import Level using (0ℓ)
 open import Relation.Binary.PropositionalEquality.Core as P
   using (_≡_; _≢_; refl; trans; cong; subst)
-open import Relation.Nullary as Nullary using (¬_; contradiction; yes ; no)
+open import Relation.Nullary as Nullary using (¬_; contradiction; map′)
 open import Relation.Binary.Core using (Rel)
 open import Relation.Binary.Definitions using (Symmetric; Decidable)
 
@@ -65,18 +65,8 @@ coprime-/gcd m n = GCD≡1⇒coprime (GCD-/gcd m n)
 sym : Symmetric Coprime
 sym c = c ∘ swap
 
-private
-  0≢1 : 0 ≢ 1
-  0≢1 ()
-
-  2+≢1 : ∀ {n} → 2+ n ≢ 1
-  2+≢1 ()
-
 coprime? : Decidable Coprime
-coprime? m n with mkGCD m n
-... | (0    , g) = no  (0≢1  ∘ GCD.unique g ∘ coprime⇒GCD≡1)
-... | (1    , g) = yes (GCD≡1⇒coprime g)
-... | (2+ _ , g) = no  (2+≢1 ∘ GCD.unique g ∘ coprime⇒GCD≡1)
+coprime? m n = map′ gcd≡1⇒coprime coprime⇒gcd≡1 (gcd m n ≟ 1)
 
 ------------------------------------------------------------------------
 -- Other basic properties