Add primop backed versions of natural-number operations (#1818)

Author: Taneb

CHANGELOG.md

@@ -1649,6 +1649,9 @@ Other minor changes
   pattern <′-base          = ≤′-refl
   pattern <′-step {n} m<′n = ≤′-step {n} m<′n
 
+  _⊔′_ : ℕ → ℕ → ℕ
+  _⊓′_ : ℕ → ℕ → ℕ
+  ∣_-_∣′ : ℕ → ℕ → ℕ
   _! : ℕ → ℕ
   ```
 
@@ -1703,6 +1706,12 @@ Other minor changes
   m<n⇒m<n*o : .{{_ : NonZero o}} → m < n → m < n * o
   m<n⇒m<o*n : .{{_ : NonZero o}} → m < n → m < o * n
   ∸-monoˡ-< : m < o → n ≤ m → m ∸ n < o ∸ n
+
+  m≤n⇒∣m-n∣≡n∸m : m ≤ n → ∣ m - n ∣ ≡ n ∸ m
+
+  ⊔≡⊔′ : m ⊔ n ≡ m ⊔′ n
+  ⊓≡⊓′ : m ⊓ n ≡ m ⊓′ n
+  ∣-∣≡∣-∣′ : ∣ m - n ∣ ≡ ∣ m - n ∣′
   ```
 
 * Re-exported additional functions from `Data.Nat`:

src/Data/Nat/Base.agda

@@ -149,13 +149,29 @@ zero  ⊔ n     = n
 suc m ⊔ zero  = suc m
 suc m ⊔ suc n = suc (m ⊔ n)
 
+-- Max defined in terms of primitive operations.
+-- This is much faster than `_⊔_` but harder to reason about. For proofs
+-- involving this function, convert it to `_⊔_` with `Data.Nat.Properties.⊔≡⊔‵`.
+_⊔′_ : ℕ → ℕ → ℕ
+m ⊔′ n with m <ᵇ n
+... | false = m
+... | true  = n
+
 -- Min.
 
 _⊓_ : ℕ → ℕ → ℕ
 zero  ⊓ n     = zero
 suc m ⊓ zero  = zero
 suc m ⊓ suc n = suc (m ⊓ n)
 
+-- Min defined in terms of primitive operations.
+-- This is much faster than `_⊓_` but harder to reason about. For proofs
+-- involving this function, convert it to `_⊓_` wtih `Data.Nat.properties.⊓≡⊓′`.
+_⊓′_ : ℕ → ℕ → ℕ
+m ⊓′ n with m <ᵇ n
+... | false = n
+... | true  = m
+
 -- Division by 2, rounded downwards.
 
 ⌊_/2⌋ : ℕ → ℕ
@@ -181,6 +197,15 @@ x ^ suc n = x * x ^ n
 ∣ x     - zero  ∣ = x
 ∣ suc x - suc y ∣ = ∣ x - y ∣
 
+-- Distance in terms of primitive operations.
+-- This is much faster than `∣_-_∣` but harder to reason about. For proofs
+-- involving this function, convert it to `∣_-_∣` with
+-- `Data.Nat.Properties.∣-∣≡∣-∣′`.
+∣_-_∣′ : ℕ → ℕ → ℕ
+∣ x - y ∣′ with x <ᵇ y
+... | false = x ∸ y
+... | true  = y ∸ x
+
 -- Division
 -- Note properties of these are in `Nat.DivMod` not `Nat.Properties`
 

src/Data/Nat/Properties.agda

@@ -1098,6 +1098,19 @@ m≥n⇒m⊓n≡n {suc m} {suc n} (s≤s m≤n) = cong suc (m≥n⇒m⊓n≡n m
   ; x≥y⇒x⊔y≈x = m≥n⇒m⊔n≡m
   }
 
+------------------------------------------------------------------------
+-- Equality to their counterparts defined in terms of primitive operations
+
+⊔≡⊔′ : ∀ m n → m ⊔ n ≡ m ⊔′ n
+⊔≡⊔′ m n with m <ᵇ n in eq
+... | false = m≥n⇒m⊔n≡m (≮⇒≥ (λ m<n → subst T eq (<⇒<ᵇ m<n)))
+... | true  = m≤n⇒m⊔n≡n (<⇒≤ (<ᵇ⇒< m n (subst T (sym eq) _)))
+
+⊓≡⊓′ : ∀ m n → m ⊓ n ≡ m ⊓′ n
+⊓≡⊓′ m n with m <ᵇ n in eq
+... | false = m≥n⇒m⊓n≡n (≮⇒≥ (λ m<n → subst T eq (<⇒<ᵇ m<n)))
+... | true  = m≤n⇒m⊓n≡m (<⇒≤ (<ᵇ⇒< m n (subst T (sym eq) _)))
+
 ------------------------------------------------------------------------
 -- Derived properties of _⊓_ and _⊔_
 
@@ -1695,6 +1708,11 @@ m≤n⇒∣n-m∣≡n∸m {_} {zero}  z≤n       = refl
 m≤n⇒∣n-m∣≡n∸m {_} {suc m} z≤n       = refl
 m≤n⇒∣n-m∣≡n∸m {_} {_}     (s≤s m≤n) = m≤n⇒∣n-m∣≡n∸m m≤n
 
+m≤n⇒∣m-n∣≡n∸m : ∀ {m n} → m ≤ n → ∣ m - n ∣ ≡ n ∸ m
+m≤n⇒∣m-n∣≡n∸m {_} {zero}  z≤n       = refl
+m≤n⇒∣m-n∣≡n∸m {_} {suc n} z≤n       = refl
+m≤n⇒∣m-n∣≡n∸m {_} {_}     (s≤s m≤n) = m≤n⇒∣m-n∣≡n∸m m≤n
+
 ∣m-n∣≡m∸n⇒n≤m : ∀ {m n} → ∣ m - n ∣ ≡ m ∸ n → n ≤ m
 ∣m-n∣≡m∸n⇒n≤m {zero}  {zero}  eq = z≤n
 ∣m-n∣≡m∸n⇒n≤m {suc m} {zero}  eq = z≤n
@@ -1796,6 +1814,11 @@ m≤∣m-n∣+n m n = subst (m ≤_) (+-comm n _) (m≤n+∣m-n∣ m n)
   where open ≤-Reasoning
 ∣-∣-triangle (suc x) (suc y) (suc z) = ∣-∣-triangle x y z
 
+∣-∣≡∣-∣′ : ∀ m n → ∣ m - n ∣ ≡ ∣ m - n ∣′
+∣-∣≡∣-∣′ m n with m <ᵇ n in eq
+... | false = m≤n⇒∣n-m∣≡n∸m {n} {m} (≮⇒≥ (λ m<n → subst T eq (<⇒<ᵇ m<n)))
+... | true  = m≤n⇒∣m-n∣≡n∸m {m} {n} (<⇒≤ (<ᵇ⇒< m n (subst T (sym eq) _)))
+
 ------------------------------------------------------------------------
 -- Metric structures