[fixes #1711] Refactoring Data.Nat.Divisibility and `Data.Nat.DivMo…

…d` (#2182)

* added new definitions to `_∣_`

* `CHANGELOG`

* don't declare `quotient≢0` as an `instance`

* replace use of `subst` with one of `trans`

* what's sauce for the goose...

* switch to a `rewrite`-based solution...

* tightened `import`s

* simplified dependenciess

* simplified dependencies; `CHANGELOG`

* removed `module` abstractions

* delegated proof of `quotient≢0` to `Data.Nat.Properties`

* removed redundant property

* cosmetic review changes; others to follow

* better proof of `quotient>1`

* `where` clause layout

* leaving in the flipped equality; moved everything else

* new lemmas moved from `Core`; knock-on consequences; lots of tidying up

* tidying up; `CHANGELOG`

* cosmetic tweaks

* reverted to simple version

* problems with exporting `quotient`

* added last lemma: defining equation for `_/_`

* improved `CHANGELOG`

* revert: simplified imports

* improved `CHANGELOG`

* endpoint of simplifying the proof of `*-pres-∣`

* simplified the proof of `n/m≡quotient`

* simplified the proof of `∣m+n∣m⇒∣n`

* simplified the proof of `∣m∸n∣n⇒∣m`

* simplified `import`s

* simplified a lot of proofs, esp. wrt `divides-refl` and `NonZero` reasoning

* simplified more proofs, esp. wrt `divides-refl` reasoning

* simplified `import`s

* moved `equalityᵒ` proof out of `Core`

* `CHANGELOG`

* temporary fix: further `NonZero` refactoring advised!

* regularised use of instance brackets

* further instance simplification

* further streamlining

* tidied up `CHANGELOG`

* simplified `NonZero` pattern matching

* regularised use of instance brackets

* simplified proof of `/-*-interchange`

* simplified proof of `/-*-interchange`

* ... permitting the migration of `*-pres-∣` to `Data.Nat.Divisibility`

* tweaked proof of `/-*-interchange`

* narrowed `import`s

* simplified proof; renamed new proofs

* Capitalisation

* streamlined `import`s; streamlined proof of decidability

* spurious duplication after merge

* missing symbol import

* replaced one use of `1 < m` with `{{NonTrivial m}}`

* fixed `CHANGELOG`

* removed use of identifier `k`

* refactoring: more use of `NonTrivial` instances

* knock-on consequences: simplified function

* two new lemmas

* refactoring: use of `connex` in proofs

* new lemmas about `pred`

* new lemmas about monus

* refactoring: use of the new properties, simplifying pattern analysis

* whitespace

* questionable? revision after comments on #2221

* silly argument name typo; remove parens

* tidied up imports of `Relation.Nullary`

* removed spurious `instance`

* localised appeals to `Reasoning`

* further use of `variable`s

* tidied up `record` name in comment

* cosmetic

* reconciled implicit/explicit arguments in various monus lemmas

* fixed knock-on change re monus; reverted change to `m/n<m`

* reverted change to `m/n≢0⇒n≤m`

* reverted breaking changes involving `NonZero` inference

* revised `CHANGELOG`

* restored deleted proof

* fix whitespace

* renaming: `DivMod.nonZeroDivisor`

* localised use of `≤-Reasoning`

* reverted export; removed anonymous module

* revert commit re `yes/no`

* renamed flipped equality

* tweaked comment

* added alias for `equality`

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