@@ -293,7 +293,6 @@ mapMaybe f (x::xs) =
293293 Just y => (S len ** y :: ys)
294294 Nothing => ( len ** ys)
295295
296−
297296--------------------------------------------------------------------------------
298297-- Folds
299298--------------------------------------------------------------------------------
@@ -321,6 +320,7 @@ foldr1 f (x::xs) = foldr f x xs
321320||| Foldl without seeding the accumulator
322321foldl1 : (t -> t -> t) -> Vect (S n) t -> t
323322foldl1 f (x::xs) = foldl f x xs
323+
324324--------------------------------------------------------------------------------
325325-- Scans
326326--------------------------------------------------------------------------------
@@ -455,13 +455,17 @@ delete = deleteBy (==)
455455-- Splitting and breaking lists
456456--------------------------------------------------------------------------------
457457
458−||| A tuple where the first element is a Vect of the n first elements and
459−||| the second element is a Vect of the remaining elements of the original Vect
460−||| It is equivalent to (take n xs, drop n xs)
458+||| A tuple where the first element is a `Vect` of the `n` first elements and
459+||| the second element is a `Vect` of the remaining elements of the original.
460+||| It is equivalent to `(take n xs, drop n xs)` (`splitAtTakeDrop`),
461+||| but is more efficient.
462+|||
461463||| @ n the index to split at
462−||| @ xs the Vect to split in two
464+||| @ xs the `Vect` to split in two
463465splitAt : (n : Nat) -> (xs : Vect (n + m) elem) -> (Vect n elem, Vect m elem)
464−splitAt n xs = (take n xs, drop n xs)
466+splitAt Z xs = ([], xs)
467+splitAt (S k) (x :: xs) with (splitAt k xs)
468+ | (tk, dr) = (x :: tk, dr)
465469
466470partition : (elem -> Bool) -> Vect len elem -> ((p ** Vect p elem), (q ** Vect q elem))
467471partition p [] = ((_ ** []), (_ ** []))
@@ -521,12 +525,14 @@ range : {len : Nat} -> Vect len (Fin len)
521525range {len=Z} = []
522526range {len=S _} = FZ :: map FS range
523527
524−||| Transpose a Vect of Vects, turning rows into columns and vice versa.
528+||| Transpose a `Vect` of `Vect`s, turning rows into columns and vice versa.
529+|||
530+||| This is like zipping all the inner `Vect`s together and is equivalent to `traverse id` (`transposeTraverse`).
525531|||
526532||| As the types ensure rectangularity, this is an involution, unlike `Prelude.List.transpose`.
527−transpose : {n : Nat} -> Vect m (Vect n elem) -> Vect n (Vect m elem)
528−transpose [] = replicate _ []
529−transpose (x :: xs) = zipWith (::) x (transpose xs)
533+transpose : Vect m (Vect n elem) -> Vect n (Vect m elem)
534+transpose [] = replicate _ [] -- = [| [] |]
535+transpose (x :: xs) = zipWith (::) x (transpose xs) -- = [| x :: xs |]
530536
531537--------------------------------------------------------------------------------
532538-- Applicative/Monad/Traversable
@@ -534,7 +540,6 @@ transpose (x :: xs) = zipWith (::) x (transpose xs)
534540
535541implementation Applicative (Vect k) where
536542 pure = replicate _
537−
538543 fs <*> vs = zipWith apply fs vs
539544
540545||| This monad is different from the List monad, (>>=)
@@ -543,8 +548,8 @@ implementation Monad (Vect len) where
543548 m >>= f = diag (map f m)
544549
545550implementation Traversable (Vect n) where
546− traverse f [] = pure Vect.Nil
547− traverse f (x::xs) = [| Vect.(::) (f x) (traverse f xs) |]
551+ traverse f [] = [| [] |]
552+ traverse f (x :: xs) = [| f x :: traverse f xs |]
548553
549554--------------------------------------------------------------------------------
550555-- Show
@@ -553,13 +558,29 @@ implementation Traversable (Vect n) where
553558implementation Show elem => Show (Vect len elem) where
554559 show = show . toList
555560
561+--------------------------------------------------------------------------------
562+-- Uninhabited
563+--------------------------------------------------------------------------------
564+
565+Uninhabited a => Uninhabited (Vect (S n) a) where
566+ uninhabited (x :: _) = uninhabited x
567+
556568--------------------------------------------------------------------------------
557569-- Properties
558570--------------------------------------------------------------------------------
559571
572+vectMustBeNil : (xs : Vect Z a) -> xs = []
573+vectMustBeNil [] = Refl
574+
560575vectConsCong : (x : elem) -> (xs : Vect len elem) -> (ys : Vect m elem) -> (xs = ys) -> (x :: xs = x :: ys)
561576vectConsCong x xs xs Refl = Refl
562577
578+vectInjective1 : {xs : Vect n a} -> {ys : Vect m b} -> x :: xs ~=~ y :: ys -> x ~=~ y
579+vectInjective1 Refl = Refl
580+
581+vectInjective2 : {xs : Vect n a} -> {ys : Vect m b} -> x :: xs ~=~ y :: ys -> xs ~=~ ys
582+vectInjective2 Refl = Refl
583+
563584vectNilRightNeutral : (xs : Vect n a) -> xs ++ [] = xs
564585vectNilRightNeutral [] = Refl
565586vectNilRightNeutral (x :: xs) =
@@ -573,16 +594,93 @@ vectAppendAssociative [] y z = Refl
573594vectAppendAssociative (x :: xs) ys zs =
574595 vectConsCong _ _ _ (vectAppendAssociative xs ys zs)
575596
597+||| Adding a prefix and then taking the prefix gets the prefix. Or,
598+||| adding a suffix and then dropping the suffix does nothing.
599+takePrefix : (ns : Vect n a) -> (ms : Vect m a) -> take n (ns ++ ms) = ns
600+takePrefix [] _ = Refl
601+takePrefix (n :: ns) ms = cong $ takePrefix ns ms
602+
603+||| Adding a prefix and then dropping the prefix does nothing. Or,
604+||| adding a suffix and then taking the suffix gets the suffix.
605+dropPrefix : (ns : Vect n a) -> (ms : Vect m a) -> drop n (ns ++ ms) = ms
606+dropPrefix [] ms = Refl
607+dropPrefix (_ :: ns) ms = dropPrefix ns ms
608+
609+||| `take n . take (n + m) = take n`
610+takeTake : (n : Nat) -> (m : Nat) ->
611+ (xs : Vect ((n + m) + l) a) -> (ys : Vect (n + (m + l)) a) ->
612+ xs ~=~ ys ->
613+ take n (take (n + m) xs) = take n ys
614+takeTake Z m _ _ _ = Refl
615+takeTake (S n) m (x :: xs) (y :: ys) prf = rewrite vectInjective1 prf in cong (takeTake n m xs ys (vectInjective2 prf))
616+
617+||| `drop (n + m) = drop m . drop n`
618+dropDrop : (n : Nat) -> (m : Nat) ->
619+ (xs : Vect ((n + m) + l) a) -> (ys : Vect (n + (m + l)) a) ->
620+ xs ~=~ ys ->
621+ drop (n + m) xs = drop m (drop n ys)
622+dropDrop Z m xs xs Refl = Refl
623+dropDrop (S n) m (_ :: xs) (_ :: ys) prf = dropDrop n m xs ys (vectInjective2 prf)
624+
625+||| A `Vect` may be restored from its components.
626+takeDropConcat : (n : Nat) -> (xs : Vect (n + m) a) -> take n xs ++ drop n xs = xs
627+takeDropConcat Z xs = Refl
628+takeDropConcat (S n) (x :: xs) = cong $ takeDropConcat n xs
629+
630+||| `drop n . take (n + m) = take m . drop n`.
631+|||
632+||| Or: there are two ways to extract a subsequence.
633+dropTakeTakeDrop : (n : Nat) -> (m : Nat) ->
634+ (xs : Vect ((n + m) + l) a) -> (ys : Vect (n + (m + l)) a) ->
635+ xs ~=~ ys ->
636+ drop n (take (n + m) xs) = take m (drop n ys)
637+dropTakeTakeDrop Z m xs xs Refl = Refl
638+dropTakeTakeDrop (S n) m (_ :: xs) (_ :: ys) prf = dropTakeTakeDrop n m xs ys (vectInjective2 prf)
639+
640+splitAtTakeDrop : (n : Nat) -> (xs : Vect (n + m) a) -> splitAt n xs = (take n xs, drop n xs)
641+splitAtTakeDrop Z xs = Refl
642+splitAtTakeDrop (S k) (x :: xs) with (splitAt k xs) proof p
643+ | (tk, dr) = let prf = trans p (splitAtTakeDrop k xs)
644+ in aux (cong {f=(x ::) . fst} prf) (cong {f=snd} prf)
645+ where aux : {a, b : Type} -> {w, x : a} -> {y, z : b} -> w = x -> y = z -> (w, y) = (x, z)
646+ aux Refl Refl = Refl
647+
648+zipWithIsLiftA2 : (f : a -> b -> c) -> (as : Vect n a) -> (bs : Vect n b) -> zipWith f as bs = [| f as bs |]
649+zipWithIsLiftA2 _ [] [] = Refl
650+zipWithIsLiftA2 f (a :: as) (b :: bs) = rewrite zipWithIsLiftA2 f as bs in Refl
651+zipWithIsLiftA3 : (f : a -> b -> c -> d) -> (as : Vect n a) -> (bs : Vect n b) -> (cs : Vect n c) -> zipWith3 f as bs cs = [| f as bs cs |]
652+zipWithIsLiftA3 _ [] [] [] = Refl
653+zipWithIsLiftA3 f (a :: as) (b :: bs) (c :: cs) = rewrite zipWithIsLiftA3 f as bs cs in Refl
654+
655+-- Note relationship to Applicative (Morphism (Fin n))
656+indexReplicate : (x : a) -> (n : Nat) -> (i : Fin n) -> index i (replicate n x) = x
657+indexReplicate x (S n) FZ = Refl
658+indexReplicate x (S n) (FS i) = indexReplicate x n i
659+indexZipWith : (f : a -> b -> c) -> (as : Vect n a) -> (bs : Vect n b) -> (i : Fin n) -> index i (zipWith f as bs) = f (index i as) (index i bs)
660+indexZipWith f (a :: _) (b :: _) FZ = Refl
661+indexZipWith f (_ :: as) (_ :: bs) (FS i) = indexZipWith f as bs i
662+indexTranspose : (x : Fin o) -> (y : Fin i) -> (xss : Vect o (Vect i a)) -> index y (index x xss) = index x (index y (transpose xss))
663+indexTranspose x y (xs :: xss) = rewrite prf in
664+ rewrite sym $ indexZipWith Vect.(::) xs (transpose xss) y in Refl
665+ where prf : index y (index x (xs :: xss)) = index x (index y xs :: index y (transpose xss))
666+ prf = case x of
667+ FZ => Refl
668+ FS k => indexTranspose k y xss
669+
670+transposeTraverse : (xss : Vect o (Vect i a)) -> transpose xss = traverse Basics.id xss
671+transposeTraverse [] = Refl
672+transposeTraverse (xs :: xss) = rewrite zipWithIsLiftA2 Vect.(::) xs (transpose xss) in cong (transposeTraverse xss)
673+
674+traverseIdCons : (xs : Vect o a) -> (xss : Vect o (Vect i a)) -> traverse Basics.id [| xs :: xss |] = xs :: traverse Basics.id xss
675+traverseIdCons [] [] = Refl
676+traverseIdCons (x :: xs) (ys :: xss) = rewrite traverseIdCons xs xss in Refl
677+transposeCons : (xs : Vect o a) -> (xss : Vect o (Vect i a)) -> transpose (zipWith (::) xs xss) = xs :: transpose xss
678+transposeCons xs xss = rewrite zipWithIsLiftA2 Vect.(::) xs xss in rewrite transposeTraverse (pure (::) <*> xs <*> xss) in rewrite transposeTraverse xss in traverseIdCons xs xss
679+
576680--------------------------------------------------------------------------------
577681-- DecEq
578682--------------------------------------------------------------------------------
579683
580−vectInjective1 : {xs, ys : Vect n a} -> {x, y : a} -> x :: xs = y :: ys -> x = y
581−vectInjective1 {x=x} {y=x} {xs=xs} {ys=xs} Refl = Refl
582−
583−vectInjective2 : {xs, ys : Vect n a} -> {x, y : a} -> x :: xs = y :: ys -> xs = ys
584−vectInjective2 {x=x} {y=x} {xs=xs} {ys=xs} Refl = Refl
585−
586684implementation DecEq a => DecEq (Vect n a) where
587685 decEq [] [] = Yes Refl
588686 decEq (x :: xs) (y :: ys) with (decEq x y)