@@ -0,0 +1,98 @@
5+-- First list is smaller than the second
6+smaller : List a -> List a -> Type
7+smaller xs ys = LT (length xs) (length ys)
9+-- Some proofs to help us out with recursion later
10+ltS : LTE (S x) y -> LTE x y
11+ltS (LTESucc x) = lteSuccRight x
14+ltTrans : LTE n m -> LTE m p -> LTE n p
15+ltTrans LTEZero y = LTEZero
16+ltTrans (LTESucc x) (LTESucc y) = LTESucc (ltTrans x y)
18+ltZimpossible : (x : smaller xs []) -> Accessible smaller xs
19+ltZimpossible LTEZero impossible
20+ltZimpossible (LTESucc _) impossible
23+smallerAcc : (ys : List a) -> smaller xs ys -> Accessible smaller xs
24+smallerAcc [] x = ltZimpossible x
25+smallerAcc (y :: ys) (LTESucc x)
26+ = Access (\val, p => smallerAcc ys (ltTrans p x))
28+lengthSuc : (xs : List a) -> (y : a) -> (ys : List a) ->
29+ length (xs ++ (y :: ys)) = S (length (xs ++ ys))
30+lengthSuc [] _ _ = Refl
31+lengthSuc (x :: xs) y ys = cong (lengthSuc xs y ys)
33+lengthLT : (xs : List a) -> (ys : List a) ->
34+ LTE (length xs) (length (ys ++ xs))
35+lengthLT xs [] = lteRefl
36+lengthLT xs (x :: ys) = lteSuccRight (lengthLT _ _)
38+smallerLeft : (ys : List a) -> (y : a) -> (zs : List a) ->
39+ LTE (S (S (length ys))) (S (length (ys ++ (y :: zs))))
40+smallerLeft [] y zs = LTESucc (LTESucc LTEZero)
41+smallerLeft (z :: ys) y zs = LTESucc (smallerLeft ys _ _)
43+smallerRight : (ys : List a) -> (zs : List a) ->
44+ LTE (S (S (length zs))) (S (length (ys ++ (y :: zs))))
45+smallerRight {y} ys zs = rewrite lengthSuc ys y zs in
46+ (LTESucc (LTESucc (lengthLT _ _)))
48+||| View for splitting a list in half, non-recursively
50+data Split : List a -> Type where
53+ SplitPair : Split (x :: xs ++ y :: ys)
55+splitHelp : (head : a) ->
57+ (counter : List a) -> Split (head :: xs)
58+splitHelp head [] counter = SplitOne
59+splitHelp head (x :: xs) [] = SplitPair {xs = []} {ys = xs}
60+splitHelp head (x :: xs) [y] = SplitPair {xs = []} {ys = xs}
61+splitHelp head (x :: xs) (_ :: _ :: ys)
62+ = case splitHelp head xs ys of
63+ SplitOne => SplitPair {xs = []} {ys = []}
64+ SplitPair {xs} {ys} => SplitPair {xs = (x :: xs)} {ys = ys}
66+||| Covering function for the `Split` view
68+split : (xs : List a) -> Split xs
70+split (x :: xs) = splitHelp x xs xs
72+||| View for splitting a list in half, recursively
74+||| This allows us to define recursive functions which repeatedly split lists
75+||| in half, with base cases for the empty and singleton lists.
77+data SplitRec : List a -> Type where
78+ SplitRecNil : SplitRec []
79+ SplitRecOne : SplitRec [x]
80+ SplitRecPair : Lazy (SplitRec xs) -> Lazy (SplitRec ys) -> SplitRec (xs ++ ys)
83+splitRecFix : (xs : List a) -> ((ys : List a) -> smaller ys xs -> SplitRec ys) ->
85+splitRecFix xs srec with (split xs)
86+ splitRecFix [] srec | SplitNil = SplitRecNil
87+ splitRecFix [x] srec | SplitOne = SplitRecOne
88+ splitRecFix (x :: (ys ++ (y :: zs))) srec | SplitPair
89+ = let left = srec (x :: ys) (smallerLeft ys y zs)
90+ right = srec (y :: zs) (smallerRight ys zs) in
91+ SplitRecPair left right
93+||| Covering function for the `SplitRec` view
95+splitRec : (xs : List a) -> SplitRec xs
96+splitRec [] = SplitRecNil
97+splitRec (x :: xs) = accInd splitRecFix (x :: xs) (smallerAcc (x :: x :: xs) lteRefl)