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

## 2007/11/12

### QSort in Agda, Round 3

After figuring out how to use the magic with, the rest is quite straightforward --- the logic is identical to the one used to prove the intrusive version.

qsort-lenpres : ∀ (\xs -> EqualLength xs (qsort xs))
qsort-lenpres [] = eqlen-base
qsort-lenpres (x :: xs) with partition x xs | partition-lenpres xs x
qsort-lenpres (x :: xs) | < ys , zs > | ind-hyp₁ with qsort-lenpres ys
| qsort-lenpres zs
qsort-lenpres (x :: xs) | < ys , zs > | ind-hyp₁ | ind-hyp₂ | ind-hyp₃ =
chainˡ> x :: xs
===ˡ qsort ys ++ x :: qsort zs byˡ lemma1 x x xs (qsort ys) (qsort zs)
(chainˡ> xs
===ˡ ys ++ zs byˡ ind-hyp₁
===ˡ qsort ys ++ qsort zs byˡ lemma2 ind-hyp₂ ind-hyp₃)


It seems that one has to with-match partition x xs and partition-lenpres xs x simultaneously in order to make Agda know that partition x xs is indeed < ys , zs > when it is inferring the type of ind-hyp₁.

--
I really have to go to bed now since I've got a midterm in the morning. XD

Labels: ,