@@ -138,12 +138,17 @@ lsplit (x :: xs) (S k) prf (S l) right prf1
138 (x :: lsrec' ** rsrec' ** (eqSucc _ _ lprf, rprf, rewrite recprf in Refl))
138 (x :: lsrec' ** rsrec' ** (eqSucc _ _ lprf, rprf, rewrite recprf in Refl))
139lsplit (_ :: _) Z Refl (S _) _ _ impossible
139lsplit (_ :: _) Z Refl (S _) _ _ impossible
141+||| Proof that two numbers differ by at most one
141data Balanced : Nat -> Nat -> Type where
143data Balanced : Nat -> Nat -> Type where
142 BalancedZ : Balanced Z Z
144 BalancedZ : Balanced Z Z
143 BalancedL : Balanced (S Z) Z
145 BalancedL : Balanced (S Z) Z
144 BalancedRec : Balanced n m -> Balanced (S n) (S m)
146 BalancedRec : Balanced n m -> Balanced (S n) (S m)
146−-- Question: worth exporting?
148+||| View of a list split into two halves
150+||| The lengths of the lists are guaranteed to differ by at most one
147data SplitBalanced : List a -> Type where
152data SplitBalanced : List a -> Type where
148 MkSplitBal : {xs, ys : List a} ->
153 MkSplitBal : {xs, ys : List a} ->
149 Balanced (length xs) (length ys) -> SplitBalanced (xs ++ ys)
154 Balanced (length xs) (length ys) -> SplitBalanced (xs ++ ys)
@@ -168,6 +173,10 @@ splitBalancedLen xs n prf with (half n)
168 lsplit xs (x + x) prf x x Refl in
173 lsplit xs (x + x) prf x x Refl in
169 rewrite apprf in (MkSplitBal (mkBalanced lprf rprf))
174 rewrite apprf in (MkSplitBal (mkBalanced lprf rprf))
176+||| Covering function for the `SplitBalanced`
178+||| Constructs the view in linear time
171splitBalanced : (xs : List a) -> SplitBalanced xs
180splitBalanced : (xs : List a) -> SplitBalanced xs
172splitBalanced xs = splitBalancedLen xs (length xs) Refl
181splitBalanced xs = splitBalancedLen xs (length xs) Refl