QuickSort is harder than one may think.

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
import Data.Vect
import Prelude.WellFounded

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

total
partition_length : (f : elem -> Bool) -> (v : Vect n elem) -> partition_condition n 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

total
qsort_step :
  Ord elem
  => (n : Nat)
  -> ((m : Nat) -> (LT m) n -> Vect m elem -> Vect m elem)
  -> Vect n elem -> Vect n elem
qsort_step Z rec [] = []
qsort_step (S k) rec (x :: xs) with (partition_length (< x) xs)
  | length_lem with (partition (< x) xs)
    | ((p ** vt), (q ** vf)) =
      rewrite length_lem in
      rewrite plusSuccRightSucc p q in
        let lem1 : LT p (S k) = rewrite length_lem in LTESucc (lteAddRight p)
            lem2 : LT q (S k) = rewrite length_lem in rewrite plusCommutative p q in LTESucc (lteAddRight q)
        in (rec _ lem1 vt ++ x :: rec _ lem2 vf)

qsort : Ord elem => Vect n elem -> Vect n elem
qsort {elem} {n} =
  accInd {rel = LT} {P = (\k => Vect k elem -> Vect k elem)} qsort_step n (ltAccessible n)