`with': hold computation from those to whom it is due (Pt. 2)

   In the post prior, I showed how to pattern match on a rewritten term by manually de-sugaring to `with'. This post will discuss a "gotcha" when writing a proof about a function that uses `with': holding up the computation. And in this case, it will reveal just why the version of swap I defined earlier is a particularly poorly written function.

   Let's get back to speed with where we were:

   We now want to write a simple proof - that swap is involutive, i.e. that it is its own inverse. Our type signature for swap-involutive:

   As a general rule, in order to prove something about a function, you will frequently have to follow the same decision tree as the function, e.g. if the function you're interested in does case analysis on a term, you probably will too. We started with n before, so

   Hmm, what's this? Why doesn't it normalize to [] ≡ [] in the first case? Even thought that's the only case that can come of this, Agda will not do any normalization unless its arguments exactly match a decision tree - in this case, we need to analyse xs, just like we did in our original function.

   If you type the special Emacs agda-mode command C-u C-, you will see the goal pre-normalization - swap zero (swap zero []) ≡ [] . Anyway, it's easy to see where to go on from here, so now let's fill the first goal, pattern match on our tail in the second case, and see what awaits!

   Woah! What are those bars doing in my goal? You can think of this as Agda's way of explicitly telling you what's holding up the computation. In our case, it's the term we rewrote and the equation we rewrote it by. In these situations I proceed in the following way: bring in each "with-held" term one at a time interactively (but all at once programmatically, e.g. all in the same use of `with'). Like so - first our equation:

Notice how +-suc n n got rewritten to eq after the bar in the goal? And now we'll try n + suc n ...

   Oh no! The red text of death! What did we do wrong? Well, reading this error is a bit of a pain - Agda wasn't able to get through type-checking the file before it reached an error, and as a consequence didn't rebind it's internal w₁ (the second with pattern, n + suc n) to our nicer name, n+sn.

   Well ok. But then it's saying w₁, which is the term we bound to n + suc n, is not n + suc n? W₁TF? Is Agda completely out of its mind? Well... no. It's hard to spot, but look at the given type signature of xs. It's Vec A w₁. We have rewritten all of the naked occurrences of n + suc n, but swap still relies on that expression (via its argument n) for its vector argument and return type. Therefore, when we rewrite xs and try to put it back where we found it, Agda complains because now swap isn't being fed an argument that (syntactically) conforms to its type. We need some way to rewrite the type of swap itself!

   I wish I could show you a solution now, but unfortunately, though I have tried many ways to skin this type, I have not had success. I'm hoping someone on #agda can help me out here when I get around to asking them (basically, when I swallow my pride and give up trying to do it myself).

   Instead, I leave with a closing thought - in my previous blog-post, I mentioned Conor McBride had a bit of difficulty defining this version of swap. I felt pretty smug about myself (althought hopefully it didn't show) that I had managed to succeed here. But after all my efforts in trying to show this swap is involutive, it occurs to me that Conor's wisdom was in avoiding a bad program as early as possible. If I may paraphrase: "Only fools code boldly where Conor McBride fears to tread."