improve implementation of splitAt, take and drop.

src/Data/Vec/Base.agda

@@ -12,11 +12,11 @@ open import Data.Bool.Base using (Bool; true; false; if_then_else_)
 open import Data.Nat.Base
 open import Data.Fin.Base using (Fin; zero; suc)
 open import Data.List.Base as List using (List)
-open import Data.Product.Base as Prod using (∃; ∃₂; _×_; _,_)
+open import Data.Product.Base as Prod using (∃; ∃₂; _×_; _,_; proj₁; proj₂)
 open import Data.These.Base as These using (These; this; that; these)
 open import Function.Base using (const; _∘′_; id; _∘_)
 open import Level using (Level)
-open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; cong)
+open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; trans; cong)
 open import Relation.Nullary.Decidable.Core using (does)
 open import Relation.Unary using (Pred; Decidable)
 
@@ -262,25 +262,22 @@ allFin _ = tabulate id
 splitAt : ∀ m {n} (xs : Vec A (m + n)) →
           ∃₂ λ (ys : Vec A m) (zs : Vec A n) → xs ≡ ys ++ zs
 splitAt zero    xs                = ([] , xs , refl)
-splitAt (suc m) (x ∷ xs)          with splitAt m xs
-splitAt (suc m) (x ∷ .(ys ++ zs)) | (ys , zs , refl) =
-  ((x ∷ ys) , zs , refl)
+splitAt (suc m) (x ∷ xs) =
+  let (ys , zs , eq) = splitAt m xs in ((x ∷ ys) , zs , cong (x ∷_) eq)
 
 take : ∀ m {n} → Vec A (m + n) → Vec A m
-take m xs          with splitAt m xs
-take m .(ys ++ zs) | (ys , zs , refl) = ys
+take m xs = proj₁ (splitAt m xs)
 
 drop : ∀ m {n} → Vec A (m + n) → Vec A n
-drop m xs          with splitAt m xs
-drop m .(ys ++ zs) | (ys , zs , refl) = zs
+drop m xs = proj₁ (proj₂ (splitAt m xs))
 
 group : ∀ n k (xs : Vec A (n * k)) →
         ∃ λ (xss : Vec (Vec A k) n) → xs ≡ concat xss
 group zero    k []                  = ([] , refl)
-group (suc n) k xs                  with splitAt k xs
-group (suc n) k .(ys ++ zs)         | (ys , zs , refl) with group n k zs
-group (suc n) k .(ys ++ concat zss) | (ys , ._ , refl) | (zss , refl) =
-  ((ys ∷ zss) , refl)
+group (suc n) k xs  = 
+  let ys , zs , eq-split = splitAt k xs in
+  let zss , eq-group     = group n k zs in
+   (ys ∷ zss) , trans eq-split (cong (ys ++_) eq-group)
 
 split : Vec A n → Vec A ⌈ n /2⌉ × Vec A ⌊ n /2⌋
 split []           = ([]     , [])
@@ -341,16 +338,15 @@ xs ʳ++ ys = foldl (Vec _ ∘ (_+ _)) (λ rev x → x ∷ rev) ys xs
 
 initLast : ∀ (xs : Vec A (1 + n)) → ∃₂ λ ys y → xs ≡ ys ∷ʳ y
 initLast {n = zero}  (x ∷ []) = ([] , x , refl)
-initLast {n = suc n} (x ∷ xs) with initLast xs
-... | (ys , y , refl) = (x ∷ ys , y , refl)
+initLast {n = suc n} (x ∷ xs) =
+  let ys , y , eq = initLast xs in
+  (x ∷ ys , y , cong (x ∷_) eq)
 
 init : Vec A (1 + n) → Vec A n
-init xs with initLast xs
-... | (ys , y , refl) = ys
+init xs = proj₁ (initLast xs)
 
 last : Vec A (1 + n) → A
-last xs with initLast xs
-... | (ys , y , refl) = y
+last xs = proj₁ (proj₂ (initLast xs))
 
 ------------------------------------------------------------------------
 -- Other operations

src/Data/Vec/Properties.agda

@@ -71,86 +71,43 @@ private
 -- take
 
 unfold-take : ∀ n x (xs : Vec A (n + m)) → take (suc n) (x ∷ xs) ≡ x ∷ take n xs
-unfold-take n x xs with splitAt n xs
-... | xs , ys , refl = refl
+unfold-take n x xs = refl
 
 take-distr-zipWith : ∀ (f : A → B → C) →
                      (xs : Vec A (m + n)) (ys : Vec B (m + n)) →
                      take m (zipWith f xs ys) ≡ zipWith f (take m xs) (take m ys)
 take-distr-zipWith {m = zero}  f xs       ys       = refl
-take-distr-zipWith {m = suc m} f (x ∷ xs) (y ∷ ys) = begin
-    take (suc m) (zipWith f (x ∷ xs) (y ∷ ys))
-  ≡⟨⟩
-    take (suc m) (f x y ∷ (zipWith f xs ys))
-  ≡⟨ unfold-take m (f x y) (zipWith f xs ys) ⟩
-    f x y ∷ take m (zipWith f xs ys)
-  ≡⟨ cong (f x y ∷_) (take-distr-zipWith f xs ys) ⟩
-    f x y ∷ (zipWith f (take m xs) (take m ys))
-  ≡⟨⟩
-    zipWith f (x ∷ (take m xs)) (y ∷ (take m ys))
-  ≡˘⟨ cong₂ (zipWith f) (unfold-take m x xs) (unfold-take m y ys) ⟩
-    zipWith f (take (suc m) (x ∷ xs)) (take (suc m) (y ∷ ys))
-  ∎
+take-distr-zipWith {m = suc m} f (x ∷ xs) (y ∷ ys) = cong (f x y ∷_) (take-distr-zipWith f xs ys)
 
 take-distr-map : ∀ (f : A → B) (m : ℕ) (xs : Vec A (m + n)) →
                  take m (map f xs) ≡ map f (take m xs)
 take-distr-map f zero xs = refl
-take-distr-map f (suc m) (x ∷ xs) = begin
-  take (suc m) (map f (x ∷ xs)) ≡⟨⟩
-  take (suc m) (f x ∷ map f xs) ≡⟨ unfold-take m (f x) (map f xs) ⟩
-  f x ∷ (take m (map f xs))     ≡⟨ cong (f x ∷_) (take-distr-map f m xs) ⟩
-  f x ∷ (map f (take m xs))     ≡⟨⟩
-  map f (x ∷ take m xs)         ≡˘⟨ cong (map f) (unfold-take m x xs) ⟩
-  map f (take (suc m) (x ∷ xs)) ∎
+take-distr-map f (suc m) (x ∷ xs) = cong (f x ∷_) (take-distr-map f m xs)
 
 ------------------------------------------------------------------------
 -- drop
 
 unfold-drop : ∀ n x (xs : Vec A (n + m)) →
               drop (suc n) (x ∷ xs) ≡ drop n xs
-unfold-drop n x xs with splitAt n xs
-... | xs , ys , refl = refl
+unfold-drop n x xs = refl
 
 drop-distr-zipWith : (f : A → B → C) →
                      (x : Vec A (m + n)) (y : Vec B (m + n)) →
                      drop m (zipWith f x y) ≡ zipWith f (drop m x) (drop m y)
 drop-distr-zipWith {m = zero} f   xs       ys = refl
-drop-distr-zipWith {m = suc m} f (x ∷ xs) (y ∷ ys) = begin
-    drop (suc m) (zipWith f (x ∷ xs) (y ∷ ys))
-  ≡⟨⟩
-    drop (suc m) (f x y ∷ (zipWith f xs ys))
-  ≡⟨ unfold-drop m (f x y) (zipWith f xs ys) ⟩
-    drop m (zipWith f xs ys)
-  ≡⟨ drop-distr-zipWith f xs ys ⟩
-    zipWith f (drop m xs) (drop m ys)
-  ≡˘⟨ cong₂ (zipWith f) (unfold-drop m x xs) (unfold-drop m y ys) ⟩
-    zipWith f (drop (suc m) (x ∷ xs)) (drop (suc m) (y ∷ ys))
-  ∎
+drop-distr-zipWith {m = suc m} f (x ∷ xs) (y ∷ ys) = drop-distr-zipWith f xs ys
 
 drop-distr-map : ∀ (f : A → B) (m : ℕ) (x : Vec A (m + n)) →
                  drop m (map f x) ≡ map f (drop m x)
 drop-distr-map f zero x = refl
-drop-distr-map f (suc m) (x ∷ xs) = begin
-  drop (suc m) (map f (x ∷ xs)) ≡⟨⟩
-  drop (suc m) (f x ∷ map f xs) ≡⟨  unfold-drop m (f x) (map f xs) ⟩
-  drop m (map f xs)             ≡⟨  drop-distr-map f m xs ⟩
-  map f (drop m xs)             ≡˘⟨ cong (map f) (unfold-drop m x xs) ⟩
-  map f (drop (suc m) (x ∷ xs)) ∎
+drop-distr-map f (suc m) (x ∷ xs) = drop-distr-map f m xs
 
 ------------------------------------------------------------------------
 -- take and drop together
 
 take-drop-id : ∀ (m : ℕ) (x : Vec A (m + n)) → take m x ++ drop m x ≡ x
 take-drop-id zero x = refl
-take-drop-id (suc m) (x ∷ xs) = begin
-    take (suc m) (x ∷ xs) ++ drop (suc m) (x ∷ xs)
-  ≡⟨ cong₂ _++_ (unfold-take m x xs) (unfold-drop m x xs) ⟩
-    (x ∷ take m xs) ++ (drop m xs)
-  ≡⟨⟩
-    x ∷ (take m xs ++ drop m xs)
-  ≡⟨ cong (x ∷_) (take-drop-id m xs) ⟩
-    x ∷ xs
-  ∎
+take-drop-id (suc m) (x ∷ xs) = cong (x ∷_) (take-drop-id m xs)
 
 ------------------------------------------------------------------------
 -- truncate
@@ -215,12 +172,8 @@ lookup⇒[]= (suc i) (_ ∷ xs) p    = there (lookup⇒[]= i xs p)
 
 lookup-inject≤-take : ∀ m (m≤m+n : m ≤ m + n) (i : Fin m) (xs : Vec A (m + n)) →
                       lookup xs (Fin.inject≤ i m≤m+n) ≡ lookup (take m xs) i
-lookup-inject≤-take (suc m) m≤m+n zero (x ∷ xs)
-  rewrite unfold-take m x xs = refl
-lookup-inject≤-take (suc (suc m)) (s≤s m≤m+n) (suc zero) (x ∷ y ∷ xs)
-  rewrite unfold-take (suc m) x (y ∷ xs) | unfold-take m y xs = refl
-lookup-inject≤-take (suc (suc m)) (s≤s (s≤s m≤m+n)) (suc (suc i)) (x ∷ y ∷ xs)
-  rewrite unfold-take (suc m) x (y ∷ xs) | unfold-take m y xs = lookup-inject≤-take m m≤m+n i xs
+lookup-inject≤-take (suc m) m≤m+n zero (x ∷ xs) = refl
+lookup-inject≤-take (suc m) (s≤s m≤m+n) (suc i) (x ∷ xs) = lookup-inject≤-take m m≤m+n i xs
 
 ------------------------------------------------------------------------
 -- updateAt (_[_]%=_)

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

@@ -148,13 +148,11 @@ module _ {P : A → Set p} where
 
 drop⁺ : ∀ m {xs} → All P {m + n} xs → All P {n} (drop m xs)
 drop⁺ zero pxs = pxs
-drop⁺ (suc m) {x ∷ xs} (px ∷ pxs)
-  rewrite Vecₚ.unfold-drop m x xs = drop⁺ m pxs
+drop⁺ (suc m) {x ∷ xs} (px ∷ pxs) = drop⁺ m pxs
 
 take⁺ : ∀ m {xs} → All P {m + n} xs → All P {m} (take m xs)
 take⁺ zero pxs = []
-take⁺ (suc m) {x ∷ xs} (px ∷ pxs)
-  rewrite Vecₚ.unfold-take m x xs = px ∷ take⁺ m pxs
+take⁺ (suc m) {x ∷ xs} (px ∷ pxs) = px ∷ take⁺ m pxs
 
 ------------------------------------------------------------------------
 -- toList

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

@@ -70,13 +70,11 @@ module _ {R : Rel A ℓ} where
 
   take⁺ : ∀ {n} m {xs} → AllPairs R {m + n} xs → AllPairs R {m} (take m xs)
   take⁺ zero pxs = []
-  take⁺ (suc m) {x ∷ xs} (px ∷ pxs)
-    rewrite Vecₚ.unfold-take m x xs = Allₚ.take⁺ m px ∷ take⁺ m pxs
+  take⁺ (suc m) {x ∷ xs} (px ∷ pxs) = Allₚ.take⁺ m px ∷ take⁺ m pxs
 
   drop⁺ : ∀ {n} m {xs} → AllPairs R {m + n} xs → AllPairs R {n} (drop m xs)
   drop⁺ zero pxs = pxs
-  drop⁺ (suc m) {x ∷ xs} (_ ∷ pxs)
-    rewrite Vecₚ.unfold-drop m x xs = drop⁺ m pxs
+  drop⁺ (suc m) (_ ∷ pxs) = drop⁺ m pxs
 
 ------------------------------------------------------------------------
 -- tabulate