Induction: Proof by Induction
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 import 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_; _≡⟨⟩_; _≡⟨_⟩_; _∎) open import Data.Nat using (ℕ; zero; suc; _+_; _*_; _∸_)
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 identity0
if0 + n ≡ n
, and right identity0
ifn + 0 ≡ n
, for alln
. 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 allm
,n
, andp
. 
Commutativity. Operator
+
is commutative if order of arguments does not matter:m + n ≡ n + m
, for allm
andn
. 
Distributivity. Operator
*
distributes over operator+
from the left if(m + n) * p ≡ (m * p) + (n * p)
, for allm
,n
, andp
, and from the right ifm * (p + q) ≡ (m * p) + (m * q)
, for allm
,p
, andq
.
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.
+assoc2 : ∀ (n p : ℕ) → (2 + n) + p ≡ 2 + (n + p) +assoc2 n p = begin (2 + n) + p ≡⟨⟩ suc (1 + n) + p ≡⟨⟩ suc ((1 + n) + p) ≡⟨ cong suc (+assoc1 n p) ⟩ suc (1 + (n + p)) ≡⟨⟩ 2 + (n + p) ∎ where +assoc1 : ∀ (n p : ℕ) → (1 + n) + p ≡ 1 + (n + p) +assoc1 n p = begin (1 + n) + p ≡⟨⟩ suc (0 + n) + p ≡⟨⟩ suc ((0 + n) + p) ≡⟨ cong suc (+assoc0 n p) ⟩ suc (0 + (n + p)) ≡⟨⟩ 1 + (n + p) ∎ where +assoc0 : ∀ (n p : ℕ) → (0 + n) + p ≡ 0 + (n + p) +assoc0 n p = begin (0 + n) + p ≡⟨⟩ n + p ≡⟨⟩ 0 + (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 notations
+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.
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 leftidentity:
zero + n ≡ n
Our first lemma states that zero is also a rightidentity:
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) ≡⟨ +assoc m n (p + q) ⟩ m + (n + (p + q)) ≡⟨ cong (m +_) (sym (+assoc n p q)) ⟩ m + ((n + p) + q) ≡⟨ sym (+assoc m (n + p) q) ⟩ (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 n p q
shifts parentheses from right to left:
(n + p) + q ≡ n + (p + q)
To shift them the other way, we use sym (+assoc n p q)
:
n + (p + q) ≡ (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 (x +_)
for the function that applied to y
returns x + y
. Thus, applying the congruence cong (m +_)
takes
the above equation into:
m + (n + (p + q)) ≡ m + ((n + p) + q)
Similarly, we write (_+ x)
for the function that applied to y
returns y + x
; 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))
After rewriting with the inductive hypothesis these two terms are equal, and the
proof is again given by refl
. Rewriting by a given equation is indicated by
the keyword rewrite
followed by a proof of that equation. 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 Cc Cl
(controlc
followed by controll), 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 Cc Cc
. 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 Cc 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 Cc Cr
will fill it in.
Typing Cc Cl
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 Cc 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 Cc 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 Cc Cr
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
.
Exercise Binlaws
(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 (′ ″ ‴ ⁗
).