module plfa.part1.Induction where

Induction makes you feel guilty for getting something out of nothing … but it is one of the greatest ideas of civilization. – Herbert Wilf

Now that we’ve defined the naturals and operations upon them, our next step is to learn how to prove properties that they satisfy. As hinted by their name, properties of inductive datatypes are proved by induction.

Imports

We require equality as in the previous chapter, plus the naturals and some operations upon them. We also require a couple of new operations, cong, sym, _≡⟨⟩_ and _≡⟨_⟩_, which are explained below:
import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; cong; sym)
open Eq.≡-Reasoning using (begin_; step-≡-∣; step-≡-⟩; _∎)
open import Data.Nat using (ℕ; zero; suc; _+_; _*_; _∸_; _^_)

(Importing step-≡-∣ defines _≡⟨⟩_ and importing step-≡-⟩ defines _≡⟨_⟩_.)

Properties of operators

Operators pop up all the time, and mathematicians have agreed on names for some of the most common properties.

  • Identity. Operator + has left identity 0 if 0 + n ≡ n, and right identity 0 if n + 0 ≡ n, for all n. A value that is both a left and right identity is just called an identity. Identity is also sometimes called unit.

  • Associativity. Operator + is associative if the location of parentheses does not matter: (m + n) + p ≡ m + (n + p), for all m, n, and p.

  • Commutativity. Operator + is commutative if order of arguments does not matter: m + n ≡ n + m, for all m and n.

  • Distributivity. Operator * distributes over operator + from the left if m * (p + q) ≡ (m * p) + (m * q), for all m, p, and q, and from the right if (m + n) * p ≡ (m * p) + (n * p), for all m, n, and p.

Addition has identity 0 and multiplication has identity 1; addition and multiplication are both associative and commutative; and multiplication distributes over addition.

If you ever bump into an operator at a party, you now know how to make small talk, by asking whether it has a unit and is associative or commutative. If you bump into two operators, you might ask them if one distributes over the other.

Less frivolously, if you ever bump into an operator while reading a technical paper, this gives you a way to orient yourself, by checking whether or not it has an identity, is associative or commutative, or distributes over another operator. A careful author will often call out these properties—or their lack—for instance by pointing out that a newly introduced operator is associative but not commutative.

Exercise operators (practice)

Give another example of a pair of operators that have an identity and are associative, commutative, and distribute over one another. (You do not have to prove these properties.)

Give an example of an operator that has an identity and is associative but is not commutative. (You do not have to prove these properties.)

Associativity

One property of addition is that it is associative, that is, that the location of the parentheses does not matter:

(m + n) + p ≡ m + (n + p)

Here m, n, and p are variables that range over all natural numbers.

We can test the proposition by choosing specific numbers for the three variables:
_ : (3 + 4) + 5 ≡ 3 + (4 + 5)
_ =
  begin
    (3 + 4) + 5
  ≡⟨⟩
    7 + 5
  ≡⟨⟩
    12
  ≡⟨⟩
    3 + 9
  ≡⟨⟩
    3 + (4 + 5)
  ∎

Here we have displayed the computation as a chain of equations, one term to a line. It is often easiest to read such chains from the top down until one reaches the simplest term (in this case, 12), and then from the bottom up until one reaches the same term.

The test reveals that associativity is perhaps not as obvious as first it appears. Why should 7 + 5 be the same as 3 + 9? We might want to gather more evidence, testing the proposition by choosing other numbers. But—since there are an infinite number of naturals—testing can never be complete. Is there any way we can be sure that associativity holds for all the natural numbers?

The answer is yes! We can prove a property holds for all naturals using proof by induction.

Proof by induction

Recall the definition of natural numbers consists of a base case which tells us that zero is a natural, and an inductive case which tells us that if m is a natural then suc m is also a natural.

Proof by induction follows the structure of this definition. To prove a property of natural numbers by induction, we need to prove two cases. First is the base case, where we show the property holds for zero. Second is the inductive case, where we assume the property holds for an arbitrary natural m (we call this the inductive hypothesis), and then show that the property must also hold for suc m.

If we write P m for a property of m, then what we need to demonstrate are the following two inference rules:

------
P zero

P m
---------
P (suc m)

Let’s unpack these rules. The first rule is the base case, and requires we show that property P holds for zero. The second rule is the inductive case, and requires we show that if we assume the inductive hypothesis—namely that P holds for m—then it follows that P also holds for suc m.

Why does this work? Again, it can be explained by a creation story. To start with, we know no properties:

-- In the beginning, no properties are known.

Now, we apply the two rules to all the properties we know about. The base case tells us that P zero holds, so we add it to the set of known properties. The inductive case tells us that if P m holds (on the day before today) then P (suc m) also holds (today). We didn’t know about any properties before today, so the inductive case doesn’t apply:

-- On the first day, one property is known.
P zero

Then we repeat the process, so on the next day we know about all the properties from the day before, plus any properties added by the rules. The base case tells us that P zero holds, but we already knew that. But now the inductive case tells us that since P zero held yesterday, then P (suc zero) holds today:

-- On the second day, two properties are known.
P zero
P (suc zero)

And we repeat the process again. Now the inductive case tells us that since P zero and P (suc zero) both hold, then P (suc zero) and P (suc (suc zero)) also hold. We already knew about the first of these, but the second is new:

-- On the third day, three properties are known.
P zero
P (suc zero)
P (suc (suc zero))

You’ve got the hang of it by now:

-- On the fourth day, four properties are known.
P zero
P (suc zero)
P (suc (suc zero))
P (suc (suc (suc zero)))

The process continues. On the n’th day there will be n distinct properties that hold. The property of every natural number will appear on some given day. In particular, the property P n first appears on day n+1.

Our first proof: associativity

To prove associativity, we take P m to be the property:

(m + n) + p ≡ m + (n + p)

Here n and p are arbitrary natural numbers, so if we can show the equation holds for all m it will also hold for all n and p. The appropriate instances of the inference rules are:

-------------------------------
(zero + n) + p ≡ zero + (n + p)

(m + n) + p ≡ m + (n + p)
---------------------------------
(suc m + n) + p ≡ suc m + (n + p)

If we can demonstrate both of these, then associativity of addition follows by induction.

Here is the proposition’s statement and proof:
+-assoc : ∀ (m n p : ℕ) → (m + n) + p ≡ m + (n + p)
+-assoc zero n p =
  begin
    (zero + n) + p
  ≡⟨⟩
    n + p
  ≡⟨⟩
    zero + (n + p)
  ∎
+-assoc (suc m) n p =
  begin
    (suc m + n) + p
  ≡⟨⟩
    suc (m + n) + p
  ≡⟨⟩
    suc ((m + n) + p)
  ≡⟨ cong suc (+-assoc m n p) ⟩
    suc (m + (n + p))
  ≡⟨⟩
    suc m + (n + p)
  ∎

We have named the proof +-assoc. In Agda, identifiers can consist of any sequence of characters not including spaces or the characters @.(){};_.

Let’s unpack this code. The signature states that we are defining the identifier +-assoc which provides evidence for the proposition:

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

The upside down A is pronounced “for all”, and the proposition asserts that for all natural numbers m, n, and p the equation (m + n) + p ≡ m + (n + p) holds. Evidence for the proposition is a function that accepts three natural numbers, binds them to m, n, and p, and returns evidence for the corresponding instance of the equation.

For the base case, we must show:

(zero + n) + p ≡ zero + (n + p)

Simplifying both sides with the base case of addition yields the equation:

n + p ≡ n + p

This holds trivially. Reading the chain of equations in the base case of the proof, the top and bottom of the chain match the two sides of the equation to be shown, and reading down from the top and up from the bottom takes us to n + p in the middle. No justification other than simplification is required.

For the inductive case, we must show:

(suc m + n) + p ≡ suc m + (n + p)

Simplifying both sides with the inductive case of addition yields the equation:

suc ((m + n) + p) ≡ suc (m + (n + p))

This in turn follows by prefacing suc to both sides of the induction hypothesis:

(m + n) + p ≡ m + (n + p)

Reading the chain of equations in the inductive case of the proof, the top and bottom of the chain match the two sides of the equation to be shown, and reading down from the top and up from the bottom takes us to the simplified equation above. The remaining equation does not follow from simplification alone, so we use an additional operator for chain reasoning, _≡⟨_⟩_, where a justification for the equation appears within angle brackets. The justification given is:

⟨ cong suc (+-assoc m n p) ⟩

Here, the recursive invocation +-assoc m n p has as its type the induction hypothesis, and cong suc prefaces suc to each side to yield the needed equation.

A relation is said to be a congruence for a given function if it is preserved by applying that function. If e is evidence that x ≡ y, then cong f e is evidence that f x ≡ f y, for any function f.

Here the inductive hypothesis is not assumed, but instead proved by a recursive invocation of the function we are defining, +-assoc m n p. As with addition, this is well founded because associativity of larger numbers is proved in terms of associativity of smaller numbers. In this case, assoc (suc m) n p is proved using assoc m n p. The correspondence between proof by induction and definition by recursion is one of the most appealing aspects of Agda.

Induction as recursion

As a concrete example of how induction corresponds to recursion, here is the computation that occurs when instantiating m to 2 in the proof of associativity.

+-assoc-0 : ∀ (n p : ℕ) → (0 + n) + p ≡ 0 + (n + p)
+-assoc-0 n p =
  begin
    (0 + n) + p
  ≡⟨⟩
    n + p
  ≡⟨⟩
    0 + (n + p)
  ∎

+-assoc-1 : ∀ (n p : ℕ) → (1 + n) + p ≡ 1 + (n + p)
+-assoc-1 n p =
  begin
    (1 + n) + p
  ≡⟨⟩
    suc (0 + n) + p
  ≡⟨⟩
    suc ((0 + n) + p)
  ≡⟨ cong suc (+-assoc-0 n p) ⟩
    suc (0 + (n + p))
  ≡⟨⟩
    1 + (n + p)
  ∎

+-assoc-2 : ∀ (n p : ℕ) → (2 + n) + p ≡ 2 + (n + p)
+-assoc-2 n p =
  begin
    (2 + n) + p
  ≡⟨⟩
    suc (1 + n) + p
  ≡⟨⟩
    suc ((1 + n) + p)
  ≡⟨ cong suc (+-assoc-1 n p) ⟩
    suc (1 + (n + p))
  ≡⟨⟩
    2 + (n + p)
  ∎

Terminology and notation

The symbol ∀ appears in the statement of associativity to indicate that it holds for all numbers m, n, and p. We refer to ∀ as the universal quantifier, and it is discussed further in Chapter Quantifiers.

Evidence for a universal quantifier is a function. The signatures

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

and

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

are equivalent. They differ from a function type such as ℕ → ℕ → ℕ in that variables are associated with each argument type, and the result type may mention (or depend upon) these variables; hence they are called dependent functions.

Ordinary functions are a special case of dependent functions. For instance, the signatures

_+_ : ℕ → ℕ → ℕ

and

_+_ : ∀ (m n : ℕ) → ℕ

and

_+_ : ∀ (m : ℕ) → ∀ (n : ℕ) → ℕ

are all equivalent.

Our second proof: commutativity

Another important property of addition is that it is commutative, that is, that the order of the operands does not matter:

m + n ≡ n + m

The proof requires that we first demonstrate two lemmas.

The first lemma

The base case of the definition of addition states that zero is a left-identity:

zero + n ≡ n

Our first lemma states that zero is also a right-identity:

m + zero ≡ m
Here is the lemma’s statement and proof:
+-identityʳ : ∀ (m : ℕ) → m + zero ≡ m
+-identityʳ zero =
  begin
    zero + zero
  ≡⟨⟩
    zero
  ∎
+-identityʳ (suc m) =
  begin
    suc m + zero
  ≡⟨⟩
    suc (m + zero)
  ≡⟨ cong suc (+-identityʳ m) ⟩
    suc m
  ∎

The signature states that we are defining the identifier +-identityʳ which provides evidence for the proposition:

∀ (m : ℕ) → m + zero ≡ m

Evidence for the proposition is a function that accepts a natural number, binds it to m, and returns evidence for the corresponding instance of the equation. The proof is by induction on m.

For the base case, we must show:

zero + zero ≡ zero

Simplifying with the base case of addition, this is straightforward.

For the inductive case, we must show:

(suc m) + zero = suc m

Simplifying both sides with the inductive case of addition yields the equation:

suc (m + zero) = suc m

This in turn follows by prefacing suc to both sides of the induction hypothesis:

m + zero ≡ m

Reading the chain of equations down from the top and up from the bottom takes us to the simplified equation above. The remaining equation has the justification:

⟨ cong suc (+-identityʳ m) ⟩

Here, the recursive invocation +-identityʳ m has as its type the induction hypothesis, and cong suc prefaces suc to each side to yield the needed equation. This completes the first lemma.

The second lemma

The inductive case of the definition of addition pushes suc on the first argument to the outside:

suc m + n ≡ suc (m + n)

Our second lemma does the same for suc on the second argument:

m + suc n ≡ suc (m + n)
Here is the lemma’s statement and proof:
+-suc : ∀ (m n : ℕ) → m + suc n ≡ suc (m + n)
+-suc zero n =
  begin
    zero + suc n
  ≡⟨⟩
    suc n
  ≡⟨⟩
    suc (zero + n)
  ∎
+-suc (suc m) n =
  begin
    suc m + suc n
  ≡⟨⟩
    suc (m + suc n)
  ≡⟨ cong suc (+-suc m n) ⟩
    suc (suc (m + n))
  ≡⟨⟩
    suc (suc m + n)
  ∎

The signature states that we are defining the identifier +-suc which provides evidence for the proposition:

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

Evidence for the proposition is a function that accepts two natural numbers, binds them to m and n, and returns evidence for the corresponding instance of the equation. The proof is by induction on m.

For the base case, we must show:

zero + suc n ≡ suc (zero + n)

Simplifying with the base case of addition, this is straightforward.

For the inductive case, we must show:

suc m + suc n ≡ suc (suc m + n)

Simplifying both sides with the inductive case of addition yields the equation:

suc (m + suc n) ≡ suc (suc (m + n))

This in turn follows by prefacing suc to both sides of the induction hypothesis:

m + suc n ≡ suc (m + n)

Reading the chain of equations down from the top and up from the bottom takes us to the simplified equation in the middle. The remaining equation has the justification:

⟨ cong suc (+-suc m n) ⟩

Here, the recursive invocation +-suc m n has as its type the induction hypothesis, and cong suc prefaces suc to each side to yield the needed equation. This completes the second lemma.

The proposition

Finally, here is our proposition’s statement and proof:
+-comm : ∀ (m n : ℕ) → m + n ≡ n + m
+-comm m zero =
  begin
    m + zero
  ≡⟨ +-identityʳ m ⟩
    m
  ≡⟨⟩
    zero + m
  ∎
+-comm m (suc n) =
  begin
    m + suc n
  ≡⟨ +-suc m n ⟩
    suc (m + n)
  ≡⟨ cong suc (+-comm m n) ⟩
    suc (n + m)
  ≡⟨⟩
    suc n + m
  ∎

The first line states that we are defining the identifier +-comm which provides evidence for the proposition:

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

Evidence for the proposition is a function that accepts two natural numbers, binds them to m and n, and returns evidence for the corresponding instance of the equation. The proof is by induction on n. (Not on m this time!)

For the base case, we must show:

m + zero ≡ zero + m

Simplifying both sides with the base case of addition yields the equation:

m + zero ≡ m

The remaining equation has the justification ⟨ +-identityʳ m ⟩, which invokes the first lemma.

For the inductive case, we must show:

m + suc n ≡ suc n + m

Simplifying both sides with the inductive case of addition yields the equation:

m + suc n ≡ suc (n + m)

We show this in two steps. First, we have:

m + suc n ≡ suc (m + n)

which is justified by the second lemma, ⟨ +-suc m n ⟩. Then we have

suc (m + n) ≡ suc (n + m)

which is justified by congruence and the induction hypothesis, ⟨ cong suc (+-comm m n) ⟩. This completes the proof.

Agda requires that identifiers are defined before they are used, so we must present the lemmas before the main proposition, as we have done above. In practice, one will often attempt to prove the main proposition first, and the equations required to do so will suggest what lemmas to prove.

Our first corollary: rearranging

We can apply associativity to rearrange parentheses however we like. Here is an example:
+-rearrange : ∀ (m n p q : ℕ) → (m + n) + (p + q) ≡ m + (n + p) + q
+-rearrange m n p q =
  begin
    (m + n) + (p + q)
  ≡⟨ sym (+-assoc (m + n) p q) ⟩
    ((m + n) + p) + q
  ≡⟨ cong (_+ q) (+-assoc m n p) ⟩
    (m + (n + p)) + q
  ∎

No induction is required, we simply apply associativity twice. A few points are worthy of note.

First, addition associates to the left, so m + (n + p) + q stands for (m + (n + p)) + q.

Second, we use sym to interchange the sides of an equation. Proposition +-assoc (m + n) p q shifts parentheses from left to right:

((m + n) + p) + q ≡ (m + n) + (p + q)

To shift them the other way, we use sym (+-assoc (m + n) p q):

(m + n) + (p + q) ≡ ((m + n) + p) + q

In general, if e provides evidence for x ≡ y then sym e provides evidence for y ≡ x.

Third, Agda supports a variant of the section notation introduced by Richard Bird. We write (_+ y) for the function that applied to x returns x + y. Thus, applying the congruence cong (_+ q) to assoc m n p takes the equation:

(m + n) + p  ≡  m + (n + p)

into the equation:

((m + n) + p) + q  ≡  (m + (n + p)) + q

Similarly, we write (x +_) for the function that applied to y returns x + y; the same works for any infix operator.

Creation, one last time

Returning to the proof of associativity, it may be helpful to view the inductive proof (or, equivalently, the recursive definition) as a creation story. This time we are concerned with judgments asserting associativity:

 -- In the beginning, we know nothing about associativity.

Now, we apply the rules to all the judgments we know about. The base case tells us that (zero + n) + p ≡ zero + (n + p) for every natural n and p. The inductive case tells us that if (m + n) + p ≡ m + (n + p) (on the day before today) then (suc m + n) + p ≡ suc m + (n + p) (today). We didn’t know any judgments about associativity before today, so that rule doesn’t give us any new judgments:

-- On the first day, we know about associativity of 0.
(0 + 0) + 0 ≡ 0 + (0 + 0)   ...   (0 + 4) + 5 ≡ 0 + (4 + 5)   ...

Then we repeat the process, so on the next day we know about all the judgments from the day before, plus any judgments added by the rules. The base case tells us nothing new, but now the inductive case adds more judgments:

-- On the second day, we know about associativity of 0 and 1.
(0 + 0) + 0 ≡ 0 + (0 + 0)   ...   (0 + 4) + 5 ≡ 0 + (4 + 5)   ...
(1 + 0) + 0 ≡ 1 + (0 + 0)   ...   (1 + 4) + 5 ≡ 1 + (4 + 5)   ...

And we repeat the process again:

-- On the third day, we know about associativity of 0, 1, and 2.
(0 + 0) + 0 ≡ 0 + (0 + 0)   ...   (0 + 4) + 5 ≡ 0 + (4 + 5)   ...
(1 + 0) + 0 ≡ 1 + (0 + 0)   ...   (1 + 4) + 5 ≡ 1 + (4 + 5)   ...
(2 + 0) + 0 ≡ 2 + (0 + 0)   ...   (2 + 4) + 5 ≡ 2 + (4 + 5)   ...

You’ve got the hang of it by now:

-- On the fourth day, we know about associativity of 0, 1, 2, and 3.
(0 + 0) + 0 ≡ 0 + (0 + 0)   ...   (0 + 4) + 5 ≡ 0 + (4 + 5)   ...
(1 + 0) + 0 ≡ 1 + (0 + 0)   ...   (1 + 4) + 5 ≡ 1 + (4 + 5)   ...
(2 + 0) + 0 ≡ 2 + (0 + 0)   ...   (2 + 4) + 5 ≡ 2 + (4 + 5)   ...
(3 + 0) + 0 ≡ 3 + (0 + 0)   ...   (3 + 4) + 5 ≡ 3 + (4 + 5)   ...

The process continues. On the m’th day we will know all the judgments where the first number is less than m.

There is also a completely finite approach to generating the same equations, which is left as an exercise for the reader.

Exercise finite-+-assoc (stretch)

Write out what is known about associativity of addition on each of the first four days using a finite story of creation, as earlier.

-- Your code goes here

Associativity with rewrite

There is more than one way to skin a cat. Here is a second proof of associativity of addition in Agda, using rewrite rather than chains of equations:
+-assoc′ : ∀ (m n p : ℕ) → (m + n) + p ≡ m + (n + p)
+-assoc′ zero    n p                          =  refl
+-assoc′ (suc m) n p  rewrite +-assoc′ m n p  =  refl

For the base case, we must show:

(zero + n) + p ≡ zero + (n + p)

Simplifying both sides with the base case of addition yields the equation:

n + p ≡ n + p

This holds trivially. The proof that a term is equal to itself is written refl.

For the inductive case, we must show:

(suc m + n) + p ≡ suc m + (n + p)

Simplifying both sides with the inductive case of addition yields the equation:

suc ((m + n) + p) ≡ suc (m + (n + p))

This is our goal to be proved. Rewriting by a given equation is indicated by the keyword rewrite followed by a proof of that equation. Rewriting replaces each occurrence of the left-hand side of the equation in the goal by the right-hand side. In this case, after rewriting by the inductive hypothesis our goal becomes

suc (m + (n + p)) ≡ suc (m + (n + p))

and the proof is again given by refl. Rewriting avoids not only chains of equations but also the need to invoke cong.

Commutativity with rewrite

Here is a second proof of commutativity of addition, using rewrite rather than chains of equations:
+-identity′ : ∀ (n : ℕ) → n + zero ≡ n
+-identity′ zero = refl
+-identity′ (suc n) rewrite +-identity′ n = refl

+-suc′ : ∀ (m n : ℕ) → m + suc n ≡ suc (m + n)
+-suc′ zero n = refl
+-suc′ (suc m) n rewrite +-suc′ m n = refl

+-comm′ : ∀ (m n : ℕ) → m + n ≡ n + m
+-comm′ m zero rewrite +-identity′ m = refl
+-comm′ m (suc n) rewrite +-suc′ m n | +-comm′ m n = refl

In the final line, rewriting with two equations is indicated by separating the two proofs of the relevant equations by a vertical bar; the rewrite on the left is performed before that on the right.

Building proofs interactively

It is instructive to see how to build the alternative proof of associativity using the interactive features of Agda in Emacs. Begin by typing:

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

The question mark indicates that you would like Agda to help with filling in that part of the code. If you type C-c C-l (control-c followed by control-l), the question mark will be replaced:

+-assoc′ : ∀ (m n p : ℕ) → (m + n) + p ≡ m + (n + p)
+-assoc′ m n p = { }0

The empty braces are called a hole, and 0 is a number used for referring to the hole. The hole may display highlighted in green. Emacs will also create a new window at the bottom of the screen displaying the text:

?0 : ((m + n) + p) ≡ (m + (n + p))

This indicates that hole 0 is to be filled in with a proof of the stated judgment.

We wish to prove the proposition by induction on m. Move the cursor into the hole and type C-c C-c. You will be given the prompt:

pattern variables to case (empty for split on result):

Typing m will cause a split on that variable, resulting in an update to the code:

+-assoc′ : ∀ (m n p : ℕ) → (m + n) + p ≡ m + (n + p)
+-assoc′ zero n p = { }0
+-assoc′ (suc m) n p = { }1

There are now two holes, and the window at the bottom tells you what each is required to prove:

?0 : ((zero + n) + p) ≡ (zero + (n + p))
?1 : ((suc m + n) + p) ≡ (suc m + (n + p))

Going into hole 0 and typing C-c C-, will display the text:

Goal: (n + p) ≡ (n + p)
————————————————————————————————————————————————————————————
p : ℕ
n : ℕ

This indicates that after simplification the goal for hole 0 is as stated, and that variables p and n of the stated types are available to use in the proof. The proof of the given goal is trivial, and going into the goal and typing C-c C-r will fill it in. Typing C-c C-l renumbers the remaining hole to 0:

+-assoc′ : ∀ (m n p : ℕ) → (m + n) + p ≡ m + (n + p)
+-assoc′ zero n p = refl
+-assoc′ (suc m) n p = { }0

Going into the new hole 0 and typing C-c C-, will display the text:

Goal: suc ((m + n) + p) ≡ suc (m + (n + p))
————————————————————————————————————————————————————————————
p : ℕ
n : ℕ
m : ℕ

Again, this gives the simplified goal and the available variables. In this case, we need to rewrite by the induction hypothesis, so let’s edit the text accordingly:

+-assoc′ : ∀ (m n p : ℕ) → (m + n) + p ≡ m + (n + p)
+-assoc′ zero n p = refl
+-assoc′ (suc m) n p rewrite +-assoc′ m n p = { }0

Going into the remaining hole and typing C-c C-, will display the text:

Goal: suc (m + (n + p)) ≡ suc (m + (n + p))
————————————————————————————————————————————————————————————
p : ℕ
n : ℕ
m : ℕ

The proof of the given goal is trivial, and going into the goal and typing C-c C-r will fill it in, completing the proof:

+-assoc′ : ∀ (m n p : ℕ) → (m + n) + p ≡ m + (n + p)
+-assoc′ zero n p = refl
+-assoc′ (suc m) n p rewrite +-assoc′ m n p = refl

Exercise +-swap (recommended)

Show

m + (n + p) ≡ n + (m + p)

for all naturals m, n, and p. No induction is needed, just apply the previous results which show addition is associative and commutative.

-- Your code goes here

Exercise *-distrib-+ (recommended)

Show multiplication distributes over addition, that is,

(m + n) * p ≡ m * p + n * p

for all naturals m, n, and p.

-- Your code goes here

Exercise *-assoc (recommended)

Show multiplication is associative, that is,

(m * n) * p ≡ m * (n * p)

for all naturals m, n, and p.

-- Your code goes here

Exercise *-comm (practice)

Show multiplication is commutative, that is,

m * n ≡ n * m

for all naturals m and n. As with commutativity of addition, you will need to formulate and prove suitable lemmas.

-- Your code goes here

Exercise 0∸n≡0 (practice)

Show

zero ∸ n ≡ zero

for all naturals n. Did your proof require induction?

-- Your code goes here

Exercise ∸-+-assoc (practice)

Show that monus associates with addition, that is,

m ∸ n ∸ p ≡ m ∸ (n + p)

for all naturals m, n, and p.

-- Your code goes here

Exercise +*^ (stretch)

Show the following three laws

 m ^ (n + p) ≡ (m ^ n) * (m ^ p)  (^-distribˡ-+-*)
 (m * n) ^ p ≡ (m ^ p) * (n ^ p)  (^-distribʳ-*)
 (m ^ n) ^ p ≡ m ^ (n * p)        (^-*-assoc)

for all m, n, and p.

-- Your code goes here

Exercise Bin-laws (stretch)

Recall that Exercise Bin defines a datatype Bin of bitstrings representing natural numbers, and asks you to define functions

inc   : Bin → Bin
to    : ℕ → Bin
from  : Bin → ℕ

Consider the following laws, where n ranges over naturals and b over bitstrings:

from (inc b) ≡ suc (from b)
to (from b) ≡ b
from (to n) ≡ n

For each law: if it holds, prove; if not, give a counterexample.

-- Your code goes here

Standard library

Definitions similar to those in this chapter can be found in the standard library:
import Data.Nat.Properties using (+-assoc; +-identityʳ; +-suc; +-comm)

Unicode

This chapter uses the following unicode:

∀  U+2200  FOR ALL (\forall, \all)
ʳ  U+02B3  MODIFIER LETTER SMALL R (\^r)
′  U+2032  PRIME (\')
″  U+2033  DOUBLE PRIME (\')
‴  U+2034  TRIPLE PRIME (\')
⁗  U+2057  QUADRUPLE PRIME (\')

Similar to \r, the command \^r gives access to a variety of superscript rightward arrows, and also a superscript letter r. The command \' gives access to a range of primes (′ ″ ‴ ⁗).