Redefines Data.Nat.Base._≤″_

CHANGELOG.md

@@ -427,6 +427,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 deprecation of (a function equiavlent to) the former
+  field name/projection function `proof`. 
+
+* Accordingly, the definition has been changed to:
+  ```agda
+  _≤″_ : (m n : ℕ)  → Set
+  _≤″_ = _∣ˡ_ +-rawMagma
+
+  pattern less-than-or-equal {k} proof = k , proof
+  ```
+
 ### Renaming of `Reflection` modules
 
 * Under the `Reflection` module, there were various impending name clashes
@@ -1109,6 +1135,11 @@ Deprecated names
   map-with-∈↔  ↦  mapWith∈↔
   ```
 
+* In `Data.Nat.Base`:
+  ```
+  _≤″_.proof ↦  Data.Product.Base.proj₂
+  ```
+
 * In `Data.Nat.Properties`:
   ```
   suc[pred[n]]≡n  ↦  suc-pred

README/Design/Decidability.agda

@@ -11,7 +11,7 @@ module README.Design.Decidability where
 open import Data.Bool
 open import Data.List
 open import Data.List.Properties using (∷-injective)
-open import Data.Nat
+open import Data.Nat hiding (proof)
 open import Data.Nat.Properties using (suc-injective)
 open import Data.Product
 open import Data.Unit

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)
 
@@ -258,14 +308,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
@@ -314,51 +362,17 @@ 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
 
+proof : ∀ {m n} (le : m ≤″ n) → let less-than-or-equal {k} _ = le in m + k ≡ n
+proof (less-than-or-equal {k} prf) = prf
+{-# WARNING_ON_USAGE proof
+"Warning: _≤″_.proof was deprecated in v2.0. Please use pattern-matching on less-than-or-equal instead. Note that the definition of _≤″_ has changed"
+#-}

src/Data/Nat/Combinatorics.agda

@@ -12,7 +12,7 @@ open import Data.Nat.Base
 open import Data.Nat.DivMod
 open import Data.Nat.Divisibility
 open import Data.Nat.Properties
-open import Relation.Binary.Definitions 
+open import Relation.Binary.Definitions
 open import Relation.Binary.PropositionalEquality
   using (_≡_; refl; sym; cong; subst)
 
@@ -118,7 +118,7 @@ module _ {n k} (k<n : k < n) where
 
     [n-k]!           = [n-k] !
     [n-k-1]!         = [n-k-1] !
-  
+
     [n-k]≡1+[n-k-1]  : [n-k] ≡ suc [n-k-1]
     [n-k]≡1+[n-k-1]  = +-∸-assoc 1 k<n
 

src/Data/Nat/Properties.agda

@@ -2098,8 +2098,8 @@ _>″?_ = 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} (≤‴-step x) with less-than-or-equal proof ← ≤‴⇒≤″ x
+  = less-than-or-equal (trans (+-suc m _) proof)
 
 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})