Quest 3 - Pi Types
We will try to formulate and prove the statement
Problem statement
The sum of two even naturals is even.
Part 0 - Defining Addition
To do so we must define +
on the naturals.
Addition takes in two naturals and spits out a natural,
so it should have type ℕ → ℕ → ℕ
.
_+_ : ℕ → ℕ → ℕ
n + m = ?
Try coming up with a sensible definition. It may not look the same as ours.
Hint
n + 0
should be n
and n + (m + 1)
should be (n + m) + 1
.
Part 1 - The Statement
Now we can make the statement that a sum of even naturals is even in agda
.
Make sure it is of the form
Name : Statement
Name = ?
The statement should be of the form (x y : A) → B
where A
represents the subset of even naturals
and B
expresses what it means for the “sum of x
and y
” to be even.
Given TipHint
x y : Σ ℕ isEven
we want to show that their sum
(really the sum of their fist components) is even,
so we should give isEven (x .fst + y .fst)
x .fst
is another notation for fst x
.
This works for all sigma types.
There are three ways to interpret this:
For all even naturals Spoiler
x
and y
,
their sum is even.isEven (x .fst + y .fst)
is a construction depending on two recipes
x
and y
.
Given two recipes x
and y
of Σ ℕ isEven
,
we break them down into their first components,
apply the conversion _+_
,
and form a recipe for isEven
of the result.isEven (_ .fst + _ .fst)
is a bundle over the categorical product
Σ ℕ isEven × Σ ℕ isEven
and SumOfEven
is a section of the bundle.
This means for every point (x , y)
in Σ ℕ isEven × Σ ℕ isEven
,
it gives a point in the fiber isEven (x .fst + y .fst)
.
More generally given A : Type
and B : A → Type
we can form the pi type (x : A) → B x : Type
(in other languages Π (x : ℕ), isEven n
),
with interpretations :
it is the proposition “for all
x : A
, we haveB x
”, and each term of the pi type is a collection of proofs ``bx : B x`, one for eachx : A
.recipes of
(x : A) → B x
are made by converting eachx : A
to some recipe ofB x
. Indeed the function typeA → B
is the special case where the typeB x
is not dependent onx
. Hence pi types are also known as dependent function types. Note that terms in the sigma type are pairs(a , b)
whilst terms in the dependent function type are a collection of pairs(a , b)
indexed bya : A
Given the bundle
B : A → Type
, we have the total spaceΣ A B
which is equipped with a projectionfst : Σ A B → A
. A term of(x : A) → B x
is a section of this projection.
We are now in a position to prove the statement. Have fun!
Part 2 - Remarks
Important
Once you have proven the statement,
check out our two ways of defining addition _+_
and _+'_
(in the solutions).
Use
C-c C-n
to check that they compute the same values on different examples.Uncomment the code for
Sum'OfEven
in the solutions. It is justSumOfEven
but with each+
changed to+'
.Load the file. Does the proof still work?
Our proof SumOfEven
relied on
the explicit definition of _+_
,
which means if we wanted to use our proof on
someone else’s definition of addition,
it might not work anymore.
Important Question
But _+_
and _+'_
compute the same values.
Are _+_
and _+'_
“the same”? What is “the same”?