Associativity, Identity, and Commtativity

We’ve constructed the natural numbers, defined operations on them, and proved some equalities. Now we’re going to prove some properties of the operators: associativity and commutativity. (This entry corresponds to chapter 2 of PLFA.)

Associativity

If you recall, all functions in type theory are unary, but we treat them as binary for the sake of convenience. What do we do when we want to add three numbers, though, like in \(3 + 4 + 5\)? In school we were taught to use parentheses— e.g. \(3 + (4 + 5)\)—in order to perform the addition in two steps: First, we add \(4\) and \(5\), then we add \(3\) to the result. But there’s another way to look at this: the outer \(+\) operator takes the term \(3\) as first argument and the term \(4 + 5\) as second argument. The latter is itself a complex term: the result of applying the operator \(+\) to \(4\) and \(5\).

Another thing we were told in school is that the following usage of the parentheses yields the same result: \((3 + 4) + 5\). Now the outer operator takes the term \((3 + 4)\) as first argument and \(5\) as second argument. This property is called associativity, and we can express the equivalence of both ways of ordering the parentheses as an equality type: \((m + n) + p ≡ m + (n + p)\).

In Agda, we can prove the particular case \((3 + 4) + 5 ≡ 3 + (4 + 5)\) using equational reasoning:

_ : (3 + 4) + 5 ≡ 3 + (4 + 5)
_ =
  begin
    (3 + 4) + 5
  ≡⟨⟩
    7 + 5
  ≡⟨⟩
    12  -- both terms reduce to this
  ≡⟨⟩
    3 + 9
  ≡⟨⟩
    3 + (4 + 5)
  ∎

In this example, the reasoning is a little different from what we’ve seen before. After the keyword begin, we write the term to the left of the \(\equiv\) sign, \((3 + 4) + 5\), and then compute the value \(12\) straightforwardly as we would do with pen and paper, that is, without going through the formal definition of addition and without using the “long form” of the natural numbers as we did in the past.¹

Now, you’ll notice something else is different in this example of equational reasoning: Before, the term to the left of the \(\equiv\) sign was complex, but the term on the right side was atomic, and our task was to reduce the complex term to the atomic one. In this case, the terms on either side of the \(\equiv\) sign are complex. So the reduction of both complex terms terminates in the middle. Here \((3 + 4) + 5\) and \(3 + (4 + 5)\) reduce to \(12\). As before, this means that the equality type \((3 + 4) + 5 ≡ 3 + (4 + 5)\) is equivalent to the type \(12 ≡ 12\) (which always has a term/proof, namely, \(\mathtt{refl}\)). And so we’ve shown that the placement of the parentheses indeed does not matter!

But we want to give a general proof of this; that is, we want to show that this is true for any natural numbers \(m, n,\) and \(p\).

We do this by defining a new constructor that takes \(m, n,\) and \(p\), and returns a term/proof of the equality type/proposition \((m + n) + p ≡ m + (n + p)\). We give this function the name \(+\text{-}\mathrm{assoc}\):

+-assoc : ∀ (m n p : ℕ) → (m + n) + p ≡ m + (n + p)

The signature states that when \(+\text{-}\mathrm{assoc}\) takes any three natural numbers, it returns the term \(+\text{-}\mathrm{assoc}\, m\, n\, p\) whose type is \((m + n) + p ≡ m + (n + p)\). In other words, \(+\text{-}\mathrm{assoc}\, m\, n\, p\) is the proof of the proposition \((m + n) + p ≡ m + (n + p)\). We now show that this works as expected.

We use induction on the first variable \(m\), meaning that we show how to construct, first, the term \(+\text{-}\mathrm{assoc \, zero}\, n\, p\), then we “assume” to have the term \(+\text{-}\mathrm{assoc}\, m\, n\, p\), and, finally, we construct the term \(+\text{-}\mathrm{assoc \, suc}\, m\, n\, p\). (The reason for putting the word “assume” in quotation marks will become clear shortly.)

First the base case, where \(m\) is \(\mathrm{zero}\), and the term \(+\text{-}\mathrm{assoc \, zero}\, n\, p\) is proof of the equality type \((\mathrm{zero} + n) + p \equiv \mathrm{zero} + (n + p)\):

+-assoc zero n p =
  begin
    (zero + n) + p
  ≡⟨⟩
    n + p
  ≡⟨⟩
    zero + (n + p)
  ∎

Recall from the definition of addition that the term \(\mathrm{zero} + n\) is the same as \(n\). So the complex term \((\mathrm{zero} + n) + p\) reduces to just \(n + p\). For the same reason, the term \(\mathrm{zero} + (n + p)\) reduces to \(n + p\). Since both complex terms reduce to the same, it follows that the type \((\mathrm{zero} + n) + p ≡ \mathrm{zero} + (n + p)\) is equivalent to \(n + p ≡ n + p\), which as you might guess is always inhabited by \(\mathtt{refl}\). So our construction of \(+\text{-}\mathrm{assoc\, zero}\, n\, p\) is successful.

The middle step in mathematical induction is called the inductive hypothesis. After proving the base case, we “assume” that we have the term \(+\text{-}\mathrm{assoc}\, m\, n\, p\), which proves the type \((m + n) + p ≡ m + (n + p)\).

Next is the inductive step, where we construct the term \(+\text{-}\mathrm{assoc\, (suc}\, m)\, n\, p\), which proves the type \((\mathrm{suc}\, m + n) + p ≡ \mathrm{suc}\, m + (n + p)\):

+-assoc (suc m) n p =
  begin
    (suc m + n) + p -- line 1
  ≡⟨⟩
    suc (m + n) + p -- line 2
  ≡⟨⟩
    suc ((m + n) + p) -- line 3
  ≡⟨ cong suc (+-assoc m n p) ⟩ -- justification
    suc (m + (n + p)) -- line 4
  ≡⟨⟩
    suc m + (n + p) -- line 5
  ∎

Note how applying the rules of addition we can reduce the complex term \((\mathrm{suc}, m + n) + p\) (line 1) to \(\mathrm{suc}\, ((m + n) + p)\) (line 3), while \(\mathrm{suc}\, m + (n + p)\) (line 5) reduces to \(\mathrm{suc}, (m + (n + p))\) (line 4). These two reductions on lines 3 and 4, however, cannot be further simplified following the rules of addition, and it is clear that they do not match in their parentheses. And if two terms do not match, they are presumably not equivalent. So, what to do?

Well, let’s see: the terms \(\mathrm{suc}\, ((m + n) + p)\) and \(\mathrm{suc}\, (m + (n + p))\) contain the terms \((m + n) + p\) and \(m + (n + p)\).² These two terms also do not match in their parentheses, so, presumably, they are also not equivalent… But wait! Our inductive hypothesis says that they are equivalent! And the proof of their equivalence is the term \(\mathrm{\text{+-}assoc}\, m\, n\, p\).

So now the only thing left to do is to add back \(\mathrm{suc}\) to these equivalent terms, and we will have proved the inductive step. Can we do that?

Yes! We simply have to invoke congruence! A congruence relation is an equivalence relation on an algebraic structure (in our case, the structure of natural numbers with addition), such that when we apply an algebraic operation to equivalent terms the equivalence is preserved. Since the inductive hypothesis tells us that \((m + n) + p\) and \(m + (n + p)\) are equivalent, then applying the successor operation, \(\mathrm{suc}\), to both yields the equivalent terms \(\mathrm{suc}((m + n) + p)\) (line 3) and \(\mathrm{suc}(m + (n + p))\) (line 4).³

To complete the proof in Agda, we write these justifications in between the angled brackets—that is, invoking the term \(\mathrm{\text{+-}assoc}\, m\, n\, p\) and the fact that adding \(\mathrm{suc}\) to it preserves the equivalence because of congruence (note the keyword cong). This tells Agda what our justification is for considering the irreducible terms \(\mathrm{suc}\, ((m + n) + p)\) and \(\mathrm{suc}\, (m + (n + p))\) as being equivalent.

We have proved that the property of associativity holds for the base case of \(\mathrm{zero}\), and for the inductive case \(\mathrm{suc}\, m\) (on the basis that it holds for \(m\)). Therefore, we have proved that associativity holds for all natural numbers!

Commutativity

Another property of addition is that it does not matter whether the first and second arguments of the addition operator, \(\_ + \_\), are exchanged; the result is the same. In other words, the proposition \(m + n \equiv n + m\) is true. To prove it (equivalently, to construct a term of this type), we define a new function, \(+\text{-}\mathtt{comm}\), that takes two naturals, \(m\) and \(n\), and returns the term/proof \(+\text{-}\mathtt{comm}\, m\, n\):

+-comm : ∀ (m n : ℕ) → m + n ≡ n + m

We use induction on the second variable \(n\). First the base case, where \(n\) is \(\mathtt{zero}\), and the term we are constructing via equational reasoning is \(+\text{-}\mathtt{comm}\, m\, \mathtt{zero}: m + \mathtt{zero} \equiv \mathtt{zero} + m\):

+-comm m zero =
  begin
    m + zero
  ≡⟨⟩ -- Uh oh!
    m
  ≡⟨⟩
    zero + m
  ∎

If you put the above code into your Agda file, it won’t compile! You and I both know that this should work, so what gives? The reason Agda returns an error is that it doesn’t know that \(m + \mathtt{zero}\) can be reduced to just \(m\). Looking back at the definition of addition, we have that \(\mathtt{zero} + m\) does reduce by definition to \(m\). However, the string \(m + \mathtt{zero}\) does not match the definition; the order of the arguments is different. How can we make them match? Answer: by proving the proposition (type) \(m + \mathtt{zero} \equiv m\), for any \(m\).

This states that \(\mathtt{zero}\) is a “right-identity”, i.e., that when \(\mathtt{zero}\) is to the right of the addition operator, the term \(m + \mathtt{zero}\) is judgmentally the same as whatever is on the left of the operator, i.e., \(m\). Therefore, before proving commutativity, we need to prove the right-identity property of \(\mathtt{zero}\) (with respect to addition) as a lemma. We do so with a new function, call it \(+\text{-}\mathtt{identity}^r\), that takes any natural \(m\) and returns a term of the type/proposition \(m + \mathtt{zero} \equiv m\):

+-identityʳ : ∀ (m : ℕ) → m + zero ≡ m

This proof is also carried out via induction. We begin with the base case, where \(m\) is \(\mathtt{zero}\):

+-identityʳ zero =
  begin
    zero + zero
  ≡⟨⟩
    zero
  ∎

Then, following the logic of the proof of associativity, we prove the inductive step by a recursive invocation of the inductive hypothesis and the relation of congruence:

+-identityʳ (suc m) =
  begin
    suc m + zero
  ≡⟨⟩
    suc (m + zero)
  ≡⟨ cong suc (+-identityʳ m) ⟩  -- justification
    suc m
  ∎

And that’s it for the lemma. Having proved the right identity of \(\mathtt{zero}\), we can now prove the base case of commutativity:

+-comm m zero =
  begin
    m + zero
  ≡⟨ +-identityʳ m ⟩ -- this allows reducing the above to:
    m
  ≡⟨⟩
    zero + m
  ∎

The only thing left to do to prove commutativity in general is to prove the inductive step. But here we face another problem. The Agda code should look something like this:

+-comm m (suc n) =
  begin
    m + suc n
  ≡⟨⟩  -- Uh oh!
    suc (m + n)
  ≡⟨ cong suc (+-comm m n) ⟩
    suc (n + m)
  ≡⟨⟩
    suc n + m
  ∎

Again the problem is that we do not have a rule to match \(m + \mathtt{suc}\, n\) with \(\mathtt{suc} (m + n)\). That is, we now need to prove the lemma \(m + \mathtt{suc}\, n ≡ \mathtt{suc} (m + n)\). As before, we define a new function, call it \(+\text{-}\mathtt{suc}\), that takes any two natural numbers \(m\) and \(n\), and returns a term of the type/proposition \(m + \mathtt{suc}\, n ≡ \mathtt{suc} (m + n)\):

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

This, yet again, requires induction. I’ll spare you the details (since by now the reasoning should be familiar), and just provide the Agda code for the proof. First, the base case:

+-suc zero n =
  begin
    zero + suc n
  ≡⟨⟩
    suc n  -- by addition, the lines above and below reduce to this
  ≡⟨⟩
    suc (zero + n)
  ∎

Then the inductive step:

+-suc (suc m) n =
  begin
    suc m + suc n
  ≡⟨⟩
    suc (m + suc n)
  ≡⟨ cong suc (+-suc m n) ⟩  -- recursive invocation and congruence
    suc (suc (m + n))
  ≡⟨⟩
    suc (suc m + n)
  ∎

With this second lemma proved, we can finally prove the inductive step of commutativity:

+-comm m (suc n) =
  begin
    m + suc n
  ≡⟨ +-suc m n ⟩  -- 2nd lemma, which reduces the above to:
    suc (m + n)
  ≡⟨ cong suc (+-comm m n) ⟩ -- recursive invocation and congruence
    suc (n + m)
  ≡⟨⟩
    suc n + m
  ∎

If you got a little lost, don’t worry. I was too at first. Just take a moment, go over the code and, to use a common phrase from math textbooks, “try to convince yourself” that the reasoning is correct. This happened to me a lot while going through the PLFA tutorial. Many times I would have to go back to chapter 1 for review and find that I had missed something crucial.

More details could be given, for example, by showing how each of the terms we’ve constructed is equal to \(\mathtt{refl}\), but this post is already too long, and we need to start economizing on words as the proofs become more and more elaborate.

In the next entry, we’ll tackle relations.