@@ -104,36 +104,12 @@ take : (n : Nat) -> Vect (n + m) elem -> Vect n elem
104take Z xs = []
104take Z xs = []
105take (S k) (x :: xs) = x :: take k xs
105take (S k) (x :: xs) = x :: take k xs
107−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)
108−takeTake Z m xs = Refl
109−takeTake {l} (S k) m (x :: xs) = rewrite aux (plusAssociative k m l) x xs in cong { f = (x ::) } $ takeTake k m xs
110− where aux : {n : Nat} -> {m : Nat} -> (prf : n = m) ->
111− (x : a) -> (xs : Vect m a) ->
112− 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
113− aux Refl x xs = Refl
115||| Remove the first n elements of a Vect
107||| Remove the first n elements of a Vect
116||| @ n the number of elements to remove
108||| @ n the number of elements to remove
117drop : (n : Nat) -> Vect (n + m) elem -> Vect m elem
109drop : (n : Nat) -> Vect (n + m) elem -> Vect m elem
118drop Z xs = xs
110drop Z xs = xs
119drop (S k) (x :: xs) = drop k xs
111drop (S k) (x :: xs) = drop k xs
121−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
122−dropDrop n Z xs = Refl
123−dropDrop {l} n (S k) (x :: xs) = rewrite aux (plusAssociative k n l) x xs in dropDrop n k xs
124− where aux : {n : Nat} -> {m : Nat} -> (prf : n = m) ->
125− (x : a) -> (xs : Vect m a) ->
126− 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
127− aux Refl x xs = Refl
129−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)
130−takeDropDropTake n Z xs = Refl
131−takeDropDropTake {l} n (S k) (x :: xs) = rewrite aux (plusAssociative k n l) x xs in takeDropDropTake n k xs
132− where aux : {n : Nat} -> {m : Nat} -> (prf : n = m) ->
133− (x : a) -> (xs : Vect m a) ->
134− 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
135− aux Refl x xs = Refl
137||| Take the longest prefix of a Vect such that all elements satisfy some
113||| Take the longest prefix of a Vect such that all elements satisfy some
138||| Boolean predicate.
114||| Boolean predicate.
@@ -212,18 +188,6 @@ fromList l =
212(++) [] ys = ys
188(++) [] ys = ys
213(++) (x::xs) ys = x :: xs ++ ys
189(++) (x::xs) ys = x :: xs ++ ys
215−takePrefix : (ns : Vect n a) -> (ms : Vect m a) -> take n (ns ++ ms) = ns
216−takePrefix [] _ = Refl
217−takePrefix (n :: ns) ms = cong $ takePrefix ns ms
219−dropPrefix : (ns : Vect n a) -> (ms : Vect m a) -> drop n (ns ++ ms) = ms
220−dropPrefix [] ms = Refl
221−dropPrefix (_ :: ns) ms = dropPrefix ns ms
223−takeDropConcat : (n : Nat) -> (xs : Vect (n + m) a) -> take n xs ++ drop n xs = xs
224−takeDropConcat Z xs = Refl
225−takeDropConcat (S k) (x :: xs) = cong $ takeDropConcat k xs
227||| Repeate some value some number of times.
191||| Repeate some value some number of times.
229||| @ len the number of times to repeat it
193||| @ len the number of times to repeat it
@@ -329,7 +293,6 @@ mapMaybe f (x::xs) =
329 Just y => (S len ** y :: ys)
293 Just y => (S len ** y :: ys)
330 Nothing => ( len ** ys)
294 Nothing => ( len ** ys)
333--------------------------------------------------------------------------------
296--------------------------------------------------------------------------------
335--------------------------------------------------------------------------------
298--------------------------------------------------------------------------------
@@ -503,16 +466,6 @@ splitAt (S k) (x::xs) =
503 let (tk, dr) = splitAt k xs
466 let (tk, dr) = splitAt k xs
504 in (x::tk, dr)
467 in (x::tk, dr)
506−splitAtTakeDrop : (n : Nat) -> (xs : Vect (n + m) a) -> splitAt n xs = (take n xs, drop n xs)
507−splitAtTakeDrop Z xs = Refl
508−splitAtTakeDrop (S k) (x::xs) with (splitAt k xs) proof p
510− let rec = sym $ trans p $ splitAtTakeDrop k xs
511− tkp = cong {f=fst} rec
512− drp = cong {f=snd} rec
513− in replace {P = \tk' => (x::tk', dr) = (x::take k xs, drop k xs)} tkp $
514− replace {P = \dr' => (x::take k xs, dr') = (x::take k xs, drop k xs) } drp Refl
516partition : (elem -> Bool) -> Vect len elem -> ((p ** Vect p elem), (q ** Vect q elem))
469partition : (elem -> Bool) -> Vect len elem -> ((p ** Vect p elem), (q ** Vect q elem))
517partition p [] = ((_ ** []), (_ ** []))
470partition p [] = ((_ ** []), (_ ** []))
518partition p (x::xs) =
471partition p (x::xs) =
@@ -573,7 +526,7 @@ range {len=S _} = FZ :: map FS range
574||| Transpose a `Vect` of `Vect`s, turning rows into columns and vice versa.
527||| Transpose a `Vect` of `Vect`s, turning rows into columns and vice versa.
576−||| This is like zipping all the inner `Vect`s together and is equivalent to `traverse id`.
529+||| This is like zipping all the inner `Vect`s together and is equivalent to `traverse id` (`transposeTraverse`).
578||| As the types ensure rectangularity, this is an involution, unlike `Prelude.List.transpose`.
531||| As the types ensure rectangularity, this is an involution, unlike `Prelude.List.transpose`.
579transpose : Vect m (Vect n elem) -> Vect n (Vect m elem)
532transpose : Vect m (Vect n elem) -> Vect n (Vect m elem)
@@ -634,6 +587,84 @@ vectAppendAssociative [] y z = Refl
634vectAppendAssociative (x :: xs) ys zs =
587vectAppendAssociative (x :: xs) ys zs =
635 vectConsCong _ _ _ (vectAppendAssociative xs ys zs)
588 vectConsCong _ _ _ (vectAppendAssociative xs ys zs)
590+splitAtTakeDrop : (n : Nat) -> (xs : Vect (n + m) a) -> splitAt n xs = (take n xs, drop n xs)
591+splitAtTakeDrop Z xs = Refl
592+splitAtTakeDrop (S k) (x :: xs) with (splitAt k xs) proof p
594+ let rec = sym $ trans p $ splitAtTakeDrop k xs
595+ tkp = cong {f=fst} rec
596+ drp = cong {f=snd} rec
597+ in replace {P = \tk' => (x :: tk', dr) = (x :: take k xs, drop k xs)} tkp $
598+ replace {P = \dr' => (x :: take k xs, dr') = (x :: take k xs, drop k xs) } drp Refl
600+takePrefix : (ns : Vect n a) -> (ms : Vect m a) -> take n (ns ++ ms) = ns
601+takePrefix [] _ = Refl
602+takePrefix (n :: ns) ms = cong $ takePrefix ns ms
604+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)
605+takeTake Z m xs = Refl
606+takeTake {l} (S k) m (x :: xs) = rewrite aux (plusAssociative k m l) x xs in cong { f = (x ::) } $ takeTake k m xs
607+ where aux : {n : Nat} -> {m : Nat} -> (prf : n = m) ->
608+ (x : a) -> (xs : Vect m a) ->
609+ 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
610+ aux Refl x xs = Refl
612+dropPrefix : (ns : Vect n a) -> (ms : Vect m a) -> drop n (ns ++ ms) = ms
613+dropPrefix [] ms = Refl
614+dropPrefix (_ :: ns) ms = dropPrefix ns ms
616+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
617+dropDrop n Z xs = Refl
618+dropDrop {l} n (S k) (x :: xs) = rewrite aux (plusAssociative k n l) x xs in dropDrop n k xs
619+ where aux : {n : Nat} -> {m : Nat} -> (prf : n = m) ->
620+ (x : a) -> (xs : Vect m a) ->
621+ 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
622+ aux Refl x xs = Refl
624+takeDropConcat : (n : Nat) -> (xs : Vect (n + m) a) -> take n xs ++ drop n xs = xs
625+takeDropConcat Z xs = Refl
626+takeDropConcat (S k) (x :: xs) = cong $ takeDropConcat k xs
628+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)
629+takeDropDropTake n Z xs = Refl
630+takeDropDropTake {l} n (S k) (x :: xs) = rewrite aux (plusAssociative k n l) x xs in takeDropDropTake n k xs
631+ where aux : {n : Nat} -> {m : Nat} -> (prf : n = m) ->
632+ (x : a) -> (xs : Vect m a) ->
633+ 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
634+ aux Refl x xs = Refl
636+zipWithIsLiftA2 : (f : a -> b -> c) -> (as : Vect n a) -> (bs : Vect n b) -> zipWith f as bs = [| f as bs |]
637+zipWithIsLiftA2 _ [] [] = Refl
638+zipWithIsLiftA2 f (a :: as) (b :: bs) = rewrite zipWithIsLiftA2 f as bs in Refl
639+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 |]
640+zipWithIsLiftA3 _ [] [] [] = Refl
641+zipWithIsLiftA3 f (a :: as) (b :: bs) (c :: cs) = rewrite zipWithIsLiftA3 f as bs cs in Refl
643+-- Note relationship to Applicative (Morphism (Fin n))
644+indexReplicate : (x : a) -> (n : Nat) -> (i : Fin n) -> index i (replicate n x) = x
645+indexReplicate x (S n) FZ = Refl
646+indexReplicate x (S n) (FS i) = indexReplicate x n i
647+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)
648+indexZipWith f (a :: _) (b :: _) FZ = Refl
649+indexZipWith f (_ :: as) (_ :: bs) (FS i) = indexZipWith f as bs i
650+indexTranspose : (x : Fin o) -> (y : Fin i) -> (xss : Vect o (Vect i a)) -> index y (index x xss) = index x (index y (transpose xss))
651+indexTranspose x y (xs :: xss) = rewrite prf in
652+ rewrite sym $ indexZipWith Vect.(::) xs (transpose xss) y in Refl
653+ where prf : index y (index x (xs :: xss)) = index x (index y xs :: index y (transpose xss))
656+ FS k => indexTranspose k y xss
658+transposeTraverse : (xss : Vect o (Vect i a)) -> transpose xss = traverse Basics.id xss
659+transposeTraverse [] = Refl
660+transposeTraverse (xs :: xss) = rewrite zipWithIsLiftA2 Vect.(::) xs (transpose xss) in cong (transposeTraverse xss)
662+traverseIdCons : (xs : Vect o a) -> (xss : Vect o (Vect i a)) -> traverse Basics.id [| xs :: xss |] = xs :: traverse Basics.id xss
663+traverseIdCons [] [] = Refl
664+traverseIdCons (x :: xs) (ys :: xss) = rewrite traverseIdCons xs xss in Refl
665+transposeCons : (xs : Vect o a) -> (xss : Vect o (Vect i a)) -> transpose (zipWith (::) xs xss) = xs :: transpose xss
666+transposeCons xs xss = rewrite zipWithIsLiftA2 Vect.(::) xs xss in rewrite transposeTraverse (pure (::) <*> xs <*> xss) in rewrite transposeTraverse xss in traverseIdCons xs xss
637--------------------------------------------------------------------------------
668--------------------------------------------------------------------------------
639--------------------------------------------------------------------------------
670--------------------------------------------------------------------------------