@@ -595,51 +595,58 @@ vectAppendAssociative [] y z = Refl
595vectAppendAssociative (x :: xs) ys zs =
595vectAppendAssociative (x :: xs) ys zs =
596 vectConsCong _ _ _ (vectAppendAssociative xs ys zs)
596 vectConsCong _ _ _ (vectAppendAssociative xs ys zs)
598−splitAtTakeDrop : (n : Nat) -> (xs : Vect (n + m) a) -> splitAt n xs = (take n xs, drop n xs)
598+||| Adding a prefix and then taking the prefix gets the prefix. Or,
599−splitAtTakeDrop Z xs = Refl
599+||| adding a suffix and then dropping the suffix does nothing.
600−splitAtTakeDrop (S k) (x :: xs) with (splitAt k xs) proof p
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
608takePrefix : (ns : Vect n a) -> (ms : Vect m a) -> take n (ns ++ ms) = ns
600takePrefix : (ns : Vect n a) -> (ms : Vect m a) -> take n (ns ++ ms) = ns
609takePrefix [] _ = Refl
601takePrefix [] _ = Refl
610takePrefix (n :: ns) ms = cong $ takePrefix ns ms
602takePrefix (n :: ns) ms = cong $ takePrefix ns ms
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)
604+||| Adding a prefix and then dropping the prefix does nothing. Or,
613−takeTake Z m xs = Refl
605+||| adding a suffix and then taking the suffix gets the suffix.
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
620dropPrefix : (ns : Vect n a) -> (ms : Vect m a) -> drop n (ns ++ ms) = ms
606dropPrefix : (ns : Vect n a) -> (ms : Vect m a) -> drop n (ns ++ ms) = ms
621dropPrefix [] ms = Refl
607dropPrefix [] ms = Refl
622dropPrefix (_ :: ns) ms = dropPrefix ns ms
608dropPrefix (_ :: ns) ms = dropPrefix ns ms
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
610+||| `take n . take (n + m) = take n`
625−dropDrop n Z xs = Refl
611+takeTake : (n : Nat) -> (m : Nat) ->
626−dropDrop {l} n (S k) (x :: xs) = rewrite aux (plusAssociative k n l) x xs in dropDrop n k xs
612+ (xs : Vect ((n + m) + l) a) -> (ys : Vect (n + (m + l)) a) ->
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))
618+||| `drop (n + m) = drop m . drop n`
627− where aux : {n : Nat} -> {m : Nat} -> (prf : n = m) ->
619+dropDrop : (n : Nat) -> (m : Nat) ->
628− (x : a) -> (xs : Vect m a) ->
620+ (xs : Vect ((n + m) + l) a) -> (ys : Vect (n + (m + l)) 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
621+ xs ~=~ ys ->
630− aux Refl x xs = Refl
622+ drop (n + m) xs = drop m (drop n ys)
631−
623+dropDrop Z m xs xs Refl = Refl
624+dropDrop (S n) m (_ :: xs) (_ :: ys) prf = dropDrop n m xs ys (vectInjective2 prf)
626+||| A `Vect` may be restored from its components.
632takeDropConcat : (n : Nat) -> (xs : Vect (n + m) a) -> take n xs ++ drop n xs = xs
627takeDropConcat : (n : Nat) -> (xs : Vect (n + m) a) -> take n xs ++ drop n xs = xs
633takeDropConcat Z xs = Refl
628takeDropConcat Z xs = Refl
634−takeDropConcat (S k) (x :: xs) = cong $ takeDropConcat k xs
629+takeDropConcat (S n) (x :: xs) = cong $ takeDropConcat n xs
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)
631+||| `drop n . take (n + m) = take m . drop n`.
637−takeDropDropTake n Z xs = Refl
632+|||
638−takeDropDropTake {l} n (S k) (x :: xs) = rewrite aux (plusAssociative k n l) x xs in takeDropDropTake n k xs
633+||| Or: there are two ways to extract a subsequence.
639− where aux : {n : Nat} -> {m : Nat} -> (prf : n = m) ->
634+dropTakeTakeDrop : (n : Nat) -> (m : Nat) ->
640− (x : a) -> (xs : Vect m a) ->
635+ (xs : Vect ((n + m) + l) a) -> (ys : Vect (n + (m + l)) 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
636+ xs ~=~ ys ->
642− aux Refl x xs = Refl
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)
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
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
644zipWithIsLiftA2 : (f : a -> b -> c) -> (as : Vect n a) -> (bs : Vect n b) -> zipWith f as bs = [| f as bs |]
651zipWithIsLiftA2 : (f : a -> b -> c) -> (as : Vect n a) -> (bs : Vect n b) -> zipWith f as bs = [| f as bs |]
645zipWithIsLiftA2 _ [] [] = Refl
652zipWithIsLiftA2 _ [] [] = Refl