[ fix #1302 ] Redefine _⊖_ to use _≤ᵇ_ and _∸_ (#1303)

Author: gallais

CHANGELOG.md

@@ -21,13 +21,35 @@ Bug-fixes
 * The binary relation `_≉_` exposed by records in `Relation.Binary.Bundles` now has
   the correct infix precedence.
 
+* Added version to library name
+
 Non-backwards compatible changes
 --------------------------------
 
 * The internal build utilities package `lib.cabal` has been renamed
   `agda-stdlib-utils.cabal` to avoid potential conflict or confusion.
   Please note that the package is not intended for external use.
-* The module `Algebra.Construct.Zero` and `Algebra.Module.Construct.Zero` are now level-polymorphic, each taking two implicit level parameters.
+
+* The module `Algebra.Construct.Zero` and `Algebra.Module.Construct.Zero`
+  are now level-polymorphic, each taking two implicit level parameters.
+
+* Previously the definition of `_⊖_` in `Data.Integer.Base` was defined
+  inductively as:
+  ```agda
+  _⊖_ : ℕ → ℕ → ℤ
+  m       ⊖ ℕ.zero  = + m
+  ℕ.zero  ⊖ ℕ.suc n = -[1+ n ]
+  ℕ.suc m ⊖ ℕ.suc n = m ⊖ n
+  ```
+  which meant that the unary arguments had to be evaluated. To make it
+  much faster it's definition has been changed to use operations on `ℕ`
+  that are backed by builtin operations:
+  ```agda
+  _⊖_ : ℕ → ℕ → ℤ
+  m ⊖ n with m ℕ.<ᵇ n
+  ... | true  = - + (n ℕ.∸ m)
+  ... | false = + (m ℕ.∸ n)
+  ```
 
 Deprecated modules
 ------------------
@@ -115,6 +137,13 @@ Other minor additions
   CancellativeCommutativeSemiring c ℓ : Set (suc (c ⊔ ℓ))
   ```
 
+* Added new definitions to `Algebra.Definitions`:
+  ```agda
+  AlmostLeftCancellative  e _•_ = ∀ {x} y z → ¬ x ≈ e → (x • y) ≈ (x • z) → y ≈ z
+  AlmostRightCancellative e _•_ = ∀ {x} y z → ¬ x ≈ e → (y • x) ≈ (z • x) → y ≈ z
+  AlmostCancellative      e _•_ = AlmostLeftCancellative e _•_ × AlmostRightCancellative e _•_
+  ```
+
 * Added new records to `Algebra.Morphism.Structures`:
   ```agda
   IsNearSemiringHomomorphism (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂)
@@ -128,27 +157,38 @@ Other minor additions
   IsLatticeIsomorphism   (⟦_⟧ : A → B) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂)
   ```
 
-* Added new proofs to `Relation.Binary.Construct.Closure.Transitive`:
+* Added new definitions to `Algebra.Structures`:
   ```agda
-  reflexive   : Reflexive _∼_ → Reflexive _∼⁺_
-  symmetric   : Symmetric _∼_ → Symmetric _∼⁺_
-  transitive  : Transitive _∼⁺_
-  wellFounded : WellFounded _∼_ → WellFounded _∼⁺_
+  IsCommutativeMagma (• : Op₂ A) : Set (a ⊔ ℓ)
+  IsCancellativeCommutativeSemiring (+ * : Op₂ A) (0# 1# : A) : Set (a ⊔ ℓ)
+  ```
 
-* Added new definitions to `Algebra.Definitions`:
+* Added new proofs in `Data.Integer.Properties`:
   ```agda
-  AlmostLeftCancellative  e _•_ = ∀ {x} y z → ¬ x ≈ e → (x • y) ≈ (x • z) → y ≈ z
-  AlmostRightCancellative e _•_ = ∀ {x} y z → ¬ x ≈ e → (y • x) ≈ (z • x) → y ≈ z
-  AlmostCancellative      e _•_ = AlmostLeftCancellative e _•_ × AlmostRightCancellative e _•_
+  [1+m]⊖[1+n]≡m⊖n : suc m ⊖ suc n ≡ m ⊖ n
+  ⊖-≤             : m ≤ n → m ⊖ n ≡ - + (n ∸ m)
+  -m+n≡n⊖m        : - (+ m) + + n ≡ n ⊖ m
+  m-n≡m⊖n         : + m + (- + n) ≡ m ⊖ n
   ```
 
-* Added new record to `Algebra.Structures`:
+* Added new definition in `Data.Nat.Base`:
   ```agda
-  IsCommutativeMagma (• : Op₂ A) : Set (a ⊔ ℓ)
-  IsCancellativeCommutativeSemiring (+ * : Op₂ A) (0# 1# : A) : Set (a ⊔ ℓ)
+  _≤ᵇ_ : (m n : ℕ) → Bool
   ```
 
-* Add version to library name
+* Added new proofs in `Data.Nat.Properties`:
+  ```agda
+  ≤ᵇ⇒≤ : T (m ≤ᵇ n) → m ≤ n
+  ≤⇒≤ᵇ : m ≤ n → T (m ≤ᵇ n)
+
+  <ᵇ-reflects-< : Reflects (m < n) (m <ᵇ n)
+  ≤ᵇ-reflects-≤ : Reflects (m ≤ n) (m ≤ᵇ n)
+  ```
+
+* Added new proof in `Relation.Nullary.Reflects`:
+  ```agda
+  fromEquivalence : (T b → P) → (P → T b) → Reflects P b
+  ```
 
 * Add new properties to `Data.Vec.Properties`:
   ```agda
@@ -160,6 +200,14 @@ Other minor additions
   zipWith-replicate : zipWith {n = n} _⊕_ (replicate x) (replicate y) ≡ replicate (x ⊕ y)
   ```
 
+* Added new proofs to `Relation.Binary.Construct.Closure.Transitive`:
+  ```agda
+  reflexive   : Reflexive _∼_ → Reflexive _∼⁺_
+  symmetric   : Symmetric _∼_ → Symmetric _∼⁺_
+  transitive  : Transitive _∼⁺_
+  wellFounded : WellFounded _∼_ → WellFounded _∼⁺_
+  ```
+
 * Add new properties to `Data.Integer.Properties`:
   ```agda
   +-*-commutativeSemiring : CommutativeSemiring 0ℓ 0ℓ

src/Data/Integer/Base.agda

@@ -14,8 +14,9 @@
 
 module Data.Integer.Base where
 
+open import Data.Bool.Base using (true; false)
 open import Data.Empty using (⊥)
-open import Data.Unit using (⊤)
+open import Data.Unit.Base using (⊤)
 open import Data.Nat.Base as ℕ
   using (ℕ; z≤n; s≤s) renaming (_+_ to _ℕ+_; _*_ to _ℕ*_)
 open import Data.Sign as Sign using (Sign) renaming (_*_ to _S*_)
@@ -188,11 +189,12 @@ signAbs +[1+ n ] = Sign.+ ◂ ℕ.suc n
 - +[1+ n ] = -[1+ n ]
 
 -- Subtraction of natural numbers.
-
+-- We define it using _<ᵇ_ and _∸_ rather than inductively so that it
+-- is backed by builtin operations. This makes it much faster.
 _⊖_ : ℕ → ℕ → ℤ
-m       ⊖ ℕ.zero  = + m
-ℕ.zero  ⊖ ℕ.suc n = -[1+ n ]
-ℕ.suc m ⊖ ℕ.suc n = m ⊖ n
+m ⊖ n with m ℕ.<ᵇ n
+... | true  = - + (n ℕ.∸ m)
+... | false = + (m ℕ.∸ n)
 
 -- Addition.
 

src/Data/Integer/DivMod.agda

@@ -8,6 +8,7 @@
 
 module Data.Integer.DivMod where
 
+open import Data.Bool.Base using (true; false)
 open import Data.Fin.Base as Fin using (Fin)
 import Data.Fin.Properties as FProp
 open import Data.Integer.Base as ℤ
@@ -97,9 +98,11 @@ a≡a%ℕn+[a/ℕn]*n -[1+ n ] sd@(ℕ.suc d) with (ℕ.suc n) NDM.divMod (ℕ.s
 
     open ≡-Reasoning
 
-    fin-inv : ∀ d (k : Fin d) → + (ℕ.suc d) - + ℕ.suc (Fin.toℕ k) ≡ + (d ℕ.∸ Fin.toℕ k)
-    fin-inv (ℕ.suc n) Fin.zero    = refl
-    fin-inv (ℕ.suc n) (Fin.suc k) = ⊖-≥ {n} {Fin.toℕ k} (NProp.<⇒≤ (FProp.toℕ<n k))
+    fin-inv : ∀ d (k : Fin d) → +[1+ d ] - +[1+ Fin.toℕ k ] ≡ + (d ℕ.∸ Fin.toℕ k)
+    fin-inv d k = begin
+      +[1+ d ] - +[1+ Fin.toℕ k ] ≡⟨ m-n≡m⊖n (ℕ.suc d) (ℕ.suc (Fin.toℕ k)) ⟩
+      ℕ.suc d ⊖ ℕ.suc (Fin.toℕ k) ≡⟨ ⊖-≥ (ℕ.s≤s (FProp.toℕ≤n k)) ⟩
+      + (d ℕ.∸ Fin.toℕ k)         ∎ where open ≡-Reasoning
 
 [n/ℕd]*d≤n : ∀ n d {d≢0} → (n divℕ d) {d≢0} ℤ.* ℤ.+ d ℤ.≤ n
 [n/ℕd]*d≤n n (ℕ.suc d) = let q = n divℕ ℕ.suc d; r = n modℕ ℕ.suc d in begin