rewrite
rewrite is a spiffy pseudo-tactic in Agda that allows you to leverage dependent pattern matching on equality types to "rewrite" sub-terms in your goal. It can be very useful when a solution to the rewritten goal is obvious, but fails spectacularly if you want to do further analysis on the terms in scope. Let's look at an example - a very dumb "swap" function that takes a Vector with an even length and swaps the position of every two elements. I say "dumb" for two reasons: 1) if you want to swap pairs of adjacent elements, you really should be working on a list of pairs; 2) the way we will be expressing "even length" is by using n + n, which does not match the structure we will be working on (this length would work better if we were splitting the vector up and putting the second half in front of the first, like cutting a deck of cards).
The first thing we have to deal with isn't related to with or rewrite - Agda won't in general try to deconstruct an arbitrary expression with functions inside of it when it isn't obvious which constructor to apply. In this case it's not a big deal - we just pattern match on n instead.
Ok, so we've delt with the empty case. We know that our input list has an even number of items in it, so if it's not 0, then it has at least 2 elements in it. That means we should be able to pattern match on xs further to get the next item. Right?
Now, we know that a vector of length n + suc n is non-empty, and thus we should be able to pattern match on the tail of our original list xs because there's only one constructor that applies, but again this is not obvious to Agda. So now we get to rewrite - we want to use the lemma that says suc distributes left over addition.
Groovy! And now to pattern match on xs to get our second element (after importing Propositional equality, which is what the function +-suc returns.)
Oh no! What's happened? The answer comes from reading the Agda wiki entry on rewrite and putting 2 and 2 together (or in this case, n and n). Essentially, all rewrite does is provide sugar for saying with a | eq when a b : A and eq : a ≡ b.
In this situation, when you want to pattern match on a term in scope whose type has been rewritten in this way, the only path forward is to manually de-sugar and use with.
And pattern match on eq...
And now finally we can pattern match on xs, since it's now in the right form.
After getting through all that, I realized that Agda won't in general infer the n of a Vector of length n + n, and thus I should not have made it implicit. Oh well.
Writing this blog makes me think I should make YouTube videos of me programming in Agda live. Might be a better format for things like this than screenshots of my editor window.
Update: OK, so I do have a YouTube video now. Please forgive the poor quality: https://www.youtube.com/watch?v=g_s5G5vqjQc
Thanks for this great post, Chris. I have encountered similar strange phenomena with "with" before, but your description of this particular one, and the workaround for it, are quite helpful.
ReplyDeleteFWIW, here is how I would workaround this issue; by introducing a helper function with "where":
swap : ∀{l}{A : Set l}{n} → Vec A (n + n) → Vec A (n + n)
swap {n = 0} [] = []
swap {A = A}{n = suc n} (x :: xs) rewrite +suc n n = go xs
where go : Vec A (suc (n + n)) → Vec A (suc (suc (n + n)))
go (x' :: xs') = (x' :: x :: (swap{n = n} xs'))
(Had to transliterate a bit from Unicode to be accepted in the comment.)
Aaron
"There are many ways to skin a type", as they say ;)
DeleteThis is a good solution, though there is a trade-off: if the return type of the function depends on the original argument, the local re-bindings to x' and xs' may make it difficult for Agda to tell that xs *really is* x' :: xs'.