Redefines Data.Nat.Base._≤″_ (#1948)

CHANGELOG.md

@@ -585,6 +585,32 @@ Non-backwards compatible changes
  Prime n = ∀ {d} → 2 ≤ d → d < n → d ∤ n
  ```
 
+### Change in the definition of `_≤″_` (issue #1919)
+
+* The definition of `_≤″_` in `Data.Nat.Base` was previously:
+ ```agda
+ record _≤″_ (m n : ℕ) : Set where
+ constructor less-than-or-equal
+ field
+ {k} : ℕ
+ proof : m + k ≡ n
+ ```
+ which introduced a spurious additional definition, when this is in fact, modulo
+ field names and implicit/explicit qualifiers, equivalent to the definition of left-
+ divisibility, `_∣ˡ_` for the `RawMagma` structure of `_+_`. Since the addition of
+ raw bundles to `Data.X.Base`, this definition can now be made directly. Knock-on
+ consequences include the need to retain the old constructor name, now introduced
+ as a pattern synonym, and introduction of (a function equivalent to) the former
+ field name/projection function `proof` as `≤″-proof` in `Data.Nat.Properties`. 
+
+* Accordingly, the definition has been changed to:
+ ```agda
+ _≤″_ : (m n : ℕ) → Set
+ _≤″_ = _∣ˡ_ +-rawMagma
+
+ pattern less-than-or-equal {k} prf = k , prf
+ ```
+
 ### Renaming of `Reflection` modules
 
 * Under the `Reflection` module, there were various impending name clashes
@@ -2584,6 +2610,8 @@ Additions to existing modules
  <⇒<′ : m < n → m <′ n
  <′⇒< : m <′ n → m < n
 
+ ≤″-proof : (le : m ≤″ n) → let less-than-or-equal {k} _ = le in m + k ≡ n
+
  m+n≤p⇒m≤p∸n : m + n ≤ p → m ≤ p ∸ n
  m≤p∸n⇒m+n≤p : n ≤ p → m ≤ p ∸ n → m + n ≤ p
 

src/Data/Nat/Base.agda

@@ -12,8 +12,10 @@
 module Data.Nat.Base where
 
 open import Algebra.Bundles.Raw using (RawMagma; RawMonoid; RawNearSemiring; RawSemiring)
+open import Algebra.Definitions.RawMagma using (_∣ˡ_)
 open import Data.Bool.Base using (Bool; true; false; T; not)
 open import Data.Parity.Base using (Parity; 0ℙ; 1ℙ)
+open import Data.Product.Base using (_,_)
 open import Level using (0ℓ)
 open import Relation.Binary.Core using (Rel)
 open import Relation.Binary.PropositionalEquality.Core
@@ -120,11 +122,59 @@ instance
 >-nonZero⁻¹ (suc n) = z<s
 
 ------------------------------------------------------------------------
--- Arithmetic
+-- Raw bundles
 
 open import Agda.Builtin.Nat public
  using (_+_; _*_) renaming (_-_ to _∸_)
 
++-rawMagma : RawMagma 0ℓ 0ℓ
++-rawMagma = record
+ { _≈_ = _≡_
+ ; _∙_ = _+_
+ }
+
++-0-rawMonoid : RawMonoid 0ℓ 0ℓ
++-0-rawMonoid = record
+ { _≈_ = _≡_
+ ; _∙_ = _+_
+ ; ε = 0
+ }
+
+*-rawMagma : RawMagma 0ℓ 0ℓ
+*-rawMagma = record
+ { _≈_ = _≡_
+ ; _∙_ = _*_
+ }
+
+*-1-rawMonoid : RawMonoid 0ℓ 0ℓ
+*-1-rawMonoid = record
+ { _≈_ = _≡_
+ ; _∙_ = _*_
+ ; ε = 1
+ }
+
++-*-rawNearSemiring : RawNearSemiring 0ℓ 0ℓ
++-*-rawNearSemiring = record
+ { Carrier = _
+ ; _≈_ = _≡_
+ ; _+_ = _+_
+ ; _*_ = _*_
+ ; 0# = 0
+ }
+
++-*-rawSemiring : RawSemiring 0ℓ 0ℓ
++-*-rawSemiring = record
+ { Carrier = _
+ ; _≈_ = _≡_
+ ; _+_ = _+_
+ ; _*_ = _*_
+ ; 0# = 0
+ ; 1# = 1
+ }
+
+------------------------------------------------------------------------
+-- Arithmetic
+
 open import Agda.Builtin.Nat
  using (div-helper; mod-helper)
 
@@ -260,14 +310,12 @@ m >′ n = n <′ m
 
 ------------------------------------------------------------------------
 -- Another alternative definition of _≤_
+infix 4 _≤″_ _<″_ _≥″_ _>″_
 
-record _≤″_ (m n : ℕ) : Set where
- constructor less-than-or-equal
- field
- {k} : ℕ
- proof : m + k ≡ n
+_≤″_ : (m n : ℕ) → Set
+_≤″_ = _∣ˡ_ +-rawMagma
 
-infix 4 _≤″_ _<″_ _≥″_ _>″_
+pattern less-than-or-equal {k} proof = k , proof
 
 _<″_ : Rel ℕ 0ℓ
 m <″ n = suc m ≤″ n
@@ -316,51 +364,12 @@ compare (suc m) (suc n) with compare m n
 ... | equal m = equal (suc m)
 ... | greater n k = greater (suc n) k
 
-------------------------------------------------------------------------
--- Raw bundles
-
-+-rawMagma : RawMagma 0ℓ 0ℓ
-+-rawMagma = record
- { _≈_ = _≡_
- ; _∙_ = _+_
- }
-
-+-0-rawMonoid : RawMonoid 0ℓ 0ℓ
-+-0-rawMonoid = record
- { _≈_ = _≡_
- ; _∙_ = _+_
- ; ε = 0
- }
-
-*-rawMagma : RawMagma 0ℓ 0ℓ
-*-rawMagma = record
- { _≈_ = _≡_
- ; _∙_ = _*_
- }
-
-*-1-rawMonoid : RawMonoid 0ℓ 0ℓ
-*-1-rawMonoid = record
- { _≈_ = _≡_
- ; _∙_ = _*_
- ; ε = 1
- }
 
-+-*-rawNearSemiring : RawNearSemiring 0ℓ 0ℓ
-+-*-rawNearSemiring = record
- { Carrier = _
- ; _≈_ = _≡_
- ; _+_ = _+_
- ; _*_ = _*_
- ; 0# = 0
- }
+------------------------------------------------------------------------
+-- DEPRECATED NAMES
+------------------------------------------------------------------------
+-- Please use the new names as continuing support for the old names is
+-- not guaranteed.
 
-+-*-rawSemiring : RawSemiring 0ℓ 0ℓ
-+-*-rawSemiring = record
- { Carrier = _
- ; _≈_ = _≡_
- ; _+_ = _+_
- ; _*_ = _*_
- ; 0# = 0
- ; 1# = 1
- }
+-- Version 2.0
 

src/Data/Nat/Properties.agda

@@ -2065,6 +2065,11 @@ m<ᵇ1+m+n m = <⇒<ᵇ (m≤m+n (suc m) _)
 <″⇒<ᵇ : ∀ {m n} → m <″ n → T (m <ᵇ n)
 <″⇒<ᵇ {m} (less-than-or-equal refl) = <⇒<ᵇ (m≤m+n (suc m) _)
 
+-- equivalence to the old definition of _≤″_
+
+≤″-proof : ∀ {m n} (le : m ≤″ n) → let less-than-or-equal {k} _ = le in m + k ≡ n
+≤″-proof (less-than-or-equal prf) = prf
+
 -- equivalence to _≤_
 
 ≤″⇒≤ : _≤″_ ⇒ _≤_
@@ -2099,8 +2104,8 @@ _>″?_ = flip _<″?_
 ≤″-irrelevant : Irrelevant _≤″_
 ≤″-irrelevant {m} (less-than-or-equal eq₁)
  (less-than-or-equal eq₂)
- with +-cancelˡ-≡ m _ _ (trans eq₁ (sym eq₂))
-... | refl = cong less-than-or-equal (≡-irrelevant eq₁ eq₂)
+ with refl ← +-cancelˡ-≡ m _ _ (trans eq₁ (sym eq₂))
+  = cong less-than-or-equal (≡-irrelevant eq₁ eq₂)
 
 <″-irrelevant : Irrelevant _<″_
 <″-irrelevant = ≤″-irrelevant
@@ -2116,17 +2121,15 @@ _>″?_ = flip _<″?_
 ------------------------------------------------------------------------
 
 ≤‴⇒≤″ : ∀{m n} → m ≤‴ n → m ≤″ n
-≤‴⇒≤″ {m = m} ≤‴-refl = less-than-or-equal {k = 0} (+-identityʳ m)
-≤‴⇒≤″ {m = m} (≤‴-step x) = less-than-or-equal (trans (+-suc m _) (_≤″_.proof ind)) where
- ind = ≤‴⇒≤″ x
+≤‴⇒≤″ {m = m} ≤‴-refl = less-than-or-equal {k = 0} (+-identityʳ m)
+≤‴⇒≤″ {m = m} (≤‴-step m≤n) = less-than-or-equal (trans (+-suc m _) (≤″-proof (≤‴⇒≤″ m≤n)))
 
 m≤‴m+k : ∀{m n k} → m + k ≡ n → m ≤‴ n
-m≤‴m+k {m} {k = zero} refl = subst (λ z → m ≤‴ z) (sym (+-identityʳ m)) (≤‴-refl {m})
-m≤‴m+k {m} {k = suc k} proof
- = ≤‴-step (m≤‴m+k {k = k} (trans (sym (+-suc m _)) proof))
+m≤‴m+k {m} {k = zero} refl = subst (λ z → m ≤‴ z) (sym (+-identityʳ m)) (≤‴-refl {m})
+m≤‴m+k {m} {k = suc k} prf = ≤‴-step (m≤‴m+k {k = k} (trans (sym (+-suc m _)) prf))
 
 ≤″⇒≤‴ : ∀{m n} → m ≤″ n → m ≤‴ n
-≤″⇒≤‴ (less-than-or-equal {k} proof) = m≤‴m+k proof
+≤″⇒≤‴ m≤n = m≤‴m+k (≤″-proof m≤n)
 
 0≤‴n : ∀{n} → 0 ≤‴ n
 0≤‴n {n} = m≤‴m+k refl