5 Induction

\(\newcommand{\la}{\lambda} \newcommand{\Ga}{\Gamma} \newcommand{\ra}{\rightarrow} \newcommand{\Ra}{\Rightarrow} \newcommand{\La}{\Leftarrow} \newcommand{\tl}{\triangleleft} \newcommand{\ir}[3]{\displaystyle\frac{#2}{#3}~{\textstyle #1}}\)

This chapter introduces a central proof technique in mathematics. We saw it briefly in the demo chapter, applied to a theorem about list append. In Agda a proof by induction is a recursive function.

5.1 Properties of operators

PLFA starts by discussing possible properties of operators, all of which hold for addition: commutativity, associativity, distributivity (a property of two operators), and identity (a property of a value with respect to an operator). We tend to take these for granted, rearranging and regrouping numbers to be added almost without thinking about it. But if we look at the definition of addition from the previous chapter, we can see that it is not symmetric, so it is not obvious that, for example, when the arguments are switched, the result remains the same.

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

You won’t see this code in the Agda files for this chapter (PLFA and local), because it’s imported from the Agda standard library.

For our first theorem on properties of addition, we’ll prove that zero is the left identity for addition. I’m working in a slightly different order from PLFA.

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

This theorem can be proved without induction, because Agda can computationally reduce zero + m to m (this is the first equation in the definition of addition). So the goal becomes m ≡ m.

+-identityᴸ : ∀ (m : ℕ) → zero + m ≡ m
+-identityᴸ m = refl

But right identity is not so simple. These two theorems should remind you of the demo chapter, where we proved that the empty list was the left and right identity for list append.

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

As discussed quickly in the demo chapter, a for-all type is a dependently-typed function. The ∀ character in something like ∀ (n : ℕ) can actually be omitted; it is the name n, annotated by its type ℕ, that signifies the use of a dependent type. We’ll keep the ∀s for readability. We develop this function as we developed addition, by a case split on its argument.

This chapter of PLFA introduces the most useful interactive commands added by Agda mode. You may have seen some of these in the command log displayed at the right of asciicast windows in earlier chapters.

C-c C-l (load the Agda file and make holes active)
C-c C-f and C-c C-b (forward to next hole, back to previous hole)
C-c C-, (information about goal and context when in a hole)
C-c C-c (case-split in a hole)
C-c C-r (refine in a hole)
C-c C-SPC (completely fill a hole)

These cover the bulk of what we need to develop code. We will learn nuances of these, and a few more commands, as we go. A complete list can be found in the Agda documentation or by getting Emacs to describe Agda mode. To be honest, I am not sure what some of the available commands do.

+-identityʳ : ∀ (m : ℕ) → m + zero ≡ m
+-identityʳ m = {!!}

Putting m in the hole and case-splitting, we get:

+-identityʳ : ∀ (m : ℕ) → m + zero ≡ m
+-identityʳ zero = {!!}
+-identityʳ (suc m) = {!!}

The goal in the first hole (the type of what must be provided) should be, by direct substitution, zero + zero ≡ zero, but Agda computationally reduces the left-hand side, which matches the pattern in the first definitional equation for addition. This makes the goal zero ≡ zero, which can be proved with refl, the constructor for equality types.

The remaining equation covers the case where the argument of +-identityʳ is of the form suc m. Previously we used m to stand for the argument, but that is no longer the case. Agda’s automatic reuse of names in this fashion can be confusing at first. But since this is just a pattern introducing a name, you can change m to m′, if you wish.

The goal, by substitution, should be (suc m) + zero ≡ (suc m). But the left-hand side matches the pattern in the second definitional equation for addition, and Agda reduces the goal to suc (m + zero) ≡ suc m. The recursive application of the function +-identityʳ m has type m + zero ≡ m, and as we saw in the demo chapter, we can use Agda’s rewrite syntax to rewrite our goal using this equation. After doing this edit, which takes place outside a hole, we must reload the file in order to get Agda to take it into account.

+-identityʳ : ∀ (m : ℕ) → m + zero ≡ m
+-identityʳ zero = refl
+-identityʳ (suc m) rewrite +-identityʳ m = {!!}

The goal has become suc m ≡ suc m, which can be proved with refl.

+-identityʳ : ∀ (m : ℕ) → m + zero ≡ m
+-identityʳ zero = refl
+-identityʳ (suc m) rewrite +-identityʳ m = refl

PLFA uses syntax for equational reasoning to display the computation steps that are hidden in the proofs we have just developed. The big advantage of equational reasoning is that it is readable. This, I believe, is the main reason it was chosen for PLFA. It can be useful when a proof puts together chains of equations, or when one has developed an idea on paper. But it is less natural to develop interactively, and it is definitely more verbose, meaning it takes longer to type. I will use rewrite where possible.

Whether or not you use equational reasoning in assignments is up to you. There are times when it may help you to carry out a development. And if you are not sure how a more terse development works, you can try to rewrite it equationally if it is handling a situation for which equational reasoning helps.

Our use of rewrite is not without its costs. When reading the completed code, you mostly can’t see what the current state of the goal was when the rewrite was done, or the equation that rewrite is using, or the result of the rewrite. You can only see these things if you erase the rewrite and then redo it interactively. Another issue, which you may encounter in your own work, is that rewrite is convenient syntax (or "syntactic sugar") for more verbose boilerplate generated behind the scenes. This automatic generation can fail in complex situations.

This chapter of PLFA does introduce rewrite further down, but it doesn’t use it at first. Instead of rewriting a subexpression using an equation, it "wraps" each side of the equation in the same context using a theorem from the standard library called cong. This theorem takes an equation such as x ≡ y and a transformation f, and "lifts" the equation to f x ≡ f y. In particular, the recursive application +-identityʳ m, which has type m + zero ≡ m, can be lifted to suc (m + zero) ≡ suc m by supplying suc as the transformation f. Here’s what the proof would look like.

+-identityʳ′ : ∀ (m : ℕ) → m + zero ≡ m
+-identityʳ′ zero = refl
+-identityʳ′ (suc m) = cong suc (+-identityʳ′ m)

It’s important to realize that the ′ character in the name of the last theorem (usually pronounced "prime" in mathematics and used to denote an alternate) is not the apostrophe character ’ found on a standard keyboard, but the Unicode PRIME character, obtained in Emacs by typing \’. This is one of the drawbacks of working with Unicode; there can be very subtle visual differences between different characters. You may find yourself frustrated because Agda cannot find something, because you think you have spelled it right, but you have used a different character that looks almost identical to the one in the definition. Keep this in mind when reading Agda code here or in the standard library.

5.2 Associativity

This is the first proof by induction/recursion in PLFA, first done with equational reasoning, and later using rewrite.

5.3 Commutativity

The helper function +-suc is useful for other situations as well. Keep it in mind as we proceed.

5.4 Building proofs interactively

We covered this material earlier, just above. I put in this section header because there isn’t another in PLFA just before a number of exercises that end the chapter. Most of these I have asked you to do for credit, starting from the "completed" version of the local file. At the very end, we have the second appearance of binary notation, since now we can prove some things about it. I have added a bit more structure than provided in PLFA, and I will also reschedule where later work building on this is done. I like these exercises a lot, and I hope you will also.

The techniques learned in this chapter will work on the list examples in the demo chapter, and you can try them out if you are interested. For example, you can show that list append is associative. PLFA covers lists much later on, and it is tempting to move that material up, but let’s stick to the script.

The computational reduction that Agda does can make proofs more compact, but as we’ve seen, asymmetry in definitional equations can lead to asymmetry in computation. Sometimes we arrive at a situation where, with our algebraic training, we can see that the left-hand and right-hand sides of an equation can be made equal, but we have a long series of rearrangements to spell out to convince Agda. Automating such situations so that only "good" rewrites are done and not "bad" ones that take us further from our particular goal is the subject of active research.