[ refactor ] Change definition of Data.Nat.Base._≤‴_ (#2518)

* Fixes #2504

* add missing URL

* typo

* remove spurious delta

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](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
 ------------------
 

src/Data/Nat/Base.agda

@@ -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
 

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<m) with () ← <‴-irrefl refl m<m
-≤‴-irrelevant (≤‴-step m<m) ≤‴-refl     with () ← <‴-irrefl refl m<m
-≤‴-irrelevant (≤‴-step p)   (≤‴-step q) = cong ≤‴-step $ ≤‴-irrelevant p q
+≤‴-irrelevant : Irrelevant _≤‴_
+≤‴-irrelevant (≤‴-reflexive eq₁) (≤‴-reflexive eq₂) = cong ≤‴-reflexive (≡-irrelevant eq₁ eq₂)
+≤‴-irrelevant (≤‴-reflexive eq₁) (≤‴-step q)        with () ← <‴-irrefl eq₁ q
+≤‴-irrelevant (≤‴-step p)        (≤‴-reflexive eq₂) with () ← <‴-irrefl eq₂ p
+≤‴-irrelevant (≤‴-step p)        (≤‴-step q)        = cong ≤‴-step (≤‴-irrelevant p q)
 
 <‴-irrelevant : Irrelevant {A = ℕ} _<‴_
 <‴-irrelevant = ≤‴-irrelevant