partition_length

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
import Data.Vect

partition_condition : (f : elem -> Bool) -> (v : Vect n elem) -> Type
partition_condition {n} f v =
  case partition f v of
    ((z1 ** pt), (z2 ** pf)) => z1 + z2 = n

total
partition_length : (f : elem -> Bool) -> (v : Vect n elem) -> partition_condition f v
partition_length f [] = Refl
partition_length f (x :: xs) with (partition_length f xs)
  | IH with (partition f xs)
    | ((p ** vt), (q ** vf)) with (f x)
      | False =
        rewrite sym (plusSuccRightSucc p q) in
        rewrite IH in Refl
      | True =
        rewrite IH in Refl