Equational Reasoning

If you follow the PLFA tutorial on which these notes are based, you will recall that one of the imports for defining addition in Agda is a special module called ≡-Reasoning that allows us to use chains of equations in a proof. These work much like when we use pen and paper to prove, via explicit intermediary steps, how one mathematical object is the same as another. In such proofs, we frequently give the justification for an inference between parentheses on the right margin. Now that we’ve defined equality (the Martin Löf kind), we get to also define the equational reasoning environment in Agda for ourselves.

module ≡-Reasoning {A : Set} where

  infix  1 begin_
  infixr 2 step-≡-∣ step-≡-⟩
  infix  3 _∎

  begin_ : ∀ {x y : A} → x ≡ y → x ≡ y
  begin x≡y  =  x≡y

  step-≡-∣ : ∀ (x : A) {y : A} → x ≡ y → x ≡ y
  step-≡-∣ x x≡y  =  x≡y

  step-≡-⟩ : ∀ (x : A) {y z : A} → y ≡ z → x ≡ y → x ≡ z
  step-≡-⟩ x y≡z x≡y  =  trans x≡y y≡z

  syntax step-≡-∣ x x≡y      =  x ≡⟨⟩ x≡y
  syntax step-≡-⟩ x y≡z x≡y  =  x ≡⟨  x≡y ⟩ y≡z

  _∎ : ∀ (x : A) → x ≡ x
  x ∎  =  refl

open ≡-Reasoning

The first thing to note is that begin_, step-≡-∣, step-≡-⟩, and _∎ are all functions taking proofs of equalities. When we use pen and paper, we do not bother to write begin to indicate where the proof starts, although we do (sometimes) write the QED symbol, \(\blacksquare\), to signal the end of a proof. The reason is that we think of these things as not being relevant to the proof. But in Agda, they are, as I said, functions, so they must be defined.

The begin_ function marks the beginning of the chain, and is placed after the judgmental or definitional equality symbol \(=\) (we’ll see an example shortly). It takes as a single argument the output of the rest of the chain. What it does with the argument is simply return it, meaning that it’s purely cosmetic.

The step-≡-∣ function, you’ll notice, is almost the same as begin_, except that it has an explicit argument.

The step-≡-⟩ function is similar to the \(\mathtt{trans}\) function that we defined in a previous entry, except that one of the implicit arguments is made explicit and the order of the equality types is changed. So whereas trans x≡y y≡z is a term/proof of x≡z, in the case of step-≡-⟩ the same term/proof is step-≡-⟩ x y≡z x≡y. This appears to be purely for technical reasons: it makes Agda’s type inference more efficient.

The lines beginning with the keyword syntax allow us to re-write the application of the previous functions. So, for example, instead of writing step-≡-∣ x x≡y, we can write x ≡⟨⟩ x≡y (like infix notation). Likewise, instead of writing step-≡-⟩ x y≡z x≡y, we can now write x ≡⟨ x≡y ⟩ y≡z, where the angled brackets contain the justification of an inference. In short, we’ve re-written step-≡-∣ and step-≡-⟩, so that now they are of the form _≡⟨_⟩_, where the space between the brackets may or may not be filled (depending on whether a justification is warranted).

Finally, we have the function _∎, which takes an explicit argument, a term \(x\) of some type \(A\), and returns a proof of \(x\equiv_A x\), which is (as you’ve probably heard) \(\mathtt{refl}\).

First example

trans′ : ∀ {A : Set} {x y z : A} → x ≡ y → y ≡ z → x ≡ z
trans′ {A} {x} {y} {z} x≡y y≡z =
  begin
    x
  ≡⟨ x≡y ⟩
    y
  ≡⟨ y≡z ⟩
    z
  ∎

The first line is the signature. The second line gives us the output of \(\mathtt{trans}'\) once it takes all of its arguments, which, by currying, we can see is a term of \(x \equiv z\):

\[\begin{align*} \mathtt{trans}'\ \{A\} \{x\} \{y\} \{z\} &: x \equiv y \to y \equiv z \to x \equiv z \\ \mathtt{trans}'\ \{A\} \{x\} \{y\} \{z\}\ x\!\equiv\! y &: y \equiv z \to x \equiv z \\ \mathtt{trans}'\ \{A\} \{x\} \{y\} \{z\}\ x\!\equiv\! y\ y\!\equiv\! z &: x \equiv z \end{align*}\]

But what does that term evaluate to? That is given by the equational chain following the judgmental equality symbol \(=\).

It all begins with… \(\mathtt{begin}\). It takes as its only argument the output of the rest of the chain, i.e., \(x \equiv\!\langle\ x\!\equiv\! y\ \rangle \big(y \equiv\!\langle\ y\!\equiv\! z\ \rangle (z\ \blacksquare)\big)\), and then simply returns it. (Note that there is no spacing in \(x\!\equiv\! y\) and \(y\!\equiv\! z\), meaning that, by convention, these are considered terms of the types \(x \equiv y\) and \(y \equiv z\), respectively.)

The first nested function is \(\_\equiv\!\langle\_\rangle\_\) with arguments \(x\), \(x\!\equiv\! y\), and \(\big(y \equiv\!\langle\ y\!\equiv\! z\ \rangle (z\ \blacksquare)\big)\). This last argument is, in turn, the output of another \(\_\equiv\!\langle\_\rangle\_\) function, with arguments \(y\), \(y\!\equiv\! z\), and \(z\ \blacksquare\). And, again, the last term is the output of \(\_\blacksquare\), with \(z\) as argument.

Having parsed the code, we now go in reverse order to evaluate. The innermost \(z\ \blacksquare\) is a proof of \(z \equiv z\), and so it must be \(\mathtt{refl}\). This means that the second \(\_\equiv\langle\_\rangle\_\) takes \(y\), \(y\!\equiv\! z\) and that \(\mathtt{refl}\) and, according to its definition, is equal to \(\mathtt{trans'\ refl}\ y\!\equiv\! z\), where \(y\!\equiv\! z\) and \(\mathtt{refl}\) have now exchanged places. But \(\mathtt{trans'\ refl}\ y\!\equiv\! z\) is equal to a term of the type \(y \equiv z\). Let’s call it \(y\! \equiv\! z\) as well. The outermost \(\_\equiv\langle\_\rangle\_\) takes \(x\), \(x\!\equiv\! y\) and the term we just got in the previous step, i.e. \(y\!\equiv\! z\). So we now have \(x \equiv\!\langle\ x\!\equiv\! y\ \rangle\ y\!\equiv\! z\), which is the same as \(\mathtt{trans}'\ y\!\equiv\! z\ x\!\equiv\! y\), with the last two arguments trading places. But now this matches the last curried line of \(\mathtt{trans}'\), with implicit arguments omitted. Therefore, \(\mathtt{trans}'\ y\!\equiv\! z\ x\!\equiv\! y\) is a term of \(x \equiv z\), as required.

In simpler words, the chain is telling us that, given some \(x\), if \(x\) is the same as \(y\), then we can infer \(y\), and if \(y\) is the same as \(z\), then we can infer \(z\). So, starting from \(x\) we can conclude \(z\), i.e., we have a proof of \(x \equiv z\).

Second example

We now turn to an example of equational reasoning that we used before. We’ll prove the commutativity of addition again.

As before, we first declare the \(\mathbb{N}\) datatype with its constructors \(\mathtt{zero}\) and \(\mathtt{suc}\), and then the addition operator \(\_+\_\):

data ℕ : Set where
  zero : ℕ
  suc  : ℕ → ℕ

_+_ : ℕ → ℕ → ℕ
zero    + n  =  n
(suc m) + n  =  suc (m + n)

If you recall, to define the \(+\text{-}\mathtt{comm}\) function by which we prove commutativity we first needed to prove the “right-identity” of \(\mathtt{zero}\) for the base case. For the inductive step, we also needed to prove that \(m + \mathtt{suc}\ n\) is the same as \(\mathtt{suc}(m + n)\). Here, instead of going through the proofs again, we make them postulates:

postulate
  +-identity : ∀ (m : ℕ) → m + zero ≡ m
  +-suc : ∀ (m n : ℕ) → m + suc n ≡ suc (m + n)

+-comm : ∀ (m n : ℕ) → m + n ≡ n + m
+-comm m zero =
  begin
    m + zero
  ≡⟨ +-identity m ⟩
    m
  ≡⟨⟩
    zero + m
  ∎

That is, given \(m + \mathtt{zero}\), by the postulated \(+\text{-}\mathtt{identity}\ m\), we can infer \(m\). And given \(m\), we can infer \(\mathtt{zero} + m\), no justification needed (empty angled brackets) because that is the definition for \(\mathtt{zero}\).

Given \(m + \mathtt{suc}\ n\), by the postulated \(+\text{-}\mathtt{suc}\ m\ n\) (proof that \(m + \mathtt{suc}\ n\) is the same as \(\mathtt{suc} (m +n)\)), we can infer \(\mathtt{suc}\ (m + n)\). Then, given \(\mathtt{suc}\ (m + n)\), by the inductive hypothesis \(+\text{-}\mathtt{comm}\ m\ n\) and congruence (i.e., that since \(m+n\) is the same as \(n+m\), then \(\mathtt{suc}\) applied to the former is the same as \(\mathtt{suc}\) applied to the latter), we can infer \(\mathtt{suc}\ (n + m)\). And from this we can conclude \(\mathtt{suc}\ n + m\), no justification needed (empty angled brackets) because we’re merely omitting parentheses.

In simpler terms, the equational reasoning has allowed us to infer \(\mathtt{zero} + m\) from \(m + \mathtt{zero}\), and \(\mathtt{suc}\ n + m\) from \(n + \mathtt{suc}\ m\). This means that, for any natural numbers \(m\) and \(n\), we can infer \(n + m\) from \(m + n\), and this is proof of the identity type \(m + n \equiv n + m\), quod erat demonstrandum.