### A Question about Magic With --- Resolved

While I was on the bed listening to Eric Clapton's *Bell Bottom Blues*, it occurred to me that I could probably use `subst`

to replace `partition p xs`

with `< ys , zs >`

, i.e., something like

subst (\X -> EqualLength xs (pair-concat X)) (refl {< ys , zs >}) (partition xs p)

I expect there are some mysterious connection between a term and a pattern that is matched with the term, which would remind Agda that `partition p xs`

is in fact `< ys , zs >`

. Unfortunately it failed. But not much later I came up with the idea that maybe doing a direct `with`

-match on `partition-lenpres xs p`

would work, and indeed it worked! The final result is

partition-lenpres : (xs : List Nat)(p : Nat) -> EqualLength xs (pair-concat (partition p xs)) partition-lenpres [] _ = eqlen-base partition-lenpres (x :: xs) p with partition p xs | cmp x p | partition-lenpres xs p -- magic with ... | < ys , zs > | \/-IL x≼p | indHyp = eqlen-step indHyp ... | < ys , zs > | \/-IR p≼x | indHyp = lemma1 x x xs ys zs indHyp

where `lemma1`

has been proved when I was working on the "intrusive" proof.

lemma1 : {A : Set}(x z : A)(xs ys zs : List A) -> EqualLength xs (ys ++ zs) -> EqualLength (x :: xs) (ys ++ z :: zs)

--

Excellent! Though I still don't understand exactly how `with`

works...

Labels: Agda, Programming

<< 回到主頁