### A Question about Magic With

I finished preparation for the midterm of Epistemology early, so now I've got time to try to prove that qsort is length-preserving "externally." Given a plain definition of qsort

partition : Nat -> List Nat -> List Nat × List Nat partition p [] = < [] , [] > partition p (x :: xs) with partition p xs | cmp x p ... | < ys , zs > | \/-IL x≼p = < x :: ys , zs > ... | < ys , zs > | \/-IR p≼x = < ys , x :: zs > qsort : List Nat -> List Nat qsort [] = [] qsort (x :: xs) with partition x xs ... | < ys , zs > = qsort ys ++ x :: qsort zs

the goal is proving

qsort-lenpres : {xs : List Nat} -> EqualLength xs (qsort xs)

I think it is necessary to prove that `partition`

is length-preserving first, so I come up with a function `pair-concat`

that concatenates a pair of lists into one and a proposition `partition-lenpres`

saying that `partition`

is length-preserving.

pair-concat : {A : Set} -> List A × List A -> List A pair-concat < xs , ys > = xs ++ ys partition-lenpres : (xs : List Nat)(p : Nat) -> EqualLength xs (pair-concat (partition p xs))

The proof of `partition-lenpres`

is (again) by induction. The base case is trivial.

partition-lenpres [] = eqlen-base

For the inductive case, I asked Agda for the normalised goal type, which is

EqualLength (x :: xs) (pair-concat (partition p (x :: xs) | cmp x p | partition p xs))

The bars naturally remind me of the "magic `with`

," which is explained on the Agda Wiki and whose usage I never understood before I work on this proof. According to the Agda Wiki, I should write something like

partition-lenpres (x :: xs) p with partition p xs | cmp x p -- magic with ... | < ys , zs > | \/-IL x≼p = ?_{0}... | < ys , zs > | \/-IR p≼x = ?_{1}

and the goal types for `?`

and _{0}`?`

would simply be _{1}`EqualLength (x :: xs) (x :: ys ++ zs)`

and `EqualLength (x :: xs) (ys ++ x :: zs)`

respectively. However when I put the induction hypothesis `partition-lenpres {xs}{p}`

in the place of `?`

, the normalised inferred type is
_{0}

EqualLength xs (pair-concat (partition p xs))

I would expect the innermost `partition p xs`

be replaced by `< ys , zs >`

and the whole type would be further normalised into

EqualLength xs (ys ++ zs)

then the hypothesis term would be a proof for `?`

after an application of _{0}`eqlen-step`

. But it doesn't work in that way! Now I cannot construct the desired induction hypothesis and get stuck here.

--

Is there a way to get around?

Labels: Agda, Programming

<< 回到主頁