Remove (almost!) all external use of _≤″_ beyond Data.Nat.*

CHANGELOG.md

@@ -75,20 +75,32 @@ Additions to existing modules
   nonZeroDivisor : DivMod dividend divisor → NonZero divisor
   ```
 
-* Added new proofs in `Data.Nat.Properties`:
+* Added new proofs and pattern synonyms in `Data.Nat.Properties`:
   ```agda
   m≤n+o⇒m∸n≤o : ∀ m n {o} → m ≤ n + o → m ∸ n ≤ o
   m<n+o⇒m∸n<o : ∀ m n {o} → .{{NonZero o}} → m < n + o → m ∸ n < o
   pred-cancel-≤ : pred m ≤ pred n → (m ≡ 1 × n ≡ 0) ⊎ m ≤ n
   pred-cancel-< : pred m < pred n → m < n
   pred-injective : .{{NonZero m}} → .{{NonZero n}} → pred m ≡ pred n → m ≡ n
   pred-cancel-≡ : pred m ≡ pred n → ((m ≡ 0 × n ≡ 1) ⊎ (m ≡ 1 × n ≡ 0)) ⊎ m ≡ n
+
+  <⇒<″    : _<_ ⇒ _<″_
+  ≤-proof : m ≤ n → ∃ λ k → m + k ≡ n
+
+  pattern ≤-offset k = k , refl
+  pattern <-offset k = ≤-offset k
   ```
 
 * Added new functions in `Data.String.Base`:
   ```agda
   map : (Char → Char) → String → String
   ```
 
+* Added new functions in `Data.Vec.Bounded.Base`:
+  ```agda
+  isBounded : (as : Vec≤ A n) → Vec≤.length as ≤ n
+  toVec     : (as : Vec≤ A n) → Vec A (Vec≤.length as)
+  ```
+
 * In `Function.Bundles`, added `_⟶ₛ_` as a synonym for `Func` that can
   be used infix.

src/Data/Nat/Properties.agda

@@ -2101,31 +2101,43 @@ n≤′m+n (suc m) n = ≤′-step (n≤′m+n m n)
 -- Properties of _≤″_ and _<″_
 ------------------------------------------------------------------------
 
-m<ᵇn⇒1+m+[n-1+m]≡n : ∀ m n → T (m <ᵇ n) → suc m + (n ∸ suc m) ≡ n
-m<ᵇn⇒1+m+[n-1+m]≡n m n lt = m+[n∸m]≡n (<ᵇ⇒< m n lt)
+-- equivalence of  _≤″_ to _≤_
 
-m<ᵇ1+m+n : ∀ m {n} → T (m <ᵇ suc (m + n))
-m<ᵇ1+m+n m = <⇒<ᵇ (m≤m+n (suc m) _)
+≤⇒≤″ : _≤_ ⇒ _≤″_
+≤⇒≤″ = less-than-or-equal ∘ m+[n∸m]≡n
 
-<ᵇ⇒<″ : T (m <ᵇ n) → m <″ n
-<ᵇ⇒<″ {m} {n} leq = less-than-or-equal (m+[n∸m]≡n (<ᵇ⇒< m n leq))
+<⇒<″ : _<_ ⇒ _<″_
+<⇒<″ = ≤⇒≤″
 
-<″⇒<ᵇ : ∀ {m n} → m <″ n → T (m <ᵇ n)
-<″⇒<ᵇ {m} (<″-offset k) = <⇒<ᵇ (m≤m+n (suc m) k)
+≤″⇒≤ : _≤″_ ⇒ _≤_
+≤″⇒≤ (≤″-offset k) = m≤m+n _ k
 
 -- equivalence to the old definition of _≤″_
 
-≤″-proof : ∀ {m n} (le : m ≤″ n) → let less-than-or-equal {k} _ = le in m + k ≡ n
+≤″-proof : (le : m ≤″ n) → let less-than-or-equal {k} _ = le in m + k ≡ n
 ≤″-proof (less-than-or-equal prf) = prf
 
--- equivalence to _≤_
+-- yielding corresponding proof and `pattern` aliases for _≤″_/_<_
 
-≤″⇒≤ : _≤″_ ⇒ _≤_
-≤″⇒≤ {zero}  (≤″-offset k) = z≤n {k}
-≤″⇒≤ {suc m} (≤″-offset k) = s≤s (≤″⇒≤ (≤″-offset k))
+≤-proof : m ≤ n → ∃ λ k → m + k ≡ n
+≤-proof le = _ , ≤″-proof (≤⇒≤″ le)
 
-≤⇒≤″ : _≤_ ⇒ _≤″_
-≤⇒≤″ = less-than-or-equal ∘ m+[n∸m]≡n
+pattern ≤-offset k = k , refl
+pattern <-offset k = ≤-offset k
+
+-- equivalence of _<″_ to _<ᵇ_
+
+m<ᵇn⇒1+m+[n-1+m]≡n : ∀ m n → T (m <ᵇ n) → suc m + (n ∸ suc m) ≡ n
+m<ᵇn⇒1+m+[n-1+m]≡n m n lt = m+[n∸m]≡n (<ᵇ⇒< m n lt)
+
+m<ᵇ1+m+n : ∀ m {n} → T (m <ᵇ suc (m + n))
+m<ᵇ1+m+n m = <⇒<ᵇ (m≤m+n (suc m) _)
+
+<ᵇ⇒<″ : T (m <ᵇ n) → m <″ n
+<ᵇ⇒<″ {m} {n} = <⇒<″ ∘ (<ᵇ⇒< m n)
+
+<″⇒<ᵇ : ∀ {m n} → m <″ n → T (m <ᵇ n)
+<″⇒<ᵇ {m} (<″-offset k) = <⇒<ᵇ (m≤m+n (suc m) k)
 
 -- NB: we use the builtin function `_<ᵇ_ : (m n : ℕ) → Bool` here so
 -- that the function quickly decides whether to return `yes` or `no`.

src/Data/Vec/Bounded/Base.agda

@@ -43,20 +43,27 @@ record Vec≤ (A : Set a) (n : ℕ) : Set a where
         vec      : Vec A length
         .bound   : length ≤ n
 
+-- projection to recompute irrelevant field
+isBounded : (as : Vec≤ A n) → Vec≤.length as ≤ n
+isBounded as@(_ , m≤n) = recompute (_ ℕ.≤? _) m≤n
+
 ------------------------------------------------------------------------
 -- Conversion functions
 
+toVec : (as : Vec≤ A n) → Vec A (Vec≤.length as)
+toVec as@(vs , _) = vs
+
 fromVec : Vec A n → Vec≤ A n
 fromVec v = v , ℕ.≤-refl
 
 padRight : A → Vec≤ A n → Vec A n
-padRight a (vs , m≤n)
-  with ≤″-offset k ← recompute (_ ℕ.≤″? _) (ℕ.≤⇒≤″ m≤n)
+padRight a as@(vs , m≤n)
+  with ℕ.≤-offset k ← ℕ.≤-proof (isBounded as)
   = vs Vec.++ Vec.replicate k a
 
 padLeft : A → Vec≤ A n → Vec A n
 padLeft a record { length = m ; vec = vs ; bound = m≤n }
-  with ≤″-offset k ← recompute (_ ℕ.≤″? _) (ℕ.≤⇒≤″ m≤n)
+  with ℕ.≤-offset k ← ℕ.≤-proof (recompute (_ ℕ.≤? _) m≤n)
   rewrite ℕ.+-comm m k
   = Vec.replicate k a Vec.++ vs
 
@@ -72,7 +79,7 @@ private
 
 padBoth : A → A → Vec≤ A n → Vec A n
 padBoth aₗ aᵣ record { length = m ; vec = vs ; bound = m≤n }
-  with ≤″-offset k ← recompute (_ ℕ.≤″? _) (ℕ.≤⇒≤″ m≤n)
+  with ℕ.≤-offset k ← ℕ.≤-proof (recompute (_ ℕ.≤? _) m≤n)
   rewrite split m k
   = Vec.replicate ⌊ k /2⌋ aₗ
       Vec.++ vs
@@ -83,7 +90,7 @@ fromList : (as : List A) → Vec≤ A (List.length as)
 fromList = fromVec ∘ Vec.fromList
 
 toList : Vec≤ A n → List A
-toList = Vec.toList ∘ Vec≤.vec
+toList = Vec.toList ∘ toVec
 
 ------------------------------------------------------------------------
 -- Creating new Vec≤ vectors