QSort in Agda

繼續練習 dependent pairs as constraints or subtypes，這次挑上另一個經典的排序演算法 quick sort。首先是正常的版本。

-- plain qsort
qsort : List Nat -> List Nat
qsort [] = []
qsort (x :: xs) with partition x xs
  where
    partition : Nat -> List Nat -> List Nat × List Nat
    partition p [] = < [] , [] >
    partition p (x :: xs) with partition p xs
    ... | < ys , zs > = if x < p then < x :: ys , zs > else < ys , x :: zs >
... | < ys , zs > = (qsort ys) ++ (x :: (qsort zs))

我的目標是寫兩個版本的 qsort，一個證明 length-preserving，一個證明 increasingly-sorted，最後再看能不能很輕易地把這兩個版本合而為一。其實最好可以定義 IsPermutation 這種 predicate，可是之前試了一次，非常複雜，所以先練習這兩個比較簡單的性質 XD。不過事實證明，光證明 length-preserving 就有點麻煩了 XD。

首先定義「兩個 lists 長度相等」的 predicate。

data EqualLength {A B : Set} : List A -> List B -> Set where
  eqlen-base : EqualLength [] []
  eqlen-step : {x : A}{y : B}{xs : List A}{ys : List B} ->
                 EqualLength xs ys -> EqualLength (x :: xs) (y :: ys)

EqualLength 滿足 reflexivity 和 transitivity，所以可以啟用 chain reasoning（不過在這個程式裡沒怎麼用到就是了 XD）。

eqlen-refl : {A : Set}{xs : List A} -> EqualLength xs xs
eqlen-refl {_}{[]} = eqlen-base
eqlen-refl {_}{x :: xs} = eqlen-step (eqlen-refl {_}{xs})

eqlen-trans : {A B C : Set}{xs : List A}{ys : List B}{zs : List C} ->
                EqualLength xs ys -> EqualLength ys zs -> EqualLength xs zs
eqlen-trans {_}{_}{_}{[]}{[]}{[]} eqlen-base eqlen-base = eqlen-base
eqlen-trans {_}{_}{_}{x :: xs}{y :: ys}{z :: zs}
            (eqlen-step pf1) (eqlen-step pf2) = eqlen-step (eqlen-trans pf1 pf2)

open module Chain-EqualLength =
  Logic.ChainReasoning.Mono.Homogenous
    {List Nat} EqualLength (\_ -> eqlen-refl) (\_ _ _ -> eqlen-trans)
    renaming (chain>_ to chainˡ>_ ; _===_ to _===ˡ_ ; _by_ to _byˡ_)

現在重新定義 partition，夾帶 length-preserving 的證明。

partition' : Nat -> (xs : List Nat) ->
               List Nat × List Nat ∣ (\p -> EqualLength xs (fst p ++ snd p))
partition' p [] = sub < [] , [] > eqlen-base
partition' p (x :: xs) with partition' p xs
... | sub < ys , zs > sub-eqlen-pf =
  if x < p then (sub < x :: ys , zs >
                     (chainˡ> x :: xs
                         ===ˡ x :: (ys ++ zs) byˡ eqlen-step sub-eqlen-pf
                         ===ˡ x :: ys ++ zs byˡ eqlen-refl))
           else (sub < ys , x :: zs >
                     (chainˡ> x :: xs
                         ===ˡ ys ++ x :: zs
                                byˡ lemma1 x x xs ys zs sub-eqlen-pf))

lemma1 的證明。

lemma1 : {A : Set}(x z : A)(xs ys zs : List A) ->
          EqualLength xs (ys ++ zs) -> EqualLength (x :: xs) (ys ++ z :: zs)
lemma1 _ _ _ [] _ pf = eqlen-step pf
lemma1 a b (c :: xs) (d :: ys) zs (eqlen-step pf) =
  eqlen-step {_}{_}{a}{d} (lemma1 c b xs ys zs pf)

然後是 qsort 本身。with 相關的 parsing 好像還沒做到最彈性，所以我在這裡都不用省略符號 "..."。

qsort' : (xs : List Nat) -> List Nat ∣ EqualLength xs
qsort' [] = sub [] eqlen-base
qsort' (x :: xs) with partition' x xs
qsort' (x :: xs) | sub < ys , zs > pf with qsort' ys | qsort' zs
qsort' (x :: xs) | sub < ys , zs > pf | sub ys' pf1 | sub zs' pf2 =
  sub (ys' ++ x :: zs')
      (chainˡ> x :: xs
          ===ˡ ys' ++ x :: zs' byˡ lemma1 x x xs ys' zs'
               (chainˡ> xs
                   ===ˡ ys ++ zs byˡ pf
                   ===ˡ ys' ++ zs' byˡ lemma2 pf1 pf2))

最後是 lemma2 的證明。

lemma2 : {A B : Set}{ys zs : List A}{ys' zs' : List B} ->
           EqualLength ys ys' -> EqualLength zs zs' ->
           EqualLength (ys ++ zs) (ys' ++ zs')
lemma2 {_}{_}{[]}{zs}{[]}{zs'} _ pf2 = pf2
lemma2 {_}{_}{y :: ys}{zs}{y' :: ys'}{zs'} (eqlen-step pf1) pf2 =
  eqlen-step (lemma2 {_}{_}{ys}{zs}{ys'}{zs'} pf1 pf2)

--
夾帶 sortedness proof 的版本明天寫 XD。