diff --git a/CHANGELOG.md b/CHANGELOG.md index 7975dcc77b..612e45673e 100644 --- a/CHANGELOG.md +++ b/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 diff --git a/src/Data/Nat/Base.agda b/src/Data/Nat/Base.agda index 4ae0acc2dd..b0a0eafcd6 100644 --- a/src/Data/Nat/Base.agda +++ b/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′ 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 diff --git a/src/Data/Nat/Properties.agda b/src/Data/Nat/Properties.agda index 5ed9b64e43..507dfe0a08 100644 --- a/src/Data/Nat/Properties.agda +++ b/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