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`.
We also know something about the built-in type `Equal`, but maybe we need to learn more about it.
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
``````add(zero, y) = add(y, zero)
``````
because both sides are equal to `y`.
• Inductive step, suppose `x` is `add1(prev)`.
We have inductive hypothesis
``````add(prev, y) = add(y, prev)
``````
We need to prove
``````add(add1(prev), y) = add(y, add1(prev))
``````
If for the left hand side we have
``````add(add1(prev), y) = add1(add(prev, y)) // Lemma 1
``````
and for the right hand side we have
``````add(y, add1(prev)) = add1(add(y, prev)) // Lemma 2
``````
Then we can use inductive hypothesis to prove
``````add1(add(prev, y)) = add1(add(y, prev))
``````
by applying `add1` to inductive hypothesis
``````     add(prev, y)  =      add(y, prev)
``````
Now we turn to prove Lemma 1 and Lemma 2.
• Proof of Lemma 1.
It is obvious that
``````add(add1(prev), y) = add1(add(prev, y))
``````
because by the definition of `add` in the case of `add1`, we have the following
``````add(add1(prev), y) =
``````
Q.E.D. Lemma 1.
• Proof of Lemma 2, by mathematical induction over `y`.
Remind Lemma 2
``````add(y, add1(prev)) = add1(add(y, prev))
``````
• Base case, suppose `y` is `zero`.
It is obvious that
``````add(zero, add1(prev)) = add1(add(zero, prev))
``````
because both sides are equal to `add1(prev)`.
• Inductive step, suppose `y` is `add1(y_prev)`.
We have inductive hypothesis
``````add(y_prev, add1(prev)) = add1(add(y_prev, prev))
``````
We need to prove
``````add(add1(y_prev), add1(prev)) = add1(add(add1(y_prev), prev))
``````
By definition of `add` in the case of `add1`, the left hand side is equal to
``````add1(add(y_prev, add1(prev)))
``````
and the right hand side is equal to
``````add1(add1(add(y_prev, prev)))
``````
We can prove them equal by applying `add1` to inductive hypothesis
``````     add(y_prev, add1(prev)) =       add1(add(y_prev, prev))
``````
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
``````function add_is_commutative(
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
``````(x) => Equal(Nat, add(x, y), add(y, x))
``````
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
For all `x` and `y` in `Nat`, `add(x, add1(y))` is equal to `add1(add(x, y))`.
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 `Equal`s, 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 `Nat`s give us, commutative property of addition for specific `Nat`s.
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.