From 3410deedb2b3cf0206c5d5dff47a35ea930df9c2 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Thu, 12 Dec 2024 10:41:11 +0000 Subject: [PATCH 1/4] Fixes #2504 --- CHANGELOG.md | 2 ++ src/Data/Nat/Base.agda | 14 +++++++++----- src/Data/Nat/Properties.agda | 35 ++++++++++++++++------------------- 3 files changed, 27 insertions(+), 24 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 4c4a9619c7..836eeaac20 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -30,6 +30,8 @@ Non-backwards compatible changes them to name the operation `+`. * `distribˡ` and `distribʳ` are defined in the record. +* [issue #2504]() In `Data.Nat.Base` the definition of `_≤‴_` has been modified to make the witness to equality explicit in a new `≤‴-reflexive` constructor; a pattern synonym ≤‴-refl` has been added for backwards compatibility but NB. the chnage in parametrisation means that this pattern is *not* well-formed if the old implicit arguments `m`,`n` are supplied explicitly. + Minor improvements ------------------ diff --git a/src/Data/Nat/Base.agda b/src/Data/Nat/Base.agda index 91766048e8..16d68fc7d5 100644 --- a/src/Data/Nat/Base.agda +++ b/src/Data/Nat/Base.agda @@ -335,7 +335,7 @@ suc n ! = suc n * n ! -- _≤′_: this definition is more suitable for well-founded induction -- (see Data.Nat.Induction) -infix 4 _≤′_ _<′_ _≥′_ _>′_ +infix 4 _<′_ _≤′_ _≥′_ _>′_ data _≤′_ (m : ℕ) : ℕ → Set where ≤′-refl : m ≤′ m @@ -379,15 +379,19 @@ s<″s⁻¹ (k , eq) = k , cong pred eq -- _≤‴_: this definition is useful for induction with an upper bound. -data _≤‴_ : ℕ → ℕ → Set where - ≤‴-refl : ∀{m} → m ≤‴ m - ≤‴-step : ∀{m n} → suc m ≤‴ n → m ≤‴ n - infix 4 _≤‴_ _<‴_ _≥‴_ _>‴_ +data _≤‴_ (m n : ℕ) : Set + _<‴_ : Rel ℕ 0ℓ m <‴ n = suc m ≤‴ n +data _≤‴_ m n where + ≤‴-reflexive : m ≡ n → m ≤‴ n + ≤‴-step : m <‴ n → m ≤‴ n + +pattern ≤‴-refl = ≤‴-reflexive refl + _≥‴_ : Rel ℕ 0ℓ m ≥‴ n = n ≤‴ m diff --git a/src/Data/Nat/Properties.agda b/src/Data/Nat/Properties.agda index 68efe6bcdf..044e9bdefe 100644 --- a/src/Data/Nat/Properties.agda +++ b/src/Data/Nat/Properties.agda @@ -2196,25 +2196,25 @@ _>″?_ = flip _<″?_ -- Properties of _≤‴_ ------------------------------------------------------------------------ -≤‴⇒≤″ : ∀{m n} → m ≤‴ n → m ≤″ n -≤‴⇒≤″ {m = m} ≤‴-refl = 0 , +-identityʳ m -≤‴⇒≤″ {m = m} (≤‴-step m≤n) = _ , trans (+-suc m _) (≤″-proof (≤‴⇒≤″ m≤n)) +≤‴⇒≤″ : m ≤‴ n → m ≤″ n +≤‴⇒≤″ ≤‴-refl = _ , +-identityʳ _ +≤‴⇒≤″ (≤‴-step m≤n) = _ , trans (+-suc _ _) (≤″-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} prf = ≤‴-step (m≤‴m+k {k = k} (trans (sym (+-suc m _)) prf)) +m≤‴m+k : m + k ≡ n → m ≤‴ n +m≤‴m+k {k = zero} = ≤‴-reflexive ∘ trans (sym (+-identityʳ _)) +m≤‴m+k {k = suc _} = ≤‴-step ∘ m≤‴m+k ∘ trans (sym (+-suc _ _)) -≤″⇒≤‴ : ∀{m n} → m ≤″ n → m ≤‴ n -≤″⇒≤‴ m≤n = m≤‴m+k (≤″-proof m≤n) +≤″⇒≤‴ : m ≤″ n → m ≤‴ n +≤″⇒≤‴ = m≤‴m+k ∘ ≤″-proof 0≤‴n : 0 ≤‴ n 0≤‴n = m≤‴m+k refl <ᵇ⇒<‴ : T (m <ᵇ n) → m <‴ n -<ᵇ⇒<‴ leq = ≤″⇒≤‴ (<ᵇ⇒<″ leq) +<ᵇ⇒<‴ = ≤″⇒≤‴ ∘ <ᵇ⇒<″ -<‴⇒<ᵇ : ∀ {m n} → m <‴ n → T (m <ᵇ n) -<‴⇒<ᵇ leq = <″⇒<ᵇ (≤‴⇒≤″ leq) +<‴⇒<ᵇ : m <‴ n → T (m <ᵇ n) +<‴⇒<ᵇ = <″⇒<ᵇ ∘ ≤‴⇒≤″ infix 4 _<‴?_ _≤‴?_ _≥‴?_ _>‴?_ @@ -2240,14 +2240,11 @@ _>‴?_ = flip _<‴?_ <‴-irrefl : Irreflexive _≡_ _<‴_ <‴-irrefl eq = <-irrefl eq ∘ ≤‴⇒≤ -≤‴-irrelevant : Irrelevant {A = ℕ} _≤‴_ -≤‴-irrelevant ≤‴-refl = lemma refl - where - lemma : ∀ {m n} → (e : m ≡ n) → (q : m ≤‴ n) → subst (m ≤‴_) e ≤‴-refl ≡ q - lemma {m} e ≤‴-refl = cong (λ e → subst (m ≤‴_) e ≤‴-refl) $ ≡-irrelevant e refl - lemma refl (≤‴-step m Date: Thu, 12 Dec 2024 10:48:22 +0000 Subject: [PATCH 2/4] add missing URL --- CHANGELOG.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 836eeaac20..3f38441d1a 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -30,7 +30,7 @@ Non-backwards compatible changes them to name the operation `+`. * `distribˡ` and `distribʳ` are defined in the record. -* [issue #2504]() In `Data.Nat.Base` the definition of `_≤‴_` has been modified to make the witness to equality explicit in a new `≤‴-reflexive` constructor; a pattern synonym ≤‴-refl` has been added for backwards compatibility but NB. the chnage in parametrisation means that this pattern is *not* well-formed if the old implicit arguments `m`,`n` are supplied explicitly. +* [issue #2504](https://github.com/agda/agda-stdlib/issues/2504) In `Data.Nat.Base` the definition of `_≤‴_` has been modified to make the witness to equality explicit in a new `≤‴-reflexive` constructor; a pattern synonym ≤‴-refl` has been added for backwards compatibility but NB. the chnage in parametrisation means that this pattern is *not* well-formed if the old implicit arguments `m`,`n` are supplied explicitly. Minor improvements ------------------ From 9474b36fc3c8e5c0c76d358beb0630886bdd79f3 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Thu, 12 Dec 2024 11:16:42 +0000 Subject: [PATCH 3/4] typo --- CHANGELOG.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 3f38441d1a..6d8c89afbe 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -30,7 +30,7 @@ Non-backwards compatible changes them to name the operation `+`. * `distribˡ` and `distribʳ` are defined in the record. -* [issue #2504](https://github.com/agda/agda-stdlib/issues/2504) In `Data.Nat.Base` the definition of `_≤‴_` has been modified to make the witness to equality explicit in a new `≤‴-reflexive` constructor; a pattern synonym ≤‴-refl` has been added for backwards compatibility but NB. the chnage in parametrisation means that this pattern is *not* well-formed if the old implicit arguments `m`,`n` are supplied explicitly. +* [issue #2504](https://github.com/agda/agda-stdlib/issues/2504) In `Data.Nat.Base` the definition of `_≤‴_` has been modified to make the witness to equality explicit in a new `≤‴-reflexive` constructor; a pattern synonym ≤‴-refl` has been added for backwards compatibility but NB. the change in parametrisation means that this pattern is *not* well-formed if the old implicit arguments `m`,`n` are supplied explicitly. Minor improvements ------------------ From 3aac52bd108566f9f7776e591e22567e8ae0ec0f Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Thu, 12 Dec 2024 11:43:38 +0000 Subject: [PATCH 4/4] remove spurious delta --- src/Data/Nat/Base.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Data/Nat/Base.agda b/src/Data/Nat/Base.agda index 16d68fc7d5..58e3e2644f 100644 --- a/src/Data/Nat/Base.agda +++ b/src/Data/Nat/Base.agda @@ -335,7 +335,7 @@ suc n ! = suc n * n ! -- _≤′_: this definition is more suitable for well-founded induction -- (see Data.Nat.Induction) -infix 4 _<′_ _≤′_ _≥′_ _>′_ +infix 4 _≤′_ _<′_ _≥′_ _>′_ data _≤′_ (m : ℕ) : ℕ → Set where ≤′-refl : m ≤′ m