### 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: Agda, Programming

<< 回到主頁