Before going to the next datatype -- List, let's prove some theorems about Nat, to show off the power of dependent types!
It says,
When doing addition for natural number, the order of the numbers can be changed without changing the answer.
x + y = y + x
We import Nat and add from previous chapter first.
• We also imported zero and add1 to simplify our discussion.
Then we can express the following theorems by a type in our programming language,
For all x and y in Nat, add(x, y) is equal to add(y, x).
• Thanks, George Pólya (1887 – 1985), for your great teachings, and your lovely book "How to Solve It" (1945).
What is the unknown?
We need to prove a theorem in our programming language, the theorem is expressed by a type, and to prove it is to construct an element of that type.
A theorem expressed by a type, is like a puzzle -- a game between us and the type checker.
If we can construct an element of that type, we win!
And we see the type is a pi type, so its element will probably be a function.
The result type of the pi type is constructed by Equal, we might need to use Equal's constructors in our proof.
What are the data?
We have the definition of Nat, we already know a lot about it.
And we have the definition of add, which tall us how the computation of addition is performed, both in the case of zero and in the case of add1.
How should we prove the commutative property of addition in English mathematical prose?
Here is my plan, I want to review the proof in prose, and try to translate it to our programming language.
For all x and y in Nat, add(x, y) is equal to add(y, x).
Proof by mathematical induction over x.
• Base case, suppose x is zero.
It is obvious that

because both sides are equal to y.
• Inductive step, suppose x is add1(prev).
We have inductive hypothesis

We need to prove

If for the left hand side we have

and for the right hand side we have

Then we can use inductive hypothesis to prove

by applying add1 to inductive hypothesis

Now we turn to prove Lemma 1 and Lemma 2.
• Proof of Lemma 1.
It is obvious that

because by the definition of add in the case of add1, we have the following

Q.E.D. Lemma 1.
• Proof of Lemma 2, by mathematical induction over y.
Remind Lemma 2

• Base case, suppose y is zero.
It is obvious that

because both sides are equal to add1(prev).
• Inductive step, suppose y is add1(y_prev).
We have inductive hypothesis

We need to prove

By definition of add in the case of add1, the left hand side is equal to

and the right hand side is equal to

We can prove them equal by applying add1 to inductive hypothesis

Q.E.D. Lemma 2.
Since both Lemma 1 and Lemma 2 are proved, the inductive step of the original proof is finished.
Q.E.D.
The outline of our proof will be
x: Nat, y: Nat,
return induction (x) {
case zero =>
// Base case.
...
// Induction step.
// `almost.prev` is the inductive hypothesis.
...
}
}
Note that, we need to explicitly writing down our motive of this induction, namely
Where the argument is the target of the induction, and the return expression is the return type of the induction, which depends on the target.
We will extract two helper functions, one for the Base case, one for Lemma 2.
Before we dive into them, we need a utility function about Equal first -- equal_map.
It maps a function to the elements on both sides of an Equal type.
Let's practice using it first.
Intuitive, right?
In the chapter Equal Utilities, we will discuss the utility functions about Equal in details.
Base case.
The Base case itself is a meaningful theorem, which reads like
For all x in Nat, add(zero, x) is equal to add(x, zero).
Lemma 2.
The Lemma 2 itself is also a meaningful theorem, which reads like
i.e. the inner add1 applied to the second argument of add, can be moved out of add.
Back to the original proof.
We need two more utility functions about Equal.
Let's practice using them.
equal_swap can swap the left and right hand side of the Equal.
equal_compose can compose two Equals, if the right hand side of the first Equal, matchs the left hand side of the second Equal.
Now we can finish the original proof.
We can import some example Nat to test our proof.
Note that, our function add_is_commutative proves the commutative property of addition for all Nat, while applying the function to specific Nats give us, commutative property of addition for specific Nats.
Some questions for Looking back:
• Can you derive the result differently?
Maybe we can make the Lemma 1 more explicit in our formal proof.
Maybe there are different ways to use the utility functions about Equal.
• Can you see it at a glance?
If we practice our intuition about Equal and inductive, maybe the proof will be more obvious to us.
• Can you use the result, or method, for some other problem?
Maybe we can use similar idea to prove the commutative property of multiplication for natural number.
Phew ~
That's a lot of lemmas and inductions.
Compare our formal proof in programming language, with the proof in English mathematical prose, how do you feel?
Do you find more conciseness and clarity in formal proofs?
Probably not yet.
But you see, when we prove in a programming language, the checker can give us feedback. And we can play with our proofs, apply them and test them. We also can package our works to be imported by others easily.
Proof assistants [programming languages] can be extremely useful, just like musical instrument, you can use it to practise, in the circumstance where you do not have a teacher.