splitAt = take, drop proof

1 files changed, 15 insertions, 10 deletions

diff --git a/Ch10.idr b/Ch10.idr
index 1ef5a45..9ab70ce 100644
--- a/Ch10.idr
+++ b/Ch10.idr
@@ -3,18 +3,23 @@ module Ch10
 data TakeN : List a -> Type where
   Fewer : TakeN xs
   Exact : (n_xs : List a) -> TakeN (n_xs ++ rest)
- 
+
+splitStep : a -> (List a, List a) -> (List a, List a)
+splitStep x (xs, ys) = (x :: xs, ys)
+
 mySplit : (n : Nat) -> (input : List a) -> (List a, List a)
 mySplit n [] = ([], [])
 mySplit Z xs = ([], xs)
-mySplit (S k) (x :: xs) = let (this, rest) = (mySplit k xs) in
-                          (x :: this, rest)
-                          
-mySplit_keeps_list : (n : Nat) -> (input : List a) ->
-                     mySplit n input = (as, bs) -> as ++ bs = input
-mySplit_keeps_list Z [] Refl = Refl
-mySplit_keeps_list (S k) [] Refl = Refl
-mySplit_keeps_list Z (x :: xs) Refl = Refl
-mySplit_keeps_list (S k) (x :: xs) prf = ?hole  -- ????
+mySplit (S k) (x :: xs) = splitStep x (mySplit k xs)  
+
+mySplitIsTakeDrop : (n : Nat) -> (input : List a) ->
+                    mySplit n input = (take n input, drop n input)
+mySplitIsTakeDrop Z [] = Refl
+mySplitIsTakeDrop Z (x::xs) = Refl
+mySplitIsTakeDrop Z [] = Refl
+mySplitIsTakeDrop (S k) [] = Refl
+mySplitIsTakeDrop (S k) (x::xs) =
+  let rec = mySplitIsTakeDrop k xs in
+  rewrite rec in Refl
 
 takeN : (n : Nat) -> (input : List a) -> TakeN input