[ fix #1476 ] improve performance of rational numbers (#1478)

Author: MatthewDaggitt

CHANGELOG.md

@@ -14,12 +14,20 @@ Highlights
 
 * Pseudo random generators for ℕ (available from `Data.Nat.Pseudorandom.LCG`)
 
+* Large increase in the number of proofs about both normalised and unnormalised rational numbers.
+
+* Drastically increased performance of normalised rational numbers.
+
 Bug-fixes
 ---------
 
 * The sum operator `_⊎_` in `Data.Container.Indexed.Combinator` was not as universe 
   polymorphic as it should have been. This has been fixed. The old, less universe
   polymorphic variant is still available under the new name `_⊎′_`.
+
+* The performance of the `gcd` operator over naturals and hence all operations in 
+  `Data.Rational.Base` has been drastically increased by using the new `<-wellFounded-fast`
+  operation in `Data.Nat.Induction`.
 
 * The proof `isEquivalence` in `Function.Properties.(Equivalence/Inverse)` used to be 
   defined in an anonymous module that took two unneccessary `Setoid` arguments:

src/Data/Digit.agda

@@ -51,7 +51,7 @@ Bit     = Digit 2
 
 toNatDigits : (base : ℕ) {base≤16 : True (1 ≤? base)} → ℕ → List ℕ
 toNatDigits base@(suc zero)    n = replicate n 1
-toNatDigits base@(suc (suc b)) n = aux (<-wellFounded n) []
+toNatDigits base@(suc (suc b)) n = aux (<-wellFounded-fast n) []
   where
   aux : {n : ℕ} → Acc _<_ n → List ℕ → List ℕ
   aux {zero}        _        xs =  (0 ∷ xs)

src/Data/Nat/GCD.agda

@@ -14,7 +14,7 @@ open import Data.Nat.DivMod
 open import Data.Nat.GCD.Lemmas
 open import Data.Nat.Properties
 open import Data.Nat.Induction
-  using (Acc; acc; <′-Rec; <′-recBuilder; <-wellFounded)
+  using (Acc; acc; <′-Rec; <′-recBuilder; <-wellFounded-fast)
 open import Data.Product
 open import Data.Sum.Base as Sum using (_⊎_; inj₁; inj₂)
 open import Function
@@ -43,9 +43,9 @@ gcd′ m n@(suc n-1) (acc rec) n<m = gcd′ n (m % n) (rec _ n<m) (m%n<n m n-1)
 
 gcd : ℕ → ℕ → ℕ
 gcd m n with <-cmp m n
-... | tri< m<n _ _ = gcd′ n m (<-wellFounded n) m<n
+... | tri< m<n _ _ = gcd′ n m (<-wellFounded-fast n) m<n
 ... | tri≈ _ _ _   = m
-... | tri> _ _ n<m = gcd′ m n (<-wellFounded m) n<m
+... | tri> _ _ n<m = gcd′ m n (<-wellFounded-fast m) n<m
 
 ------------------------------------------------------------------------
 -- Core properties of gcd′