updated version of https://github.com/bmsherman/blog/wiki/Quicksort-in-Idris

Qsort.idr

module Qsort

%default total

data PreOrder : (a : Type) -> (a -> a -> Type) -> Type where
  PrO : {ltef : a -> a -> Type} -- <=
      -> ((x, y, z : a) -> ltef x y -> ltef y z -> ltef x z)  -- transitivity
      -> PreOrder a ltef

data TotalOrder : (a : Type) -> (a -> a -> Type) -> Type where
  TotO : PreOrder a ltef -> ((x, y : a) 
      -> Either (ltef y x) (ltef x y)) 
      -> TotalOrder a ltef

data Forall : (a -> Type) -> List a -> Type where
  None : Forall p []
  And : p x -> Forall p xs -> Forall p (x :: xs)      

impList : (f : (x : a) -> p x -> q x)
        -> (xs : List a) -> Forall p xs
        -> Forall q xs
impList f []         None        = None
impList f (x :: xs) (And px pxs) = And (f x px) (impList f xs pxs)

forallZipWith : (f : (x : a) -> p x -> q x -> r x)
             -> (xs : List a) -> Forall p xs -> Forall q xs -> Forall r xs
forallZipWith f []         None         None        = None
forallZipWith f (x :: xs) (And px pxs) (And qx qxs) = 
  And (f x px qx) (forallZipWith f xs pxs qxs)
  
propAppList : (ys : List a) -> (zs : List a)
            -> Forall p (ys ++ zs)
            -> (Forall p ys, Forall p zs)
propAppList []        zs  pzs           = (None, pzs)
propAppList (y :: ys) zs (And py pyszs) =
  let (pys, pzs) = propAppList ys zs pyszs in
  (And py pys, pzs)

propCatList : (ys : List a) -> Forall p ys
           -> (zs : List a) -> Forall p zs
           -> Forall p (ys ++ zs)
propCatList []         _           _  pzs = pzs
propCatList (_ :: ys) (And py pys) zs pzs =
  let pyszs = propCatList ys pys zs pzs in
  And py pyszs
  
data IsSorted : (a -> a -> Type) -> List a -> Type where
  None1 : IsSorted ltef []
  And1 : {ltef : a -> a -> Type} 
       -> Forall (ltef y) ys -> IsSorted ltef ys -> IsSorted ltef (y :: ys)
       
data Permutation : List a -> List a -> Type where
  Empty : Permutation [] []
  Split : (xs : List a) -> (ys : List a) -> (zs : List a)
        -> Permutation xs (ys ++ zs) -> Permutation (x :: xs) (ys ++ (x :: zs))
  Comp : Permutation xs ys -> Permutation ys zs -> Permutation xs zs
  Cat : Permutation xs zs -> Permutation ys ws -> Permutation (xs ++ ys) (zs ++ ws)
  
forallPerm : (xs : List a) -> Forall p xs
           -> (ys : List a) -> Permutation xs ys
           -> Forall p ys
forallPerm     []        None         []                _                          = None
forallPerm     _        (And px pxs) (ys ++ (x :: zs)) (Split xs ys zs permxsyszs) = 
  let (pys, pzs) = propAppList ys zs (forallPerm xs pxs (ys ++ zs) permxsyszs) in
  propCatList ys pys (x :: zs) (And px pzs)
forallPerm {p} xs        pxs          zs               (Comp {ys} permxy permyz)   = 
  forallPerm ys pys zs permyz
  where
  pys : Forall p ys
  pys = forallPerm xs pxs ys permxy
forallPerm    (xs ++ ys) pxsys       (zs ++ ws)        (Cat permxszs permysws)     = 
  let (pxs, pys) = propAppList xs ys pxsys 
      pzs = forallPerm xs pxs zs permxszs 
      pws = forallPerm ys pys ws permysws 
     in
  propCatList zs pzs ws pws
  
data LTEL : List a -> List a -> Type where
  LTELNil  : LTEL [] xs
  LTELCons : LTEL xs ys -> LTEL (x :: xs) (y :: ys)
  
loosenLTEL : LTEL xs ys -> LTEL xs (y :: ys)
loosenLTEL  LTELNil       = LTELNil
loosenLTEL (LTELCons prf) = LTELCons (loosenLTEL prf)

reflLTEL : (xs : List a) -> LTEL xs xs
reflLTEL []        = LTELNil
reflLTEL (_ :: xs) = LTELCons (reflLTEL xs)

transLTEL : LTEL xs ys -> LTEL ys zs -> LTEL xs zs
transLTEL  LTELNil        _              = LTELNil
transLTEL (LTELCons prf) (LTELCons prf2) = LTELCons (transLTEL prf prf2)

partition' : {p : a -> Type} -> {q : a -> Type}
	   -> (f : (x : a) -> Either (p x) (q x))
	   -> (xs : List a)
	   -> (ys : List a ** 
	       zs : List a ** 
	       ( LTEL ys xs, LTEL zs xs
	       , Forall p ys, Forall q zs, Permutation xs (ys ++ zs) )
	      )
partition' f [] = ( [] ** [] ** (LTELNil, LTELNil, None, None, Empty) )
partition' f (x :: xs) = 
  let (ys ** zs ** (ysSmall, zsSmall, pys, qzs, permxs)) = partition' f xs in
  case f x of
    Left  px => ( (x :: ys) ** zs ** (LTELCons ysSmall, loosenLTEL zsSmall
                , And px pys, qzs, Split xs [] (ys ++ zs) permxs ) )
    Right qx => ( ys ** (x :: zs) ** (loosenLTEL ysSmall, LTELCons zsSmall
                , pys, And qx qzs, Split xs ys zs permxs ) )

ordPartition : TotalOrder a ltef
             -> (pivot : a) -> (xs : List a)
             -> (ys : List a ** 
                 zs : List a **
               ( LTEL ys xs, LTEL zs xs
               , Forall (flip ltef pivot) ys, Forall (ltef pivot) zs
               , Forall (\y => Forall (ltef y) zs) ys, Permutation xs (ys ++ zs))
               )
ordPartition {ltef} (TotO (PrO transt) eith) pivot xs = 
  let (ys ** zs ** (ysSmall, zsSmall, pys, qzs, perm)) = 
            partition' {p=flip ltef pivot} {q=ltef pivot} (eith pivot) xs in
  (ys ** zs ** (ysSmall, zsSmall, pys, qzs, lem2 zs qzs ys pys , perm) )
  where
  lem : (y : a) -> ltef y pivot -> (zs : List a) 
      -> Forall (ltef pivot) zs -> Forall (ltef y) zs
  lem y yltx = impList (\z, xltz => transt y pivot z yltx xltz)
  lem2 :  (zs : List a) -> Forall (ltef pivot) zs
       -> (ys : List a) -> Forall (flip ltef pivot) ys 
       -> Forall (\y => Forall (ltef y) zs) ys
  lem2 zs xltzs = impList (\y, yltx => lem y yltx zs xltzs)
    
partSorted : (xs : List a) -> IsSorted ltef xs
           -> (ys : List a) -> IsSorted ltef ys
           -> Forall (\x => Forall (ltef x) ys) xs
           -> IsSorted ltef (xs ++ ys)
partSorted []                _                  _  sortys  _                 = sortys
partSorted (x :: xs) {ltef} (And1 xltxs sortxs) ys sortys (And xltys xsltys) =
  And1 xltxsys sortxsys
  where
  sortxsys : IsSorted ltef (xs ++ ys)
  sortxsys = partSorted xs sortxs ys sortys xsltys
  xltxsys : Forall (ltef x) (xs ++ ys)
  xltxsys = propCatList xs xltxs ys xltys
  
quicksortHelper : TotalOrder a ltef
		-> (xs : List a)
		-> (listBound : List a)
		-> (xsSmall : LTEL xs listBound)
		-> (ys : List a ** (IsSorted ltef ys, Permutation xs ys))
quicksortHelper        _         []        _           _                  = ([] ** (None1, Empty) )
quicksortHelper {ltef} totorder (x :: xs) (xB :: xsB) (LTELCons xsSmall) = 
  -- partition
  let (ys ** zs ** (ysSmall, zsSmall, ysltx, xltzs, ysltzs, perm)) = 
        ordPartition totorder x xs 
  -- recursive calls
      (ys' ** (sortedys', permysys')) = 
        quicksortHelper totorder ys xsB (transLTEL ysSmall xsSmall) 
      (zs' ** (sortedzs', permzszs')) = 
        quicksortHelper totorder zs xsB (transLTEL zsSmall xsSmall)

  -- show our result list is sorted
      ysltzs' : Forall (\y => Forall (ltef y) zs') ys
         = impList (\y, yltzs => forallPerm zs yltzs zs' permzszs') ys ysltzs
      ys'ltzs' : Forall (\y => Forall (ltef y) zs') ys'
               = forallPerm ys ysltzs' ys' permysys'
      ys'ltx : Forall (flip ltef x) ys'
             = forallPerm ys ysltx ys' permysys'
      ys'ltxzs' : Forall (\y => Forall (ltef y) (x :: zs')) ys' 
                = forallZipWith (\y => And) ys' ys'ltx ys'ltzs'
      sortedxzs' : IsSorted ltef (x :: zs')
                 = And1 (forallPerm zs xltzs zs' permzszs') sortedzs'
      sortedys'xzs' : IsSorted ltef (ys' ++ x :: zs')
                    = partSorted ys' sortedys' (x :: zs') sortedxzs' ys'ltxzs'

  -- show our result list is a permutation of the original list
      perm' : Permutation (ys ++ zs) (ys' ++ zs')
            = Cat permysys' permzszs'
      perm'' : Permutation xs (ys' ++ zs')
             = Comp perm perm'
      permAll : Permutation (x :: xs) (ys' ++ x :: zs')
              = Split xs ys' zs' perm'' 
     in

  -- put it all together!
  (ys' ++ (x :: zs') ** ( sortedys'xzs', permAll) )
  
quicksort : TotalOrder a ltef
	  -> (xs : List a)
	  -> (ys : List a ** (IsSorted ltef ys, Permutation xs ys))
quicksort totorder xs = quicksortHelper totorder xs xs (reflLTEL xs)

natLTETrans : (n, m, o : Nat) -> LTE n m -> LTE m o -> LTE n o
natLTETrans  Z     _     _     _           _          = LTEZero
natLTETrans (S n) (S m) (S o) (LTESucc p) (LTESucc q) = LTESucc (natLTETrans n m o p q)

natLTEEith : (x, y : Nat) -> Either (LTE y x) (LTE x y)
natLTEEith  Z     _    = Right LTEZero
natLTEEith  _     Z    = Left LTEZero
natLTEEith (S n) (S m) with (natLTEEith n m)
  | Right x = Right (LTESucc x)
  | Left y  = Left (LTESucc y)

totNat : TotalOrder Nat LTE 
totNat = TotO (PrO natLTETrans) natLTEEith

test : fst $ quicksort Qsort.totNat [5,3,2,6,1] = [1,2,3,5,6]
test = Refl