Refactor lcm (#818)

Author: MatthewDaggitt

CHANGELOG.md

@@ -72,11 +72,11 @@ Bug-fixes
 Non-backwards compatible changes
 --------------------------------
 
-* The function `gcd` in `Data.Nat.GCD` has been reimplemented so it is much
-  faster when compiled. The function `gcd` now has type `ℕ → ℕ → ℕ`. The old
-  function of type `(m n : ℕ) → ∃ λ d → GCD m n d` has been renamed `mkGCD`,
-  and `gcd′` in `Data.Nat.Coprimality` has been renamed `mkGCD′`. All other
-  functionality is untouched.
+* The functions `gcd` and `lcm` in `Data.Nat.GCD/LCM` have been reimplemented
+  so that they run much faster when compiled. The functions now have type `ℕ → ℕ → ℕ`.
+  The old functions of type `(m n : ℕ) → ∃ λ d → GCD/LCM m n d` has been renamed
+  `mkGCD`/`mkLCM`, and `gcd′` in `Data.Nat.Coprimality` has been deprecated. All
+  other functionality is untouched.
 
 * The module `IsDistributiveLattice` in `Algebra.Structures` has had its field
   renamed from `∨-∧-distribʳ` to `∨-distribʳ-∧` in order to match the conventions
@@ -285,6 +285,17 @@ been attached to all deprecated names.
   /-cong  ↦  *-cancelˡ-∣
   ```
 
+* In `Data.Nat.DivMod`:
+  ```agda
+  a≡a%n+[a/n]*n  ↦  m≡m%n+[m/n]*n
+  a%1≡0          ↦  n%1≡0
+  a%n%n≡a%n      ↦  m%n%n≡m%n
+  [a+n]%n≡a%n    ↦  [m+n]%n≡m%n
+  [a+kn]%n≡a%n   ↦  [m+kn]%n≡m%n
+  kn%n≡0         ↦  m*n%n≡0
+  a%n<n          ↦  m%n<n
+  ```
+
 * In `Data.Nat.Properties`:
   ```agda
   m≢0⇒suc[pred[m]]≡m  ↦  suc[pred[n]]≡n
@@ -617,20 +628,19 @@ Other minor additions
   _>>=_     : Maybe A → (A → Maybe B) → Maybe B
   ```
 
-* Added new proofs to `Data.Nat.GCD`:
-  ```agda
-  gcd-comm     : gcd m n ≡ gcd n m
-  gcd[m,n]∣m   : gcd m n ∣ m
-  gcd[m,n]∣n   : gcd m n ∣ n
-  gcd-greatest : c ∣ m → c ∣ n → c ∣ gcd m n
-  gcd≢0        : m ≢ 0 ⊎ n ≢ 0 → gcd m n ≢ 0
-  ```
-
 * Added new proofs to `Data.Nat.Divisibility`:
   ```agda
-  ∣m∸n∣n⇒∣m : n ≤ m → i ∣ m ∸ n → i ∣ n → i ∣ m
-  ∣n∣m%n⇒∣m : d ∣ n → d ∣ (m % n) → d ∣ m
-  %-presˡ-∣ : d ∣ m → d ∣ n → d ∣ (m % n)
+  ∣m∸n∣n⇒∣m   : n ≤ m → i ∣ m ∸ n → i ∣ n → i ∣ m
+  ∣n∣m%n⇒∣m   : d ∣ n → d ∣ (m % n) → d ∣ m
+  *-monoˡ-∣   : i ∣ j → i * k ∣ j * k
+  %-presˡ-∣   : d ∣ m → d ∣ n → d ∣ (m % n)
+  m/n∣m       : n ∣ m → m / n ∣ m
+  m*n∣o⇒m∣o/n : m * n ∣ o → m ∣ o / n
+  m*n∣o⇒n∣o/m : m * n ∣ o → n ∣ o / m
+  m∣n/o⇒m*o∣n : o ∣ n → m ∣ n / o → m * o ∣ n
+  m∣n/o⇒o*m∣n : o ∣ n → m ∣ n / o → o * m ∣ n
+  m/n∣o⇒m∣o*n : n ∣ m → m / n ∣ o → m ∣ o * n
+  m∣n*o⇒m/n∣o : n ∣ m → m ∣ o * n → m / n ∣ o
   ```
 
 * Added new operator and proofs to `Data.Nat.DivMod`:
@@ -643,13 +653,14 @@ Other minor additions
   %-remove-+ʳ         : d ∣ n → (m + n) % d ≡ m % d
   %-pred-≡0           : suc m % n ≡ 0 → m % n ≡ n ∸ 1
   m<[1+n%d]⇒m≤[n%d]   : m < suc n % d → m ≤ n % d
-  [1+a%n]≤1+m⇒[a%n]≤m : 0 < suc n % d → suc n % d ≤ suc m → n % d ≤ m
+  [1+m%d]≤1+n⇒[m%d]≤n : 0 < suc m % d → suc m % d ≤ suc n → m % d ≤ n
 
   0/n≡0           : 0 / n ≡ 0
-  n/1≡a           : n / 1 ≡ n
+  n/1≡n           : n / 1 ≡ n
   n/n≡1           : n / n ≡ 1
   m*n/n≡m         : m * n / n ≡ m
   m/n*n≡m         : n ∣ m → m / n * n ≡ m
+  m*[n/m]≡n       : m ∣ n → m * (n / m) ≡ n
   m/n*n≤m         : m / n * n ≤ m
   m/n<m           : m ≥ 1 → n ≥ 2 → m / n < m
   *-/-assoc       : d ∣ n → (m * n) / d ≡ m * (n / d)
@@ -661,6 +672,30 @@ Other minor additions
   division and modulus functions has been marked irrelevant. This means
   that the operations `_%_`, `_/_` etc. can now be used with `cong`.
 
+* Added new proofs to `Data.Nat.GCD`:
+  ```agda
+  gcd[m,n]∣m            : gcd m n ∣ m
+  gcd[m,n]∣n            : gcd m n ∣ n
+  gcd-greatest          : c ∣ m → c ∣ n → c ∣ gcd m n
+  gcd[0,0]≡0            : gcd 0 0 ≡ 0
+  gcd[m,n]≢0            : m ≢ 0 ⊎ n ≢ 0 → gcd m n ≢ 0
+  gcd-comm              : gcd m n ≡ gcd n m
+  gcd-universality      : (∀ {d} → d ∣ m × d ∣ n → d ∣ g) → (∀ {d} → d ∣ g → d ∣ m × d ∣ n) → g ≡ gcd m n
+  gcd[cm,cn]/c≡gcd[m,n] : gcd (c * m) (c * n) / c ≡ gcd m n
+  c*gcd[m,n]≡gcd[cm,cn] : c * gcd m n ≡ gcd (c * m) (c * n)
+  ```
+
+* Added new proofs to `Data.Nat.LCM`:
+  ```agda
+  m∣lcm[m,n] : m ∣ lcm m n
+  n∣lcm[m,n] : n ∣ lcm m n
+  lcm-least  : m ∣ c → n ∣ c → lcm m n ∣ c
+  lcm[0,n]≡0 : lcm 0 n ≡ 0
+  lcm[n,0]≡0 : lcm n 0 ≡ 0
+  lcm-comm   : lcm m n ≡ lcm n m
+  gcd*lcm    : gcd m n * lcm m n ≡ m * n
+  ```
+
 * Added new proofs to `Data.Nat.Properties`:
   ```agda
   ≤-<-connex : Connex _≤_ _<_

src/Data/Integer/DivMod.agda

@@ -41,7 +41,7 @@ _mod_ : (dividend divisor : ℤ) {≠0 : False (∣ divisor ∣ ℕ.≟ 0)} →
 (n mod d) {d≢0} = (n modℕ ∣ d ∣) {d≢0}
 
 n%ℕd<d : ∀ n d {d≢0} → (n modℕ d) {d≢0} ℕ.< d
-n%ℕd<d (+ n)    sd@(ℕ.suc d) = NDM.a%n<n n d
+n%ℕd<d (+ n)    sd@(ℕ.suc d) = NDM.m%n<n n d
 n%ℕd<d -[1+ n ] sd@(ℕ.suc d) with ℕ.suc n NDM.divMod sd
 ... | NDM.result q Fin.zero    eq = ℕ.s≤s ℕ.z≤n
 ... | NDM.result q (Fin.suc r) eq = ℕ.s≤s (NProp.n∸m≤n (Fin.toℕ r) d)
@@ -52,7 +52,7 @@ n%d<d n -[1+ d ]    = n%ℕd<d n (ℕ.suc d)
 
 a≡a%ℕn+[a/ℕn]*n : ∀ n d {d≢0} → n ≡ + (n modℕ d) {d≢0} + (n divℕ d) {d≢0} * + d
 a≡a%ℕn+[a/ℕn]*n (+ n) sd@(ℕ.suc d) = let q = n NDM./ sd; r = n NDM.% sd in begin
-  + n                ≡⟨ cong +_ (NDM.a≡a%n+[a/n]*n n d) ⟩
+  + n                ≡⟨ cong +_ (NDM.m≡m%n+[m/n]*n n d) ⟩
   + (r ℕ.+ q ℕ.* sd) ≡⟨ pos-+-commute r (q ℕ.* sd) ⟩
   + r + + (q ℕ.* sd) ≡⟨ cong (_+_ (+ (+ n modℕ sd))) (sym (pos-distrib-* q sd)) ⟩
   + r + + q * + sd   ∎ where open ≡-Reasoning

src/Data/Nat/Coprimality.agda

@@ -6,6 +6,9 @@
 
 {-# OPTIONS --without-K --safe #-}
 
+-- Disabled to prevent warnings from deprecated names
+{-# OPTIONS --warn=noUserWarning #-}
+
 module Data.Nat.Coprimality where
 
 open import Data.Empty
@@ -148,28 +151,38 @@ prime⇒coprime (suc (suc m)) p (suc n) _ 1+n<2+m {suc (suc i)}
     (P.sym (cong (2 +_) (toℕ-fromℕ≤ i<m)))
     2+i∣2+m
 
+
+------------------------------------------------------------------------
+-- DEPRECATED NAMES
 ------------------------------------------------------------------------
--- A variant of GCD.
+-- Please use GCD from `Data.Nat.GCD` as continued support for the
+-- proofs below is not guaranteed.
+
+-- Version 1.1.
 
 data GCD′ : ℕ → ℕ → ℕ → Set where
   gcd-* : ∀ {d} q₁ q₂ (c : Coprime q₁ q₂) →
           GCD′ (q₁ * d) (q₂ * d) d
-
--- The two definitions are equivalent.
-
+{-# WARNING_ON_USAGE GCD′
+"Warning: GCD′ was deprecated in v1.1."
+#-}
 gcd-gcd′ : ∀ {d m n} → GCD m n d → GCD′ m n d
 gcd-gcd′         g with GCD.commonDivisor g
 gcd-gcd′ {zero}  g | (divides q₁ refl , divides q₂ refl)
   with q₁ * 0 | *-comm 0 q₁ | q₂ * 0 | *-comm 0 q₂
 ... | .0 | refl | .0 | refl = gcd-* 1 1 (1-coprimeTo 1)
 gcd-gcd′ {suc d} g | (divides q₁ refl , divides q₂ refl) =
   gcd-* q₁ q₂ (Bézout-coprime (Bézout.identity g))
-
+{-# WARNING_ON_USAGE gcd-gcd′
+"Warning: gcd-gcd′ was deprecated in v1.1."
+#-}
 gcd′-gcd : ∀ {m n d} → GCD′ m n d → GCD m n d
 gcd′-gcd (gcd-* q₁ q₂ c) = GCD.is (n∣m*n q₁ , n∣m*n q₂) (coprime-factors c)
-
--- Calculates (the alternative representation of) the gcd of the
--- arguments.
-
+{-# WARNING_ON_USAGE gcd′-gcd
+"Warning: gcd′-gcd was deprecated in v1.1."
+#-}
 mkGCD′ : ∀ m n → ∃ λ d → GCD′ m n d
 mkGCD′ m n = Prod.map id gcd-gcd′ (mkGCD m n)
+{-# WARNING_ON_USAGE mkGCD′
+"Warning: mkGCD′ was deprecated in v1.1."
+#-}