module Ch10

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
  
mySplitPreservesElements : (n : Nat) -> (input : List a) -> ((ps, qs) = mySplit n input) -> ps ++ qs = input
mySplitPreservesElements n input prf =
  let prf2 = mySplitIsTakeDrop n input in
  case trans prf prf2 of Refl => takeDropIsIdentity n input

data Partition : List a -> Type where
  Split : (xs, ys : List a) -> Partition (xs ++ ys)

test : (input : List a) -> Partition input
test zs =
  let (xs, ys) = mySplit 5 zs in ?test
  

data TakeN : List a -> Type where
  Fewer : TakeN xs
  Exact : (n_xs : List a) -> TakeN (n_xs ++ rest)
  
-- takeN : (n : Nat) -> (input : List a) -> TakeN input
-- takeN n input =
--   let (n_xs, rest) = mySplit n input in
--   let prf0 = mySplitPreservesLength n input ?foo in
--   let prf = the (n_xs ++ rest = input) ?my in
--     if length n_xs < n
--       then Fewer
--       else ?hole