Refactoring (inversion) properties of _<_ on Nat, plus consequences (agda#2000)

Author: jamesmckinna

CHANGELOG.md

@@ -1276,7 +1276,7 @@ Deprecated modules
 
 ### Deprecation of `Data.Nat.Properties.Core`
 
-* The module `Data.Nat.Properties.Core` has been deprecated, and its one entry moved to `Data.Nat.Properties`
+* The module `Data.Nat.Properties.Core` has been deprecated, and its one lemma moved to `Data.Nat.Base`, renamed as `s≤s⁻¹`
 
 ### Deprecation of `Data.Fin.Substitution.Example`
 
@@ -1543,6 +1543,7 @@ Deprecated names
   ≤-stepsˡ        ↦  m≤n⇒m≤o+n
   ≤-stepsʳ        ↦  m≤n⇒m≤n+o
   <-step          ↦  m<n⇒m<1+n
+  pred-mono       ↦  pred-mono-≤
 
   <-transʳ        ↦  ≤-<-trans
   <-transˡ        ↦  <-≤-trans
@@ -2618,9 +2619,18 @@ Additions to existing modules
   pattern z<s {n}         = s≤s (z≤n {n})
   pattern s<s {m} {n} m<n = s≤s {m} {n} m<n
 
+  s≤s⁻¹ : suc m ≤ suc n → m ≤ n
+  s<s⁻¹ : suc m < suc n → m < n
+
   pattern <′-base          = ≤′-refl
   pattern <′-step {n} m<′n = ≤′-step {n} m<′n
 
+  pattern ≤″-offset k = less-than-or-equal {k} refl
+  pattern <″-offset k = ≤″-offset k
+
+  s≤″s⁻¹ : ∀ {m n} → suc m ≤″ suc n → m ≤″ n
+  s<″s⁻¹ : ∀ {m n} → suc m <″ suc n → m <″ n
+
   _⊔′_ : ℕ → ℕ → ℕ
   _⊓′_ : ℕ → ℕ → ℕ
   ∣_-_∣′ : ℕ → ℕ → ℕ
@@ -2671,12 +2681,13 @@ Additions to existing modules
   m*n≢0     : .{{_ : NonZero m}} .{{_ : NonZero n}} → NonZero (m * n)
   m≤n⇒n∸m≤n : m ≤ n → n ∸ m ≤ n
 
-  ≤-pred        : suc m ≤ suc n → m ≤ n
   s<s-injective : ∀ {p q : m < n} → s<s p ≡ s<s q → p ≡ q
-  <-pred        : suc m < suc n → m < n
   <-step        : m < n → m < 1 + n
   m<1+n⇒m<n∨m≡n : m < suc n → m < n ⊎ m ≡ n
 
+  pred-mono-≤   : m ≤ n → pred m ≤ pred n
+  pred-mono-<   : .⦃ _ : NonZero m ⦄ → m < n → pred m < pred n
+
   z<′s : zero <′ suc n
   s<′s : m <′ n → suc m <′ suc n
   <⇒<′ : m < n → m <′ n

src/Data/Digit/Properties.agda

@@ -15,7 +15,7 @@ open import Data.Product.Base using (_,_; proj₁)
 open import Data.Vec.Relation.Unary.Unique.Propositional using (Unique)
 import Data.Vec.Relation.Unary.Unique.Propositional.Properties as Uniqueₚ
 open import Data.Vec.Relation.Unary.AllPairs using (allPairs?)
-open import Relation.Nullary.Decidable using (True; from-yes; ¬?)
+open import Relation.Nullary.Decidable.Core using (True; from-yes; ¬?)
 open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl)
 open import Function.Base using (_∘_)
 

src/Data/Fin/Base.agda

@@ -11,17 +11,16 @@
 
 module Data.Fin.Base where
 
-open import Data.Bool.Base using (Bool; true; false; T; not)
-open import Data.Nat.Base as ℕ using (ℕ; zero; suc; z≤n; s≤s; z<s; s<s; _^_)
+open import Data.Bool.Base using (Bool; T)
+open import Data.Nat.Base as ℕ using (ℕ; zero; suc)
 open import Data.Product.Base as Product using (_×_; _,_; proj₁; proj₂)
 open import Data.Sum.Base as Sum using (_⊎_; inj₁; inj₂; [_,_]′)
 open import Function.Base using (id; _∘_; _on_; flip)
 open import Level using (0ℓ)
-open import Relation.Nullary.Negation.Core using (contradiction)
-open import Relation.Nullary.Decidable.Core using (yes; no; True; toWitness)
 open import Relation.Binary.Core
 open import Relation.Binary.PropositionalEquality.Core using (_≡_; _≢_; refl; cong)
 open import Relation.Binary.Indexed.Heterogeneous.Core using (IRel)
+open import Relation.Nullary.Negation.Core using (contradiction)
 
 private
   variable
@@ -68,16 +67,15 @@ fromℕ (suc n) = suc (fromℕ n)
 
 -- fromℕ< {m} _ = "m".
 
-fromℕ< : m ℕ.< n → Fin n
-fromℕ< {zero}  {suc n} z<s = zero
-fromℕ< {suc m} {suc n} (s<s m<n) = suc (fromℕ< m<n)
+fromℕ< : .(m ℕ.< n) → Fin n
+fromℕ< {zero}  {suc _} _   = zero
+fromℕ< {suc m} {suc _} m<n = suc (fromℕ< (ℕ.s<s⁻¹ m<n))
 
 -- fromℕ<″ m _ = "m".
 
-fromℕ<″ : ∀ m {n} → m ℕ.<″ n → Fin n
-fromℕ<″ zero    (ℕ.less-than-or-equal refl) = zero
-fromℕ<″ (suc m) (ℕ.less-than-or-equal refl) =
-  suc (fromℕ<″ m (ℕ.less-than-or-equal refl))
+fromℕ<″ : ∀ m {n} → .(m ℕ.<″ n) → Fin n
+fromℕ<″ zero    {suc _} _    = zero
+fromℕ<″ (suc m) {suc _} m<″n = suc (fromℕ<″ m (ℕ.s<″s⁻¹ m<″n))
 
 -- canonical liftings of i:Fin m to larger index
 
@@ -95,9 +93,9 @@ zero    ↑ʳ i = i
 
 -- reduce≥ "m + i" _ = "i".
 
-reduce≥ : ∀ (i : Fin (m ℕ.+ n)) (i≥m : toℕ i ℕ.≥ m) → Fin n
-reduce≥ {zero}  i       i≥m       = i
-reduce≥ {suc m} (suc i) (s≤s i≥m) = reduce≥ i i≥m
+reduce≥ : ∀ (i : Fin (m ℕ.+ n)) → .(m ℕ.≤ toℕ i) → Fin n
+reduce≥ {zero}  i       _   = i
+reduce≥ {suc _} (suc i) m≤i = reduce≥ i (ℕ.s≤s⁻¹ m≤i)
 
 -- inject⋆ m "i" = "i".
 
@@ -106,16 +104,16 @@ inject {i = suc i} zero    = zero
 inject {i = suc i} (suc j) = suc (inject j)
 
 inject! : ∀ {i : Fin (suc n)} → Fin′ i → Fin n
-inject! {n = suc _} {i = suc _}  zero    = zero
-inject! {n = suc _} {i = suc _}  (suc j) = suc (inject! j)
+inject! {n = suc _} {i = suc _} zero    = zero
+inject! {n = suc _} {i = suc _} (suc j) = suc (inject! j)
 
 inject₁ : Fin n → Fin (suc n)
 inject₁ zero    = zero
 inject₁ (suc i) = suc (inject₁ i)
 
-inject≤ : Fin m → m ℕ.≤ n → Fin n
-inject≤ {_} {suc n} zero    _         =  zero
-inject≤ {_} {suc n} (suc i) (s≤s m≤n) = suc (inject≤ i m≤n)
+inject≤ : Fin m → .(m ℕ.≤ n) → Fin n
+inject≤ {n = suc _} zero    _   = zero
+inject≤ {n = suc _} (suc i) m≤n = suc (inject≤ i (ℕ.s≤s⁻¹ m≤n))
 
 -- lower₁ "i" _ = "i".
 
@@ -166,12 +164,12 @@ combine {suc m} {n} zero    j = j ↑ˡ (m ℕ.* n)
 combine {suc m} {n} (suc i) j = n ↑ʳ (combine i j)
 
 -- Next in progression after splitAt and remQuot
-finToFun : Fin (m ^ n) → (Fin n → Fin m)
-finToFun {m} {suc n} i zero    = quotient (m ^ n) i
-finToFun {m} {suc n} i (suc j) = finToFun (remainder {m} (m ^ n) i) j
+finToFun : Fin (m ℕ.^ n) → (Fin n → Fin m)
+finToFun {m} {suc n} i zero    = quotient (m ℕ.^ n) i
+finToFun {m} {suc n} i (suc j) = finToFun (remainder {m} (m ℕ.^ n) i) j
 
 -- inverse of above function
-funToFin : (Fin m → Fin n) → Fin (n ^ m)
+funToFin : (Fin m → Fin n) → Fin (n ℕ.^ m)
 funToFin {zero}  f = zero
 funToFin {suc m} f = combine (f zero) (funToFin (f ∘ suc))