resolves issue #1800: deprecates ≤-step etc. throughout

CHANGELOG.md

@@ -908,6 +908,10 @@ Deprecated names
 * In `Data.Nat.Properties`:
   ```
   suc[pred[n]]≡n  ↦  suc-pred
+  ≤-step          ↦  m≤n⇒m≤1+n
+  ≤-stepsˡ        ↦  m≤n⇒m≤o+n
+  ≤-stepsʳ        ↦  m≤n⇒m≤n+o
+  <-step          ↦  m<n⇒m<1+n
   ```
 
 * In `Data.Rational.Unnormalised.Properties`:
@@ -1602,8 +1606,8 @@ Other minor changes
   pattern z<s {n}         = s≤s (z≤n {n})
   pattern s<s {m} {n} m<n = s≤s {m} {n} m<n
 
-  pattern <′-base          = ≤′-refl
-  pattern <′-step {n} m<′n = ≤′-step {n} m<′n
+  pattern n<′1+n               = ≤′-refl
+  pattern m<′n⇒m<′1+n {n} m<′n = ≤′-step {n} m<′n
 
   _! : ℕ → ℕ
   ```

src/Data/Fin/Properties.agda

@@ -163,7 +163,7 @@ toℕ≤pred[n] zero                 = z≤n
 toℕ≤pred[n] (suc {n = suc n} i)  = s≤s (toℕ≤pred[n] i)
 
 toℕ≤n : ∀ (i : Fin n) → toℕ i ℕ.≤ n
-toℕ≤n {suc n} i = ℕₚ.≤-step (toℕ≤pred[n] i)
+toℕ≤n {suc n} i = ℕₚ.m≤n⇒m≤1+n (toℕ≤pred[n] i)
 
 toℕ<n : ∀ (i : Fin n) → toℕ i ℕ.< n
 toℕ<n {suc n} i = s≤s (toℕ≤pred[n] i)
@@ -471,7 +471,7 @@ inject₁ℕ≤ = ℕₚ.<⇒≤ ∘ inject₁ℕ<
 
 i≤inject₁[j]⇒i≤1+j : i ≤ inject₁ j → i ≤ suc j
 i≤inject₁[j]⇒i≤1+j {i = zero} i≤j = z≤n
-i≤inject₁[j]⇒i≤1+j {i = suc i} {j = suc j} (s≤s i≤j) = s≤s (ℕₚ.≤-step (subst (toℕ i ℕ.≤_) (toℕ-inject₁ j) i≤j))
+i≤inject₁[j]⇒i≤1+j {i = suc i} {j = suc j} (s≤s i≤j) = s≤s (ℕₚ.m≤n⇒m≤1+n (subst (toℕ i ℕ.≤_) (toℕ-inject₁ j) i≤j))
 
 ------------------------------------------------------------------------
 -- lower₁

src/Data/Fin/Subset/Properties.agda

@@ -254,7 +254,7 @@ module _ (n : ℕ) where
 p⊆q⇒∣p∣≤∣q∣ : p ⊆ q → ∣ p ∣ ≤ ∣ q ∣
 p⊆q⇒∣p∣≤∣q∣ {p = []}          {[]}          p⊆q = z≤n
 p⊆q⇒∣p∣≤∣q∣ {p = outside ∷ p} {outside ∷ q} p⊆q = p⊆q⇒∣p∣≤∣q∣ (drop-∷-⊆ p⊆q)
-p⊆q⇒∣p∣≤∣q∣ {p = outside ∷ p} {inside  ∷ q} p⊆q = ℕₚ.≤-step (p⊆q⇒∣p∣≤∣q∣ (drop-∷-⊆ p⊆q))
+p⊆q⇒∣p∣≤∣q∣ {p = outside ∷ p} {inside  ∷ q} p⊆q = ℕₚ.m≤n⇒m≤1+n (p⊆q⇒∣p∣≤∣q∣ (drop-∷-⊆ p⊆q))
 p⊆q⇒∣p∣≤∣q∣ {p = inside  ∷ p} {outside ∷ q} p⊆q = contradiction (p⊆q here) λ()
 p⊆q⇒∣p∣≤∣q∣ {p = inside  ∷ p} {inside  ∷ q} p⊆q = s≤s (p⊆q⇒∣p∣≤∣q∣ (drop-∷-⊆ p⊆q))
 

src/Data/Integer/Properties.agda

@@ -1287,9 +1287,9 @@ i<j⇒i≤pred[j] {_} { -[1+ n ]} (-<- n<m) = -≤- n<m
 
 ≤-step-neg : i ≤ j → pred i ≤ j
 ≤-step-neg -≤+               = -≤+
-≤-step-neg (-≤- n≤m)         = -≤- (ℕ.≤-step n≤m)
+≤-step-neg (-≤- n≤m)         = -≤- (ℕ.m≤n⇒m≤1+n n≤m)
 ≤-step-neg (+≤+ z≤n)         = -≤+
-≤-step-neg (+≤+ (s≤s m≤n)) = +≤+ (ℕ.≤-step m≤n)
+≤-step-neg (+≤+ (s≤s m≤n)) = +≤+ (ℕ.m≤n⇒m≤1+n m≤n)
 
 pred-mono : pred Preserves _≤_ ⟶ _≤_
 pred-mono (-≤+ {n = 0})     = -≤- z≤n

src/Data/List/Membership/Propositional/Properties.agda

@@ -361,7 +361,7 @@ finite inj (x ∷ xs) fᵢ∈x∷xs = excluded-middle helper
     ∈-if-not-i i≢j = not-x (i≢j ∘ f-inj ∘ trans fᵢ≡x ∘ sym)
 
     lemma : ∀ {k j} → i ≤ j → ¬ (i ≤ k) → suc j ≢ k
-    lemma i≤j i≰1+j refl = i≰1+j (≤-step i≤j)
+    lemma i≤j i≰1+j refl = i≰1+j (m≤n⇒m≤1+n i≤j)
 
     f′ⱼ∈xs : ∀ j → f′ j ∈ xs
     f′ⱼ∈xs j with i ≤ᵇ j | Reflects.invert (≤ᵇ-reflects-≤ i j)

src/Data/List/Properties.agda

@@ -139,7 +139,7 @@ module _ (f : A → Maybe B) where
   length-mapMaybe []       = z≤n
   length-mapMaybe (x ∷ xs) with f x
   ... | just y  = s≤s (length-mapMaybe xs)
-  ... | nothing = ≤-step (length-mapMaybe xs)
+  ... | nothing = m≤n⇒m≤1+n (length-mapMaybe xs)
 
 ------------------------------------------------------------------------
 -- _++_
@@ -725,7 +725,7 @@ module _ {P : Pred A p} (P? : Decidable P) where
   length-filter : ∀ xs → length (filter P? xs) ≤ length xs
   length-filter []       = z≤n
   length-filter (x ∷ xs) with does (P? x)
-  ... | false = ≤-step (length-filter xs)
+  ... | false = m≤n⇒m≤1+n (length-filter xs)
   ... | true  = s≤s (length-filter xs)
 
   filter-all : ∀ {xs} → All P xs → filter P? xs ≡ xs
@@ -739,15 +739,15 @@ module _ {P : Pred A p} (P? : Decidable P) where
   ... | false because _ = s≤s (length-filter xs)
   ... | yes          px = contradiction px ¬px
   filter-notAll (x ∷ xs) (there any) with does (P? x)
-  ... | false = ≤-step (filter-notAll xs any)
+  ... | false = m≤n⇒m≤1+n (filter-notAll xs any)
   ... | true  = s≤s (filter-notAll xs any)
 
   filter-some : ∀ {xs} → Any P xs → 0 < length (filter P? xs)
   filter-some {x ∷ xs} (here px)   with P? x
   ... | true because _ = z<s
   ... | no         ¬px = contradiction px ¬px
   filter-some {x ∷ xs} (there pxs) with does (P? x)
-  ... | true  = ≤-step (filter-some pxs)
+  ... | true  = m≤n⇒m≤1+n (filter-some pxs)
   ... | false = filter-some pxs
 
   filter-none : ∀ {xs} → All (∁ P) xs → filter P? xs ≡ []
@@ -794,7 +794,7 @@ module _ {R : Rel A p} (R? : B.Decidable R) where
   length-derun [] = ≤-refl
   length-derun (x ∷ []) = ≤-refl
   length-derun (x ∷ y ∷ xs) with does (R? x y) | length-derun (y ∷ xs)
-  ... | true  | r = ≤-step r
+  ... | true  | r = m≤n⇒m≤1+n r
   ... | false | r = s≤s r
 
   length-deduplicate : ∀ xs → length (deduplicate R? xs) ≤ length xs
@@ -832,8 +832,8 @@ module _ {P : Pred A p} (P? : Decidable P) where
                      length ys ≤ length xs × length zs ≤ length xs
   length-partition []       = z≤n , z≤n
   length-partition (x ∷ xs) with does (P? x) | length-partition xs
-  ...  | true  | rec = Prod.map s≤s ≤-step rec
-  ...  | false | rec = Prod.map ≤-step s≤s rec
+  ...  | true  | rec = Prod.map s≤s m≤n⇒m≤1+n rec
+  ...  | false | rec = Prod.map m≤n⇒m≤1+n s≤s rec
 
 ------------------------------------------------------------------------
 -- _ʳ++_

src/Data/List/Relation/Binary/Infix/Heterogeneous/Properties.agda

@@ -70,7 +70,7 @@ module _ {c t} {C : Set c} {T : REL A C t} where
 
 length-mono : ∀ {as bs} → Infix R as bs → length as ≤ length bs
 length-mono (here pref) = Prefixₚ.length-mono pref
-length-mono (there p)   = ℕₚ.≤-step (length-mono p)
+length-mono (there p)   = ℕₚ.m≤n⇒m≤1+n (length-mono p)
 
 ------------------------------------------------------------------------
 -- As an order

src/Data/List/Relation/Binary/Permutation/Setoid/Properties.agda

@@ -116,8 +116,8 @@ Unique-resp-↭ = AllPairs-resp-↭ (_∘ ≈-sym) ≉-resp₂
 
 0<steps : ∀ {xs ys} (xs↭ys : xs ↭ ys) → 0 < steps xs↭ys
 0<steps (refl _)             = z<s
-0<steps (prep eq xs↭ys)      = ≤-step (0<steps xs↭ys)
-0<steps (swap eq₁ eq₂ xs↭ys) = ≤-step (0<steps xs↭ys)
+0<steps (prep eq xs↭ys)      = m<n⇒m<1+n (0<steps xs↭ys)
+0<steps (swap eq₁ eq₂ xs↭ys) = m<n⇒m<1+n (0<steps xs↭ys)
 0<steps (trans xs↭ys xs↭ys₁) =
   <-transˡ (0<steps xs↭ys) (m≤m+n (steps xs↭ys) (steps xs↭ys₁))
 

src/Data/List/Relation/Binary/Sublist/Heterogeneous/Properties.agda

@@ -58,7 +58,7 @@ module _ {a b r} {A : Set a} {B : Set b} {R : REL A B r} where
 
   length-mono-≤ : ∀ {as bs} → Sublist R as bs → length as ≤ length bs
   length-mono-≤ []        = z≤n
-  length-mono-≤ (y ∷ʳ rs) = ℕₚ.≤-step (length-mono-≤ rs)
+  length-mono-≤ (y ∷ʳ rs) = ℕₚ.m≤n⇒m≤1+n (length-mono-≤ rs)
   length-mono-≤ (r ∷ rs)  = s≤s (length-mono-≤ rs)
 
 ------------------------------------------------------------------------
@@ -219,7 +219,7 @@ module _ {a b r} {A : Set a} {B : Set b} {R : REL A B r} where
           Sublist R (drop m as) (drop n bs)
   drop⁺ {m} z≤n       rs        = drop-Sublist m rs
   drop⁺     (s≤s m≥n) []        = []
-  drop⁺     (s≤s m≥n) (y ∷ʳ rs) = drop⁺ (ℕₚ.≤-step m≥n) rs
+  drop⁺     (s≤s m≥n) (y ∷ʳ rs) = drop⁺ (ℕₚ.m≤n⇒m≤1+n m≥n) rs
   drop⁺     (s≤s m≥n) (r ∷ rs)  = drop⁺ m≥n rs
 
   drop⁺-≥ : ∀ {m n as bs} → m ≥ n → Pointwise R as bs →

src/Data/List/Relation/Binary/Suffix/Heterogeneous/Properties.agda

@@ -76,7 +76,7 @@ module _ {a b r} {A : Set a} {B : Set b} {R : REL A B r} where
 
   length-mono : ∀ {as bs} → Suffix R as bs → length as ≤ length bs
   length-mono (here rs)   = ≤-reflexive (Pointwise-length rs)
-  length-mono (there suf) = ≤-step (length-mono suf)
+  length-mono (there suf) = m≤n⇒m≤1+n (length-mono suf)
 
   S[as][bs]⇒∣as∣≢1+∣bs∣ : ∀ {as bs} → Suffix R as bs →
                           length as ≢ suc (length bs)

src/Data/List/Relation/Unary/All/Properties.agda

@@ -30,7 +30,7 @@ open import Data.List.Relation.Binary.Subset.Propositional using (_⊆_)
 open import Data.Maybe.Base as Maybe using (Maybe; just; nothing)
 open import Data.Maybe.Relation.Unary.All as Maybe using (just; nothing)
 open import Data.Nat.Base using (zero; suc; s≤s; _<_; z<s; s<s)
-open import Data.Nat.Properties using (≤-refl; ≤-step)
+open import Data.Nat.Properties using (≤-refl; m≤n⇒m≤1+n)
 open import Data.Product as Prod using (_×_; _,_; uncurry; uncurry′)
 open import Function.Base
 open import Function.Equality using (_⟨$⟩_)
@@ -543,7 +543,7 @@ all-upTo n = applyUpTo⁺₁ id n id
 
 applyDownFrom⁺₁ : ∀ f n → (∀ {i} → i < n → P (f i)) → All P (applyDownFrom f n)
 applyDownFrom⁺₁ f zero    Pf = []
-applyDownFrom⁺₁ f (suc n) Pf = Pf ≤-refl ∷ applyDownFrom⁺₁ f n (Pf ∘ ≤-step)
+applyDownFrom⁺₁ f (suc n) Pf = Pf ≤-refl ∷ applyDownFrom⁺₁ f n (Pf ∘ m≤n⇒m≤1+n)
 
 applyDownFrom⁺₂ : ∀ f n → (∀ i → P (f i)) → All P (applyDownFrom f n)
 applyDownFrom⁺₂ f n Pf = applyDownFrom⁺₁ f n (λ _ → Pf _)

src/Data/List/Relation/Unary/AllPairs/Properties.agda

@@ -16,7 +16,7 @@ open import Data.Bool.Base using (true; false)
 open import Data.Fin.Base using (Fin)
 open import Data.Fin.Properties using (suc-injective)
 open import Data.Nat.Base using (zero; suc; _<_; z≤n; s≤s)
-open import Data.Nat.Properties using (≤-refl; ≤-step)
+open import Data.Nat.Properties using (≤-refl; m<n⇒m<1+n)
 open import Function.Base using (_∘_; flip)
 open import Level using (Level)
 open import Relation.Binary using (Rel; DecSetoid)
@@ -104,7 +104,7 @@ module _ {R : Rel A ℓ} where
   applyDownFrom⁺₁ f zero    Rf = []
   applyDownFrom⁺₁ f (suc n) Rf =
     All.applyDownFrom⁺₁ _ n (flip Rf ≤-refl)  ∷
-    applyDownFrom⁺₁ f n (λ j<i i<n → Rf j<i (≤-step i<n))
+    applyDownFrom⁺₁ f n (λ j<i i<n → Rf j<i (m<n⇒m<1+n i<n))
 
   applyDownFrom⁺₂ : ∀ f n → (∀ i j → R (f i) (f j)) → AllPairs R (applyDownFrom f n)
   applyDownFrom⁺₂ f n Rf = applyDownFrom⁺₁ f n (λ _ _ → Rf _ _)

src/Data/List/Relation/Unary/Any/Properties.agda

@@ -22,7 +22,7 @@ open import Data.List.Membership.Propositional.Properties.Core
 open import Data.List.Relation.Binary.Pointwise
   using (Pointwise; []; _∷_)
 open import Data.Nat using (zero; suc; _<_; z<s; s<s; s≤s)
-open import Data.Nat.Properties using (_≟_; ≤∧≢⇒<; ≤-refl; ≤-step)
+open import Data.Nat.Properties using (_≟_; ≤∧≢⇒<; ≤-refl; m<n⇒m<1+n)
 open import Data.Maybe.Base using (Maybe; just; nothing)
 open import Data.Maybe.Relation.Unary.Any as MAny using (just)
 open import Data.Product as Prod
@@ -506,7 +506,7 @@ module _ {P : A → Set p} where
                    ∃ λ i → i < n × P (f i)
   applyDownFrom⁻ f {suc n} (here p)  = n , ≤-refl , p
   applyDownFrom⁻ f {suc n} (there p) with applyDownFrom⁻ f p
-  ... | i , i<n , pf = i , ≤-step i<n , pf
+  ... | i , i<n , pf = i , m<n⇒m<1+n i<n , pf
 
 ------------------------------------------------------------------------
 -- tabulate

src/Data/List/Relation/Unary/Linked/Properties.agda

@@ -19,7 +19,7 @@ open import Data.List.Relation.Unary.Linked as Linked
 open import Data.Fin.Base using (Fin)
 open import Data.Fin.Properties using (suc-injective)
 open import Data.Nat.Base using (zero; suc; _<_; z<s; s<s)
-open import Data.Nat.Properties using (≤-refl; ≤-pred; ≤-step)
+open import Data.Nat.Properties using (≤-refl; ≤-pred; m≤n⇒m≤1+n)
 open import Data.Maybe.Relation.Binary.Connected
   using (Connected; just; nothing; just-nothing; nothing-just)
 open import Level using (Level)
@@ -118,7 +118,7 @@ module _ {R : Rel A ℓ} where
   applyDownFrom⁺₁ f zero          Rf = []
   applyDownFrom⁺₁ f (suc zero)    Rf = [-]
   applyDownFrom⁺₁ f (suc (suc n)) Rf =
-    Rf ≤-refl ∷ applyDownFrom⁺₁ f (suc n) (Rf ∘ ≤-step)
+    Rf ≤-refl ∷ applyDownFrom⁺₁ f (suc n) (Rf ∘ m≤n⇒m≤1+n)
 
   applyDownFrom⁺₂ : ∀ f n → (∀ i → R (f (suc i)) (f i)) →
                     Linked R (applyDownFrom f n)

src/Data/List/Sort/MergeSort.agda

@@ -23,7 +23,7 @@ open import Data.Maybe.Base using (just)
 open import Relation.Nullary using (does)
 open import Data.Nat using (_<_; _>_; z<s; s<s)
 open import Data.Nat.Induction
-open import Data.Nat.Properties using (≤-step)
+open import Data.Nat.Properties using (m<n⇒m<1+n)
 open import Data.Product as Prod using (_,_)
 open import Function.Base using (_∘_)
 open import Relation.Binary using (DecTotalOrder)
@@ -51,7 +51,7 @@ private
   length-mergePairs : ∀ xs ys xss → length (mergePairs (xs ∷ ys ∷ xss)) < length (xs ∷ ys ∷ xss)
   length-mergePairs _ _ []              = s<s z<s
   length-mergePairs _ _ (xss ∷ [])      = s<s (s<s z<s)
-  length-mergePairs _ _ (xs ∷ ys ∷ xss) = s<s (≤-step (length-mergePairs xs ys xss))
+  length-mergePairs _ _ (xs ∷ ys ∷ xss) = s<s (m<n⇒m<1+n (length-mergePairs xs ys xss))
 
 mergeAll : (xss : List (List A)) → Acc _<_ (length xss) → List A
 mergeAll []        _               = []

src/Data/Nat/Base.agda

@@ -210,13 +210,15 @@ data _≤′_ (m : ℕ) : ℕ → Set where
   ≤′-refl :                         m ≤′ m
   ≤′-step : ∀ {n} (m≤′n : m ≤′ n) → m ≤′ suc n
 
+pattern m≤′n⇒m≤′1+n = ≤′-step
+
 _<′_ : Rel ℕ 0ℓ
 m <′ n = suc m ≤′ n
 
 -- Smart constructors of _<′_
 
-pattern <′-base          = ≤′-refl
-pattern <′-step {n} m<′n = ≤′-step {n} m<′n
+pattern n<′1+n               = ≤′-refl
+pattern m<′n⇒m<′1+n {n} m<′n = ≤′-step {n} m<′n
 
 _≥′_ : Rel ℕ 0ℓ
 m ≥′ n = n ≤′ m

src/Data/Nat/Binary/Properties.agda

@@ -280,7 +280,7 @@ toℕ-mono-< {zero}     {2[1+ _ ]} _               =  ℕₚ.0<1+n
 toℕ-mono-< {zero}     {1+[2 _ ]} _               =  ℕₚ.0<1+n
 toℕ-mono-< {2[1+ x ]} {2[1+ y ]} (even<even x<y) =  begin
   ℕ.suc (2 ℕ.* (ℕ.suc xN))    ≤⟨ ℕₚ.+-monoʳ-≤ 1 (ℕₚ.*-monoʳ-≤ 2 xN<yN) ⟩
-  ℕ.suc (2 ℕ.* yN)            ≤⟨ ℕₚ.≤-step ℕₚ.≤-refl ⟩
+  ℕ.suc (2 ℕ.* yN)            ≤⟨ ℕₚ.n≤1+n _ ⟩
   2 ℕ.+ (2 ℕ.* yN)            ≡⟨ sym (ℕₚ.*-distribˡ-+ 2 1 yN) ⟩
   2 ℕ.* (ℕ.suc yN)            ∎
   where open ℕₚ.≤-Reasoning;  xN = toℕ x;  yN = toℕ y;  xN<yN = toℕ-mono-< x<y
@@ -290,7 +290,7 @@ toℕ-mono-< {1+[2 x ]} {2[1+ y ]} (odd<even (inj₁ x<y)) =   begin
   ℕ.suc (ℕ.suc (2 ℕ.* xN))    ≡⟨⟩
   2 ℕ.+ (2 ℕ.* xN)            ≡⟨ sym (ℕₚ.*-distribˡ-+ 2 1 xN) ⟩
   2 ℕ.* (ℕ.suc xN)            ≤⟨ ℕₚ.*-monoʳ-≤ 2 xN<yN ⟩
-  2 ℕ.* yN                    ≤⟨ ℕₚ.*-monoʳ-≤ 2 (ℕₚ.≤-step ℕₚ.≤-refl) ⟩
+  2 ℕ.* yN                    ≤⟨ ℕₚ.*-monoʳ-≤ 2 (ℕₚ.n≤1+n _) ⟩
   2 ℕ.* (ℕ.suc yN)            ∎
   where open ℕₚ.≤-Reasoning;  xN = toℕ x;  yN = toℕ y;  xN<yN = toℕ-mono-< x<y
 toℕ-mono-< {1+[2 x ]} {2[1+ .x ]} (odd<even (inj₂ refl)) =

src/Data/Nat/Induction.agda

@@ -68,8 +68,8 @@ cRec = build cRecBuilder
 
 <′-wellFounded n = acc (<′-wellFounded′ n)
 
-<′-wellFounded′ (suc n) n <′-base       = <′-wellFounded n
-<′-wellFounded′ (suc n) m (<′-step m<n) = <′-wellFounded′ n m m<n
+<′-wellFounded′ (suc n) n n<′1+n            = <′-wellFounded n
+<′-wellFounded′ (suc n) m (m<′n⇒m<′1+n m<n) = <′-wellFounded′ n m m<n
 
 module _ {ℓ : Level} where
   open WF.All <′-wellFounded ℓ public