$\newcommand{\defeq}{\mathrel{\mathop:}=}$

## 2007/11/10

### QSort in Agda

-- 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))


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' : 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' : (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 : {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)


--

Labels: ,