From f18fdcb2e0d1ef4ce1cf5892dec99909126af129 Mon Sep 17 00:00:00 2001 From: Kjetil Orbekk Date: Tue, 14 Feb 2017 14:59:39 -0500 Subject: splitAt = take, drop proof --- Ch10.idr | 25 +++++++++++++++---------- 1 file 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 -- cgit v1.2.3