Equational Reasoning vs rewrite in Agda: Equational reasoning

In my last post we explored how to use rewrite to reason about equations in Agda. We found that while rewrite can do quite a lot of the heavy lifting of manipulating equations, too much leads to unreadable code - the equalities are all tacit, meaning if a reader wants to follow along with the proof they would have to work out the types of the intermediate goals by hand. In this post we shall see that Agda's equational reasoning allows the programmer to write these intermediate goals explicitly and even use them to guide their proof.

The Agda standard library provides very useful functions and syntax for equational reasoning in module Relation.Binary.PropositionalEquality. The following import statements should bring the appropriate definitions into scope:

open import Relation.Binary.PropositionalEquality as PropEq
  using (_≡_; refl) renaming (cong to ≡-cong)
open PropEq.≡-Reasoning

Lets see how its used with the same example, proving the commutativity of addition.

 In our previous example, the second case of +-comm' only required one rewrite before finishing with refl. With equational reasoning, we will see that it is a little more verbose. We begin a block of equational reasoning with begin:

Woah! A little scary! The full goal type is given below. Fortunately, beginners such as myself don't need to worry about most of this - only the last couple
 of lines have the immediately relevant information. These lines tell us that to finish this proof we only need to show that suc (m + 0) ≡ suc m. (IsRelatedTo)

Every "chunk" of a block of equational reasoning consists of three parts: the current left hand side of the equation; a rule to apply, and the rest of the proof. These chunks can be broken up for you (and the first chunk automatically filled for you) by Agda. First type ? ≡⟨ ? ⟩ ? in the goal and use the "refine" command. Then, you can use the automatic search to fill the first goal. The result should be the following (after formatting):

Next, I provide the rule I want to use. In this case, I want to show that
suc (m + 0) ≡ suc m. I know how to show that m + 0 ≡ m, so in a sense I want to rewrite the equation under the application of suc on both sides. rewrite did that for us automatically, but when using equational reasoning we need to use  ≡-cong, specifying the structure we want to undo in a lambda as a first argument and the rule we wish to apply in the second.

And after all that, we have our proof. To finish:

This case of the proof is significantly more verbose that using rewrite and has a much steeper learning curve, and it's arguably less readable as well. However, it has the potential to scale, and additionally working on the right hand side of the equation allows us to use the information from multiple goals to write our proofs.

Lets continue with the next case in our proof.

 I can tell that I will finish the proof if, again, I just manipulate everything under the application of suc, but I am also sure that I won't be able to do it in a single step. Thankfully, there is nothing stopping me from nesting another block of equational reasoning.

So far so good. At this point, I realize that I will need a separate lemma (like last time) to finish, so I sketch out what using the lemma should look like:

And of course this proof follows much like the one from last time

Now finishing the proof using more equational reasoning:

A little verbose but very readable, I'd say, and not nearly as verbose as labeling the transformations on the equations using lemmas.

One weakness I see is that unlike rewrite, equational reasoning does not seem to easily support manipulating both sides of the equation. You need only compare the definitions +-comm'-under-sr in this and the last post - the previous post used two rewrites to deal with an intermediate goal suc m + suc n ≡ suc n + suc m before finishing, whereas in this proof it occurs in the middle. This may seem like a small complaint, but for more complicated equations I can imagine it might be conceptually easier to massage both ends of an equation to a provable goal than forcing the programmer to march left to right.

That said, it is certainly more readable and offers the programmer more guidance along the way than with using rewrites as much of the information outside of the angle brackets can be inferred by Agda. All in all I would say, use rewrite sparingly - it's a neat syntactic sugar useful in very small equational manipulations. Very complicated equational manipulations should use the features of ≡-Reasoning.

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.