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) = 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
  
takeDropIsIdentity : (n : Nat) -> (input : List a) -> take n input ++ drop n input = input
takeDropIsIdentity Z input = Refl
takeDropIsIdentity (S k) [] = Refl
takeDropIsIdentity (S k) (x :: xs) =
  rewrite takeDropIsIdentity k xs in Refl

takeN : (n : Nat) -> (input : List a) -> TakeN input