@@ -595,51 +595,58 @@ vectAppendAssociative [] y z = Refl
595595vectAppendAssociative (x :: xs) ys zs =
596596 vectConsCong _ _ _ (vectAppendAssociative xs ys zs)
597597
598−splitAtTakeDrop : (n : Nat) -> (xs : Vect (n + m) a) -> splitAt n xs = (take n xs, drop n xs)
599−splitAtTakeDrop Z xs = Refl
600−splitAtTakeDrop (S k) (x :: xs) with (splitAt k xs) proof p
601− | (tk, dr) =
602− let rec = sym $ trans p $ splitAtTakeDrop k xs
603− tkp = cong {f=fst} rec
604− drp = cong {f=snd} rec
605− in replace {P = \tk' => (x :: tk', dr) = (x :: take k xs, drop k xs)} tkp $
606− replace {P = \dr' => (x :: take k xs, dr') = (x :: take k xs, drop k xs) } drp Refl
607−
598+||| Adding a prefix and then taking the prefix gets the prefix. Or,
599+||| adding a suffix and then dropping the suffix does nothing.
608600takePrefix : (ns : Vect n a) -> (ms : Vect m a) -> take n (ns ++ ms) = ns
609601takePrefix [] _ = Refl
610602takePrefix (n :: ns) ms = cong $ takePrefix ns ms
611603
612−takeTake : (n : Nat) -> (m : Nat) -> (xs : Vect (n + m + l) a) -> take n (take (n + m) xs) = take n {m = m + l} (rewrite plusAssociative n m l in xs)
613−takeTake Z m xs = Refl
614−takeTake {l} (S k) m (x :: xs) = rewrite aux (plusAssociative k m l) x xs in cong { f = (x ::) } $ takeTake k m xs
615− where aux : {n : Nat} -> {m : Nat} -> (prf : n = m) ->
616− (x : a) -> (xs : Vect m a) ->
617− rewrite__impl (\rep => Vect rep a) (rewrite__impl (\rep => S rep = S m) prf Refl) (x :: xs) = x :: rewrite__impl (\rep => Vect rep a) prf xs
618− aux Refl x xs = Refl
619−
604+||| Adding a prefix and then dropping the prefix does nothing. Or,
605+||| adding a suffix and then taking the suffix gets the suffix.
620606dropPrefix : (ns : Vect n a) -> (ms : Vect m a) -> drop n (ns ++ ms) = ms
621607dropPrefix [] ms = Refl
622608dropPrefix (_ :: ns) ms = dropPrefix ns ms
623609
624−dropDrop : (n : Nat) -> (m : Nat) -> (xs : Vect (m + n + l) a) -> drop n (drop m {m = n + l} (rewrite plusAssociative m n l in xs)) = drop (m + n) xs
625−dropDrop n Z xs = Refl
626−dropDrop {l} n (S k) (x :: xs) = rewrite aux (plusAssociative k n l) x xs in dropDrop n k xs
627− where aux : {n : Nat} -> {m : Nat} -> (prf : n = m) ->
628− (x : a) -> (xs : Vect m a) ->
629− rewrite__impl (\rep => Vect rep a) (rewrite__impl (\rep => S rep = S m) prf Refl) (x :: xs) = x :: rewrite__impl (\rep => Vect rep a) prf xs
630− aux Refl x xs = Refl
631−
610+||| `take n . take (n + m) = take n`
611+takeTake : (n : Nat) -> (m : Nat) ->
612+ (xs : Vect ((n + m) + l) a) -> (ys : Vect (n + (m + l)) a) ->
613+ xs ~=~ ys ->
614+ take n (take (n + m) xs) = take n ys
615+takeTake Z m _ _ _ = Refl
616+takeTake (S n) m (x :: xs) (y :: ys) prf = rewrite vectInjective1 prf in cong (takeTake n m xs ys (vectInjective2 prf))
617+
618+||| `drop (n + m) = drop m . drop n`
619+dropDrop : (n : Nat) -> (m : Nat) ->
620+ (xs : Vect ((n + m) + l) a) -> (ys : Vect (n + (m + l)) a) ->
621+ xs ~=~ ys ->
622+ drop (n + m) xs = drop m (drop n ys)
623+dropDrop Z m xs xs Refl = Refl
624+dropDrop (S n) m (_ :: xs) (_ :: ys) prf = dropDrop n m xs ys (vectInjective2 prf)
625+
626+||| A `Vect` may be restored from its components.
632627takeDropConcat : (n : Nat) -> (xs : Vect (n + m) a) -> take n xs ++ drop n xs = xs
633628takeDropConcat Z xs = Refl
634−takeDropConcat (S k) (x :: xs) = cong $ takeDropConcat k xs
635−
636−takeDropDropTake : (n : Nat) -> (m : Nat) -> (xs : Vect (m + n + l) a) -> take n (drop m {m = n + l} (rewrite plusAssociative m n l in xs)) = drop m (take (m + n) xs)
637−takeDropDropTake n Z xs = Refl
638−takeDropDropTake {l} n (S k) (x :: xs) = rewrite aux (plusAssociative k n l) x xs in takeDropDropTake n k xs
639− where aux : {n : Nat} -> {m : Nat} -> (prf : n = m) ->
640− (x : a) -> (xs : Vect m a) ->
641− rewrite__impl (\rep => Vect rep a) (rewrite__impl (\rep => S rep = S m) prf Refl) (x :: xs) = x :: rewrite__impl (\rep => Vect rep a) prf xs
642− aux Refl x xs = Refl
629+takeDropConcat (S n) (x :: xs) = cong $ takeDropConcat n xs
630+
631+||| `drop n . take (n + m) = take m . drop n`.
632+|||
633+||| Or: there are two ways to extract a subsequence.
634+dropTakeTakeDrop : (n : Nat) -> (m : Nat) ->
635+ (xs : Vect ((n + m) + l) a) -> (ys : Vect (n + (m + l)) a) ->
636+ xs ~=~ ys ->
637+ drop n (take (n + m) xs) = take m (drop n ys)
638+dropTakeTakeDrop Z m xs xs Refl = Refl
639+dropTakeTakeDrop (S n) m (_ :: xs) (_ :: ys) prf = dropTakeTakeDrop n m xs ys (vectInjective2 prf)
640+
641+splitAtTakeDrop : (n : Nat) -> (xs : Vect (n + m) a) -> splitAt n xs = (take n xs, drop n xs)
642+splitAtTakeDrop Z xs = Refl
643+splitAtTakeDrop (S k) (x :: xs) with (splitAt k xs) proof p
644+ | (tk, dr) =
645+ let rec = sym $ trans p $ splitAtTakeDrop k xs
646+ tkp = cong {f=fst} rec
647+ drp = cong {f=snd} rec
648+ in replace {P = \tk' => (x :: tk', dr) = (x :: take k xs, drop k xs)} tkp $
649+ replace {P = \dr' => (x :: take k xs, dr') = (x :: take k xs, drop k xs) } drp Refl
643650
644651zipWithIsLiftA2 : (f : a -> b -> c) -> (as : Vect n a) -> (bs : Vect n b) -> zipWith f as bs = [| f as bs |]
645652zipWithIsLiftA2 _ [] [] = Refl