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.