Report a paste

Please put a quick comment for the admin.

If it looks like spam, the admin will mark it as spam so that the spam filter picks it up in the future.

If the paste contains something private or offensive, it'll probably just be deleted.

QuickSort is harder than one may think.

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)