blob: b9e47141b70886a1d7b144fd59238027d4ef7681 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
|
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
|
