From bde655f8aa742ea82aa2c33e732353509d7dd397 Mon Sep 17 00:00:00 2001
From: jamesmckinna <31931406+jamesmckinna@users.noreply.github.com>
Date: Sat, 20 Jan 2024 13:31:40 +0000
Subject: [PATCH] Remove all external use of `less-than-or-equal` beyond
 `Data.Nat.*` (#2256)

* removed all external use of `less-than-or-equal` beyond `Data.Nat.*`

* use of `variable`s
---
 src/Data/Vec/Bounded/Base.agda | 97 +++++++++++++++++-----------------
 1 file changed, 48 insertions(+), 49 deletions(-)

diff --git a/src/Data/Vec/Bounded/Base.agda b/src/Data/Vec/Bounded/Base.agda
index c926c9dfb1..7476afb2d4 100644
--- a/src/Data/Vec/Bounded/Base.agda
+++ b/src/Data/Vec/Bounded/Base.agda
@@ -9,11 +9,11 @@
 module Data.Vec.Bounded.Base where
 
 open import Data.Nat.Base
-import Data.Nat.Properties as ℕₚ
+import Data.Nat.Properties as ℕ
 open import Data.List.Base as List using (List)
-open import Data.List.Extrema ℕₚ.≤-totalOrder
+open import Data.List.Extrema ℕ.≤-totalOrder
 open import Data.List.Relation.Unary.All as All using (All)
-import Data.List.Relation.Unary.All.Properties as Allₚ
+import Data.List.Relation.Unary.All.Properties as All
 open import Data.List.Membership.Propositional using (mapWith∈)
 open import Data.Product.Base using (∃; _×_; _,_; proj₁; proj₂)
 open import Data.Vec.Base as Vec using (Vec)
@@ -21,7 +21,7 @@ open import Data.These.Base as These using (These)
 open import Function.Base using (_∘_; id; _$_)
 open import Level using (Level)
 open import Relation.Nullary.Decidable.Core using (recompute)
-open import Relation.Binary.PropositionalEquality.Core as P using (_≡_; refl)
+open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_)
 open import Relation.Binary.PropositionalEquality.Properties
   using (module ≡-Reasoning)
 
@@ -31,6 +31,7 @@ private
     A : Set a
     B : Set b
     C : Set c
+    m n : ℕ
 
 ------------------------------------------------------------------------
 -- Types
@@ -45,37 +46,35 @@ record Vec≤ (A : Set a) (n : ℕ) : Set a where
 ------------------------------------------------------------------------
 -- Conversion functions
 
-fromVec : ∀ {n} → Vec A n → Vec≤ A n
-fromVec v = v , ℕₚ.≤-refl
+fromVec : Vec A n → Vec≤ A n
+fromVec v = v , ℕ.≤-refl
 
-padRight : ∀ {n} → A → Vec≤ A n → Vec A n
+padRight : A → Vec≤ A n → Vec A n
 padRight a (vs , m≤n)
-  with recompute (_ ℕₚ.≤″? _) (ℕₚ.≤⇒≤″ m≤n)
-... | less-than-or-equal refl = vs Vec.++ Vec.replicate  _ a
+  with ≤″-offset k ← recompute (_ ℕ.≤″? _) (ℕ.≤⇒≤″ m≤n)
+  = vs Vec.++ Vec.replicate k a
 
-padLeft : ∀ {n} → A → Vec≤ A n → Vec A n
-padLeft a as@(vs , m≤n)
-  with recompute (_ ℕₚ.≤″? _) (ℕₚ.≤⇒≤″ m≤n)
-... | less-than-or-equal {k} ∣as∣+k≡n
-  with P.trans (ℕₚ.+-comm k (Vec≤.length as)) ∣as∣+k≡n
-...   | refl = Vec.replicate k a Vec.++ vs
+padLeft : A → Vec≤ A n → Vec A n
+padLeft a record { length = m ; vec = vs ; bound = m≤n }
+  with ≤″-offset k ← recompute (_ ℕ.≤″? _) (ℕ.≤⇒≤″ m≤n)
+  rewrite ℕ.+-comm m k
+  = Vec.replicate k a Vec.++ vs
 
 private
-  split : ∀ {m n} k → m + k ≡ n → ⌊ k /2⌋ + (m + ⌈ k /2⌉) ≡ n
-  split {m} {n} k eq = begin
-    ⌊ k /2⌋ + (m + ⌈ k /2⌉) ≡⟨ ℕₚ.+-comm ⌊ k /2⌋ _ ⟩
-    m + ⌈ k /2⌉ + ⌊ k /2⌋   ≡⟨ ℕₚ.+-assoc m ⌈ k /2⌉ ⌊ k /2⌋ ⟩
-    m + (⌈ k /2⌉ + ⌊ k /2⌋) ≡⟨ P.cong (m +_) (ℕₚ.+-comm ⌈ k /2⌉ ⌊ k /2⌋) ⟩
-    m + (⌊ k /2⌋ + ⌈ k /2⌉) ≡⟨ P.cong (m +_) (ℕₚ.⌊n/2⌋+⌈n/2⌉≡n k) ⟩
-    m + k                   ≡⟨ eq ⟩
-    n                       ∎ where open ≡-Reasoning
-
-padBoth : ∀ {n} → A → A → Vec≤ A n → Vec A n
-padBoth aₗ aᵣ as@(vs , m≤n)
-  with recompute (_ ℕₚ.≤″? _) (ℕₚ.≤⇒≤″ m≤n)
-... | less-than-or-equal {k} ∣as∣+k≡n
-    with split k ∣as∣+k≡n
-... | refl = Vec.replicate ⌊ k /2⌋ aₗ
+  split : ∀ m k → m + k ≡ ⌊ k /2⌋ + (m + ⌈ k /2⌉)
+  split m k = begin
+    m + k                   ≡⟨ ≡.cong (m +_) (ℕ.⌊n/2⌋+⌈n/2⌉≡n k) ⟨
+    m + (⌊ k /2⌋ + ⌈ k /2⌉) ≡⟨ ≡.cong (m +_) (ℕ.+-comm ⌊ k /2⌋ ⌈ k /2⌉) ⟩
+    m + (⌈ k /2⌉ + ⌊ k /2⌋) ≡⟨ ℕ.+-assoc m ⌈ k /2⌉ ⌊ k /2⌋ ⟨
+    m + ⌈ k /2⌉ + ⌊ k /2⌋   ≡⟨ ℕ.+-comm _ ⌊ k /2⌋ ⟩
+    ⌊ k /2⌋ + (m + ⌈ k /2⌉) ∎
+    where open ≡-Reasoning
+
+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)
+  rewrite split m k
+  = Vec.replicate ⌊ k /2⌋ aₗ
       Vec.++ vs
       Vec.++ Vec.replicate ⌈ k /2⌉ aᵣ
 
@@ -83,59 +82,59 @@ padBoth aₗ aᵣ as@(vs , m≤n)
 fromList : (as : List A) → Vec≤ A (List.length as)
 fromList = fromVec ∘ Vec.fromList
 
-toList : ∀ {n} → Vec≤ A n → List A
+toList : Vec≤ A n → List A
 toList = Vec.toList ∘ Vec≤.vec
 
 ------------------------------------------------------------------------
 -- Creating new Vec≤ vectors
 
-replicate : ∀ {m n} .(m≤n : m ≤ n) → A → Vec≤ A n
+replicate : .(m≤n : m ≤ n) → A → Vec≤ A n
 replicate m≤n a = Vec.replicate _ a , m≤n
 
-[] : ∀ {n} → Vec≤ A n
+[] : Vec≤ A n
 [] = Vec.[] , z≤n
 
 infixr 5 _∷_
-_∷_ : ∀ {n} → A → Vec≤ A n → Vec≤ A (suc n)
+_∷_ : A → Vec≤ A n → Vec≤ A (suc n)
 a ∷ (as , p) = a Vec.∷ as , s≤s p
 
 ------------------------------------------------------------------------
 -- Modifying Vec≤ vectors
 
-≤-cast : ∀ {m n} → .(m≤n : m ≤ n) → Vec≤ A m → Vec≤ A n
-≤-cast m≤n (v , p) = v , ℕₚ.≤-trans p m≤n
+≤-cast : .(m≤n : m ≤ n) → Vec≤ A m → Vec≤ A n
+≤-cast m≤n (v , p) = v , ℕ.≤-trans p m≤n
 
-≡-cast : ∀ {m n} → .(eq : m ≡ n) → Vec≤ A m → Vec≤ A n
-≡-cast m≡n = ≤-cast (ℕₚ.≤-reflexive m≡n)
+≡-cast : .(eq : m ≡ n) → Vec≤ A m → Vec≤ A n
+≡-cast m≡n = ≤-cast (ℕ.≤-reflexive m≡n)
 
-map : (A → B) → ∀ {n} → Vec≤ A n → Vec≤ B n
+map : (A → B) → Vec≤ A n → Vec≤ B n
 map f (v , p) = Vec.map f v , p
 
-reverse : ∀ {n} → Vec≤ A n → Vec≤ A n
+reverse : Vec≤ A n → Vec≤ A n
 reverse (v , p) = Vec.reverse v , p
 
 -- Align and Zip.
 
-alignWith : (These A B → C) → ∀ {n} → Vec≤ A n → Vec≤ B n → Vec≤ C n
-alignWith f (as , p) (bs , q) = Vec.alignWith f as bs , ℕₚ.⊔-lub p q
+alignWith : (These A B → C) → Vec≤ A n → Vec≤ B n → Vec≤ C n
+alignWith f (as , p) (bs , q) = Vec.alignWith f as bs , ℕ.⊔-lub p q
 
-zipWith : (A → B → C) → ∀ {n} → Vec≤ A n → Vec≤ B n → Vec≤ C n
-zipWith f (as , p) (bs , q) = Vec.restrictWith f as bs , ℕₚ.m≤n⇒m⊓o≤n _ p
+zipWith : (A → B → C) → Vec≤ A n → Vec≤ B n → Vec≤ C n
+zipWith f (as , p) (bs , q) = Vec.restrictWith f as bs , ℕ.m≤n⇒m⊓o≤n _ p
 
-zip : ∀ {n} → Vec≤ A n → Vec≤ B n → Vec≤ (A × B) n
+zip : Vec≤ A n → Vec≤ B n → Vec≤ (A × B) n
 zip = zipWith _,_
 
-align : ∀ {n} → Vec≤ A n → Vec≤ B n → Vec≤ (These A B) n
+align : Vec≤ A n → Vec≤ B n → Vec≤ (These A B) n
 align = alignWith id
 
 -- take and drop
 
-take : ∀ {m} n → Vec≤ A m → Vec≤ A (n ⊓ m)
+take : ∀ n → Vec≤ A m → Vec≤ A (n ⊓ m)
 take             zero    _                = []
 take             (suc n) (Vec.[] , p)     = []
 take {m = suc m} (suc n) (a Vec.∷ as , p) = a ∷ take n (as , s≤s⁻¹ p)
 
-drop : ∀ {m} n → Vec≤ A m → Vec≤ A (m ∸ n)
+drop : ∀ n → Vec≤ A m → Vec≤ A (m ∸ n)
 drop             zero    v                = v
 drop             (suc n) (Vec.[] , p)     = []
 drop {m = suc m} (suc n) (a Vec.∷ as , p) = drop n (as , s≤s⁻¹ p)
@@ -150,7 +149,7 @@ rectangle {A = A} rows = width , padded where
   width = max 0 sizes
 
   all≤ : All (λ v → proj₁ v ≤ width) rows
-  all≤ = Allₚ.map⁻ (xs≤max 0 sizes)
+  all≤ = All.map⁻ (xs≤max 0 sizes)
 
   padded : List (Vec≤ A width)
   padded = mapWith∈ rows $ λ {x} x∈rows →