---
title : "Induction: Proof by Induction"
permalink : /Induction/
---
```agda
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:
```agda
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) {#operators}
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:
```agda
_ : (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:
```agda
+-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.
```agda
+-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](/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:
```agda
+-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:
```agda
+-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:
```agda
+-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 {#sections}
We can apply associativity to rearrange parentheses however we like.
Here is an example:
```agda
+-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) {#finite-plus-assoc}
Write out what is known about associativity of addition on each of the
first four days using a finite story of creation, as
[earlier](/Naturals/#finite-creation).
```agda
-- 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:
```agda
+-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:
```agda
+-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) {#plus-swap}
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.
```agda
-- Your code goes here
+-swap : ∀ (m n p : ℕ) → m + (n + p) ≡ n + (m + p)
+-swap m n p =
begin
m + (n + p)
≡⟨ sym (+-assoc m n p) ⟩
(m + n) + p
≡⟨ cong (_+ p) (+-comm m n) ⟩
(n + m) + p
≡⟨ +-assoc n m p ⟩
n + (m + p)
∎
```
#### Exercise `*-distrib-+` (recommended) {#times-distrib-plus}
Show multiplication distributes over addition, that is,
(m + n) * p ≡ m * p + n * p
for all naturals `m`, `n`, and `p`.
```agda
-- Your code goes here
*-distrib-+ : ∀ (m n p : ℕ) → (m + n) * p ≡ m * p + n * p
*-distrib-+ zero n p = refl
*-distrib-+ (suc m) n p rewrite *-distrib-+ m n p | +-assoc p (m * p) (n * p) = refl
```
#### Exercise `*-assoc` (recommended) {#times-assoc}
Show multiplication is associative, that is,
(m * n) * p ≡ m * (n * p)
for all naturals `m`, `n`, and `p`.
```agda
-- Your code goes here
*-assoc : ∀ (m n p : ℕ) → (m * n) * p ≡ m * (n * p)
*-assoc zero n p = refl
*-assoc (suc m) n p rewrite *-distrib-+ n (m * n) p | *-assoc m n p = refl
```
#### Exercise `*-comm` (practice) {#times-comm}
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.
```agda
-- Your code goes here
*-zero : ∀ (m : ℕ) → m * zero ≡ zero
*-zero zero = refl
*-zero (suc m) rewrite *-zero m = refl
-- NOTE: manually w/o rewrite
-- *-zero (suc m) =
-- begin
-- suc m * zero
-- ≡⟨⟩
-- zero + m * zero
-- ≡⟨⟩
-- m * zero
-- ≡⟨ *-zero m ⟩
-- zero
-- ∎
-- Like inductive `*` but on the right operand
*-sucʳ : ∀ (m n : ℕ) → n * suc m ≡ n + n * m
*-sucʳ m zero = refl
*-sucʳ m (suc n) =
begin
suc n * suc m
≡⟨⟩
suc m + n * suc m
≡⟨ cong (\x → suc m + x) (*-sucʳ m n) ⟩
suc m + (n + n * m)
≡⟨ +-comm (suc m) (n + n * m) ⟩
(n + n * m) + suc m
≡⟨ +-suc (n + n * m) m ⟩
suc (n + n * m + m)
≡⟨ cong suc (+-assoc n (n * m) m) ⟩
suc (n + (n * m + m))
≡⟨ cong (\x → suc (n + x)) (+-comm (n * m) m) ⟩
suc (n + (m + n * m))
∎
-- *-sucʳ zero n = {!!}
-- *-sucʳ (suc m) n = {!!}
*-comm : ∀ (m n : ℕ) → m * n ≡ n * m
*-comm zero n rewrite *-zero n = refl
*-comm (suc m) n rewrite *-comm m n | sym (*-sucʳ m n) = refl
-- NOTE: manually w/o rewrite
-- *-comm (suc m) n =
-- begin
-- suc m * n
-- ≡⟨⟩
-- n + m * n
-- ≡⟨ cong (n +_) (*-comm m n) ⟩
-- n + n * m
-- ≡⟨ sym (*-sucʳ m n) ⟩
-- n * suc m
-- ∎a
```
#### Exercise `0∸n≡0` (practice) {#zero-monus}
Show
zero ∸ n ≡ zero
for all naturals `n`. Did your proof require induction?
```agda
-- Your code goes here
0∸n≡0 : ∀ (n : ℕ) → 0 ∸ n ≡ 0
0∸n≡0 zero = refl
0∸n≡0 (suc n) = refl
```
#### Exercise `∸-+-assoc` (practice) {#monus-plus-assoc}
Show that monus associates with addition, that is,
m ∸ n ∸ p ≡ m ∸ (n + p)
for all naturals `m`, `n`, and `p`.
```agda
-- Your code goes here
-- ∸-suc-∸-suc : ∀ (m n p : ℕ) → m ∸ n ∸ p ≡ m ∸ (n + p)
-- -- Goal: m ∸ suc n ∸ suc p ≡ m ∸ suc (n + suc p)
-- ∸-suc-∸-suc m n p = {!!}
∸-+-assoc : ∀ (m n p : ℕ) → m ∸ n ∸ p ≡ m ∸ (n + p)
∸-+-assoc m zero zero = refl
∸-+-assoc m (suc n) zero rewrite +-identityʳ n = refl
∸-+-assoc m zero (suc p) = refl
∸-+-assoc zero (suc n) (suc p) = refl
∸-+-assoc (suc m) (suc n) p =
begin
m ∸ n ∸ p
≡⟨ ∸-+-assoc m n p ⟩
m ∸ (n + p)
∎
-- NOTE: Why is this so much harder to proof than the case above?
-- Goal: m ∸ suc n ∸ suc p ≡ m ∸ suc (n + suc p)
-- ∸-+-assoc m (suc n) (suc p) =
-- begin
-- m ∸ suc n ∸ suc p
-- ≡⟨⟩
-- (m ∸ suc n) ∸ suc p
-- ≡⟨⟩
-- (m ∸ suc n ∸ suc p)
-- ≡⟨ {!!} ⟩
-- (m ∸ (suc n + suc p))
-- ≡⟨⟩
-- m ∸ suc (n + suc p)
-- ∎
```
#### 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
*-identityʳ : ∀ (m : ℕ) → m * 1 ≡ m
*-identityʳ zero = refl
*-identityʳ (suc m) =
begin
suc (m * 1)
≡⟨ cong suc (*-identityʳ m) ⟩
suc m
∎
^-distribˡ-+-* : ∀ (m n p : ℕ) → m ^ (n + p) ≡ (m ^ n) * (m ^ p)
^-distribˡ-+-* m zero zero = refl
^-distribˡ-+-* m zero (suc p) =
begin
m * m ^ p
≡⟨ sym (+-identityʳ (m * m ^ p)) ⟩
m * m ^ p + zero
∎
^-distribˡ-+-* m (suc n) zero =
begin
m * m ^ (n + zero)
≡⟨ cong (\x → m * m ^ x) (+-identityʳ n) ⟩
m * m ^ n
≡⟨ sym (*-identityʳ (m * m ^ n)) ⟩
(m * m ^ n) * 1
∎
^-distribˡ-+-* zero (suc n) (suc p) = refl
^-distribˡ-+-* (suc m) (suc n) (suc p) =
begin
suc m * suc m ^ (n + suc p)
≡⟨ cong (\x → suc m * suc m ^ x) (+-suc n p) ⟩
suc m * (suc m * suc m ^ (n + p))
≡⟨ sym (*-assoc (suc m) (suc m) (suc m ^ (n + p))) ⟩
suc m * suc m * (suc m ^ (n + p))
≡⟨ cong (\x → suc m * suc m * x) (^-distribˡ-+-* (suc m) n p) ⟩
suc m * suc m * ((suc m ^ n) * (suc m ^ p))
≡⟨ sym (*-assoc (suc m * suc m) (suc m ^ n) (suc m ^ p)) ⟩
suc m * suc m * suc m ^ n * suc m ^ p
≡⟨ cong (\x → x * (suc m ^ p)) (*-assoc (suc m) (suc m) (suc m ^ n)) ⟩
suc m * (suc m * suc m ^ n) * (suc m ^ p)
≡⟨ cong (\x → x * (suc m ^ p)) (*-comm (suc m) (suc m * suc m ^ n)) ⟩
(suc m * suc m ^ n) * suc m * suc m ^ p
≡⟨ *-assoc (suc m * suc m ^ n) (suc m) (suc m ^ p) ⟩
(suc m * suc m ^ n) * (suc m * suc m ^ p)
≡⟨⟩
(suc m ^ suc n) * (suc m ^ suc p)
∎
^-distribʳ-* : ∀ (m n p : ℕ) → (m * n) ^ p ≡ (m ^ p) * (n ^ p)
^-distribʳ-* m n zero = refl
^-distribʳ-* m n (suc p) =
begin
(m * n) ^ (suc p)
≡⟨⟩
(m * n) * (m * n) ^ p
≡⟨⟩
(m * n) * ((m * n) ^ p)
≡⟨ cong (\x → m * n * x) (^-distribʳ-* m n p) ⟩
(m * n) * ((m ^ p) * (n ^ p))
≡⟨ sym (*-assoc (m * n) (m ^ p) (n ^ p)) ⟩
(m * n) * (m ^ p) * (n ^ p)
≡⟨ cong (\x → x * (m ^ p) * (n ^ p)) (*-comm m n) ⟩
(n * m) * (m ^ p) * (n ^ p)
≡⟨ cong (\x → x * (n ^ p)) (*-assoc n m (m ^ p)) ⟩
n * (m * (m ^ p)) * (n ^ p)
≡⟨ cong (\x → x * (n ^ p)) (*-comm n (m * m ^ p)) ⟩
(m * m ^ p) * n * n ^ p
≡⟨ *-assoc (m * m ^ p) n (n ^ p) ⟩
(m * m ^ p) * (n * n ^ p)
≡⟨⟩
(m ^ suc p) * (n ^ suc p)
∎
^-*-assoc : ∀ (m n p : ℕ) → (m ^ n) ^ p ≡ m ^ (n * p)
^-*-assoc m n zero =
begin
(m ^ n) ^ zero
≡⟨⟩
m ^ 0
≡⟨⟩
m ^ (0 * n)
≡⟨ cong (\x → m ^ x) (*-comm 0 n) ⟩
m ^ (n * 0)
∎
^-*-assoc m n (suc p) =
begin
(m ^ n) ^ (suc p)
≡⟨⟩
m ^ n * (m ^ n) ^ p
≡⟨ cong (\x → m ^ n * x) (^-*-assoc m n p) ⟩
m ^ n * m ^ (n * p)
≡⟨ cong (\x → m ^ n * m ^ x) (*-comm n p) ⟩
(m ^ n) * (m ^ (p * n))
≡⟨ sym (^-distribˡ-+-* m n (p * n)) ⟩
m ^ (n + p * n)
≡⟨⟩
m ^ (suc p * n)
≡⟨ cong (\x → m ^ x) (*-comm (suc p) n) ⟩
m ^ (n * suc p)
∎
```
#### Exercise `Bin-laws` (stretch) {#Bin-laws}
Recall that
Exercise [Bin](/Naturals/#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.
```agda
-- Your code goes here
-- NOTE: This doesn't work:
--
-- open import plfa.part1.Naturals using (inc,to,from)
--
-- It fails with:
-- Duplicate binding for built-in thing NATURAL, previous binding to
-- Agda.Builtin.Nat.Nat
-- when checking the pragma BUILTIN NATURAL ℕ
data Bin : Set where
⟨⟩ : Bin
_O : Bin → Bin
_I : Bin → Bin
inc : Bin → Bin
inc ⟨⟩ = ⟨⟩ I
inc (rest O) = rest I
inc (rest I) = (inc rest) O
to : ℕ → Bin
to zero = ⟨⟩ O
to (suc n) = inc (to n)
from : Bin → ℕ
from ⟨⟩ = 0
from (rest O) = 2 * (from rest)
from (rest I) = 1 + 2 * (from rest)
from-inc-suc-from : ∀ (b : Bin) → from (inc b) ≡ suc (from b)
from-inc-suc-from ⟨⟩ = refl
from-inc-suc-from (b O) = refl
from-inc-suc-from (b I) =
begin
from (inc (b I))
≡⟨⟩
from ((inc b) O)
≡⟨⟩
2 * (from (inc b))
≡⟨ cong (\x → 2 * x) (from-inc-suc-from b) ⟩
2 * suc (from b)
≡⟨⟩
2 * (1 + (from b))
≡⟨ *-comm 2 (1 + (from b)) ⟩
(1 + (from b)) * 2
≡⟨ *-distrib-+ 1 (from b) 2 ⟩
2 + (from b) * 2
≡⟨ cong (\x → 2 + x) (*-comm (from b) 2) ⟩
2 + 2 * (from b)
≡⟨⟩
suc (1 + 2 * (from b))
≡⟨⟩
suc (from (b I))
∎
-- NOTE: Does not hold cause `⟨⟩` isn't equal to canonical zero `⟨⟩ O`
-- to-from-id : ∀ (b : Bin) → to (from b) ≡ b
-- to-from-id ⟨⟩ =
-- begin
-- to (0)
-- ≡⟨⟩
-- ⟨⟩ O
-- ≡⟨⟩
-- ⟨⟩
-- ∎
-- to-from-id (b O) = {!!}
-- to-from-id (b I) = {!!}
from-to-id : ∀ (m : ℕ) → from (to m) ≡ m
from-to-id zero = refl
from-to-id (suc m) =
begin
from (to (suc m))
≡⟨⟩
from (inc (to m))
≡⟨ from-inc-suc-from (to m) ⟩
suc (from (to m))
≡⟨ cong suc (from-to-id m) ⟩
suc m
∎
```
## Standard library
Definitions similar to those in this chapter can be found in the standard library:
```agda
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 (`′ ″ ‴ ⁗`).