In this post, I want to continue the series about programming with Agda, but before doing so, I want to put out the following disclaimer: I’m learning this subject on my own, having had no formal training in either computer programming or mathematics. Because of that, at times my reasoning for a proof may come across as too verbose and, perhaps, even condescending. But the verbosity is the result of how I explain things in my head to satisfy myself. Everything has to be made explicit before I can move on. There are already several tutorials on Agda on the web (and what I offer here is not really a tutorial) that are more concise and to the point. If you are proficient in functional programming or have had formal training in (pure) mathematics, you might find those tutorials easier to read. Nevertheless, I’m publishing these notes, first, to fix my understanding and, second, in case there’s someone out there that can derive some benefit from them, especially if they are in a situation similar to mine, where more details are needed to understand even the simplest of proofs. Lastly, be aware that there might be errors in the following!

A note about definition vs proof

Previously, we constructed the natural numbers using two constructors, namely, zero and suc. The former is a nullary function that takes no arguments and just returns itself as a constant, while the latter is a unary function that takes any natural number and returns its successor. In the beginning, we have no numbers for suc to construct. We only have zero, which in a weird sort of way we got for free. But once we have zero, then suc can give us its successor, which is \(1\). “Feeding” \(1\) back to suc gives us \(2\). And then we’re off into infinity, as suc gives us the successor of each new number we create.

We then learned how the function/operation of addition, _+_, can add two natural numbers. Leveraging what we learned in elementary school, we defined the addition of zero to any number \(n\) to be the same as just \(n\). (Equivalently, the term zero + n just is the term n.) Now, suppose we were in a class of first graders, and one of the students, hearing this, raised his hand and asked “but how do you know that zero plus any number is that same number? Why is it not any other number?” In other words, the child would be asking for a proof that zero + n = n. From what we have so far, no answer can be given, except to explain that this is a definition. We want it to be like that because to prove anything by induction, we need a base case, that is, a ground floor from which we will then raise our structure. To be sure, there is a proof, but it is a little too involved at this stage and, in any case, the proof, for practical purposes, is usually then turned back into a definitional equality: zero + n := n. So at this point, if the kid insists on a proof, we just tell him to lower his hand and shut up.

Currying

Another thing that perhaps might not have been clear is the different sorts of terms there are in type theory. Recall that we have atomic terms that cannot be broken down into simpler components. Examples, include the constant \(\mathtt{zero}: \mathbb{N}\), the number \(5 : \mathbb{N}\), and the successor function \(\mathtt{suc}: \mathbb{N \to N}\). But note that a function-term (or simply “function”), once it takes an argument, becomes a compound term. So, \(\mathtt{suc(zero)}\) is a compound term.

The operation of addition \(\_ + \_\) is another function-term. Specifically, a function of type \(\mathbb{N \to N \to N}\). Usually we say that it is a “binary” function, but strictly speaking, functions in type theory are always unary: they take a single argument. In the case of addition, once it takes a natural number as a first argument, it returns another unary function of type \(\mathbb{N\to N}\). This is called “currying”. This second function then takes a natural and returns another natural number.

Example. Say that \(\_ + \_\) takes the number \(3\), then it returns the function \(3 + \_\), whose type is \(\mathbb{N\to N}\). Think of this function as already having \(3\) in “memory”, so that whatever new argument it takes, it will add \(3\) to it. When \(3 + \_\) takes \(4\), it returns a compound term, namely, \(3 + 4\), whose type is \(\mathbb{N}\).

Monus

The next basic operation we would like to define is subtraction. Except that it can’t be the ordinary operation we all know for the simple reason that we are working within the natural numbers. Consider the operation \(3-5\). What is the output of this operation? Well, \(-2\), obviously. But \(-2\) is not a natural number. So this operation is ill-defined in the natural numbers system. Therefore, we’ll have to define a similar operation that does not take us outside of the natural numbers. The PLFA calls this operation “monus” (instead of “minus”) and denotes it with the symbol \(∸\). Its definition is as follows:

_∸_ : ℕ → ℕ → ℕ
m ∸ zero = m
zero ∸ suc n  = zero
suc m ∸ suc n = m ∸ n

The signature (the first line) tells us that the operation \(∸\) is a term of type \(\mathbb{N \to N \to N}\), that is, a function that takes a natural, returns another function of type \(\mathbb{N\to N}\), which takes a natural and, finally, returns another natural. To simplify, going forward we’ll treat \(∸\) as a binary function, with the understanding that this is not technically true.

Monus is defined on the basis of three cases (the three equations below the signature): 1) when the first argument is \(m\) (which is any number, including zero) and the second argument is zero, we define the result as being just \(m\) (remember, we are not proving anything yet!);¹ 2) when the first argument is zero but the second one is a successor (i.e., any number but zero), we define the result as being just zero. In other words, monus just returns the first argument. This allows us to stay within the natural numbers system. So if we have \(0 ∸ 5\), the answer is not \(-5\), but \(0\).

Finally, 3) when both arguments are successors, we define the result as being the same operation of monus but applied to the immediate predecessors of the arguments. This definition is recursive.

Example:

_ : 3 ∸ 2 ≡ 1
_ =
  begin
    3 ∸ 2
  ≡⟨⟩
    2 ∸ 1
  ≡⟨⟩
    1 ∸ 0
  ≡⟨⟩
    1
  ∎

Recall that \(3 ∸ 2 \equiv 1\) is an equality (or identity) type, which we can interpret as the proposition “3 monus 2 is equal to 1”. To prove the type-as-proposition, we need to construct or exhibit a term for it. If we can’t construct a term, then the type is empty, i.e., the proposition is false. Here we will use equational reasoning, where the term on the left of the \(\equiv\) symbol can be reduced (or matched) to the symbol on the right. If we can reduce \(3 ∸ 2\) to \(1\), then we show that the type \(3 ∸ 2 \equiv 1\) is the same as the type \(1 \equiv 1\), which is the equality type for which we always have a proof/term, i.e., refl.

So, the first line says that \(\_\) is the proof/term that we want to construct for the type \(3 ∸ 2 \equiv 1\). We do not care to give it a name, so we use the dummy symbol \(\_\).

The second line is where we show what the term \(\_\) is judgmentally equal to. If you recall from our discussion of addition, we could have shortened the proof considerably by simply writing:

_ : 3 ∸ 2 ≡ 1
_ = refl

…because for this simple operation we know that the reduction does indeed succeed. But since we want the reasoning to be explicit, we instead write out the reduction via equational reasoning, putting everything between the keyword begin and the QED symbol ∎.

So after the keyword begin, we write the term on the left of the \(\equiv\) symbol, which is \(3 ∸ 2\), and in each subsequent line we apply the definition of monus. Since \(3\) and \(2\) are successors, we apply the third case from the definition, which tells us that this is equivalent to monus applied to their immediate predecesors, i.e., \(2 ∸ 1\). Again, \(2\) and \(1\) are sucessors, so we apply the same reasoning, and get \(1 ∸ 0\). Now \(1\) is a successor, but \(0\) is not. Therefore, we apply the first case of the definition, which tells us that \(1 ∸ 0\) is the same as just \(1\). The term \(1\) cannot be reduced further. Thus the reduction of \(3 ∸ 2\) to \(1\) is finished, and the proof is complete, which we indicate by writing the symbol ∎.

What we have shown is that the type \(3 ∸ 2 \equiv 1\) is equivalent to \(1 \equiv 1\), which is always inhabited, meaning that the proposition “3 monus 2 is equal to 1” is true.

Multiplication

With addition and monus under our belt, we move on to define the operation of ordinary multiplication:

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

The definition has two cases: 1) the first argument is zero and the second argument is any number (including zero), and 2) the first argument is a successor (any number except zero) and the second is again any number. You’ll notice that the definition for the second case is not only recursive, but also based on addition. That is, multiplication is just repeated addition within the natural numbers. As the PLFA states: “Computing m * n returns the sum of m copies of n.”

Example. In the following we construct the inhabitant (or witness or proof) of the equality type \(2 \ast 1 ≡ 2\), which is constructed from the terms \(2\ast 1\) and \(2\):

_ : 2 ∗ 1 ≡ 2
_ =
  begin
  2 ∗ 1
  ≡⟨⟩
  1 + (1 ∗ 1)
  ≡⟨⟩
  1 + (1 + (1 ∗ 0))
  ≡⟨⟩
  1 + (1 + (0 + (0 ∗ 0)))
  ≡⟨⟩
  1 + (1 + (0 + 0))
  ≡⟨⟩
  2
  ∎

Again, the first line says that the term \(\_\) is the proof or inhabitant we are constructing. The second line is where we carry out our reasoning. To repeat, for this simple operation, we could have written

_ : 2 ∗ 1 ≡ 2
_ = refl

and be done with the proof, since it is quite obvious that \(2 \ast 1\) is indeed equal to \(2\). But once more we prefer to carry the proof in detail with equational reasoning.

Well, then, since the term \(2 \ast 1\) is composed of successors, we apply the second case of the definition, yielding \(1 + (1 \ast 1)\). This term still contains the second case of the definition inside the parenthesis, i.e., \(1 \ast 1\). Applying the definition again we get \(1 + (1 + (1 \ast 0))\). A further application results in \(1 + (1 + (0 + (0 \ast 0)))\). Now the innermost parenthesis has the base case, \(0 \ast 0\). Applying that part of the definition leaves us with \(1 + (1 + (0 + 0))\), and we have successfully reduced multiplication to addition. Mentally working out the operation of addition, we get that \(1 + (1 + (0 + 0))\) is just the number \(2\), and the proof ends.

However, if we wanted to, we could continue being explicit and reduce the term by applying the definition of addition:

_ : 2 ∗ 1 ≡ 2
_ =
  begin
  2 ∗ 1
  ≡⟨⟩
  1 + (1 ∗ 1)
  ≡⟨⟩
  1 + (1 + (1 ∗ 0))
  ≡⟨⟩
  1 + (1 + (0 + (0 ∗ 0)))
  ≡⟨⟩
  1 + (1 + (0 + 0))
  ≡⟨⟩ -- Applying the base case for addition yields:
  1 + (1 + 0)
  ≡⟨⟩ -- Applying the second case for addition, we have:
  1 + (suc (0 + 0))
  ≡⟨⟩ -- Applying again the base case:
  1 + (suc 0)
  ≡⟨⟩ -- Applying the second case for addition:
  suc 0 + suc 0
  ≡⟨⟩ -- Applying the second case yet again:
  suc (0 + (suc 0))
  ≡⟨⟩ -- Applying the base case one final time:
  suc (suc 0)
  ≡⟨⟩ -- which is the long way to write:
  2
  ∎

Exponentiation

The last operation we’re going to look at is exponentiation. Here’s the definition:

_^_ : ℕ → ℕ → ℕ
m ^ 0 = 1
m ^ (suc n) = m ∗ (m ^ n)

It tells us that exponentiation is just repeated multiplication in the natural numbers system.

Let’s use exponentiation to prove (construct a term) for the equality type \(3 ^\wedge 4 \equiv 81\). The reasoning should be familiar by now:

_ : 3 ^ 4 ≡ 81
_ =
  begin
  3 ^ 4
  ≡⟨⟩
  3 ∗ (3 ^ 3)
  ≡⟨⟩
  3 ∗ (3 ∗ (3 ^ 2))
  ≡⟨⟩
  3 ∗ (3 ∗ (3 ∗ (3 ^ 1)))
  ≡⟨⟩
  3 ∗ (3 ∗ (3 ∗ (3 ∗ (3 ^ 0))))
  ≡⟨⟩ -- We now reduce exponentiation to multiplication:
  3 ∗ (3 ∗ (3 ∗ (3 ∗ 1)))
  ≡⟨⟩
  3 ∗ (3 ∗ (3 ∗ 3))
  ≡⟨⟩
  3 ∗ (3 ∗ 9)
  ≡⟨⟩
  3 ∗ 27
  ≡⟨⟩
  81
  ∎

As you can imagine, once we reduced exponentiation to multiplication, we could then reduce multiplication to addition and then reduce addition to the “long form” of writing a natural number, but the process would be too long! Therefore, we content ourselves with just mentally working out that \(3 \ast 27\) is \(81\).