Equational Reasoning vs rewrite in Agda: Rewrite

My first blog post will not be terribly ambitious. I have been learning how to program in Agda, a dependently typed functional language / theorem proving assistant and recently I hit a roadblock while trying to prove some basic properties about arithmetic (like that addition is associative, multiplication distributes over addition, etc). I am going to write about the problem and what I learned from it, in the hopes that other new Agda programmers might benefit from it, especially since I'm not aware of any other in-depth treatment of this topic (feel free to share a link in the comments if you know of something.)

So, often we would like to prove some property P about some term x (we'll notate that as P x), and we have that x ≡ y and further we know how to prove P y. We should be able to use this fact to prove P x then.

Here's an example: while trying to prove that addition is commutative, I worked my way into a sub-case of proving suc (m + 0) ≡ suc m.

Sadly, I can't simply apply lem-n≡n+0 because the structure doesn't match - that lemma will give us m' ≡ m + 0 but the successor operation gets in the way. So what can we do?

Agda version 2.2.6 introduces a syntactic sugar called rewrite. There's no need to go into detail here what it's sugar for since that's well documented in the release notes and on the Wiki. What is important is how it can be used - to rewrite arbitrary terms in our goal type using any equivalence we have available (left to right).

Using it in our example would yield:

 and at that point we need only supply refl to finish the proof.

 Now, of course we could have solved this a different way, but using rewrite did not involve any extra lemmas or recursion, and in this example it's rather clean looking. But how does it scale with a more complex example, such as proving an important lemma for our proof of commutativity - that m + suc n ≡ n + suc n?

 And now fast forwarding a bit


 Having gotten this far, I found myself a little stuck. Again, we can't merely solve for our goal with recursion on lem-comm-under-suc because the structres of the two sides of the equation don't match (suc n is not n). But with a little help from rewrite we get

Again, this is quite nice. However, in this and in the next example I will show we can start to see one of the major drawbacks of using rewrite too liberally. My images show the intermediate goal types that I (the programmer) can see as I write, but the end result may not show clearly the process of proving the goal type.

Additionally, while in this example I used all my rewrites on the left hand side before I supplied answers on the right, but in the process of writing these proofs it possible to interleave editing the right and left hand sides of the equation, making it even harder for the reader. For example, rewrite may be used to rewrite a term that does not even appear in the immediate goal type, but only occurs in an intermediate goal! There some ways to help with this of course such as documenting the rewrites using functions defined in where clauses, but this ends forcing the programmer to do tedious book-keeping (again, see below)

These functions show the range of entirely unreadable and entirely too verbose when using rewrite. Is there some happy middle for larger proofs using several equalities? We will look at Agda's equational reasoning in the next post and consider its relative merits.