To play this document inside your browser use ALT-N and ALT-P.
You can save your edits inside your browser and load them back (edits are also saved when you close the window). Finally you can download the file for offline editing.
Today we learn how to state and prove theorems. We don't do that in the void, nor without a methodology.
We work on top of the Mathematical Components library and we follow the Small Scale Reflection approach using the SSReflect proof language.
The Mathematical Components library can be browsed online. The modules of interest are ssrnat and ssrbool (see the headers for the doc).
The SSReflect proof language (reference manual) is covered in full details by the Mathematical Components book. Here we just cover the basics.
Most of the statements that we consider in Mathematical Components are equalities.
For example, we can equate two expressions representing natural numbers.
Addition is defined as left-associative.
Quantifications can be set as parameters before the colon.
In lesson 1 we have defined many boolean tests that can play the role of (decidable) predicates.
This choice has a deep impact on the proofs we make in lesson 2 and 3 and the way we can form new types in lesson 4.
Booleans can be coerced into statements.
Tests can be turned into statements.
the is_true
coercion
is automatically inserted by Coq.
Equality statement between tests reads as if and only if
.
(_ <= _) && (_ <= _) has a special notation (_ <= _ <= _)
Our statements are programs. Hence they compute!
The by[] tactic solves trivial goal (mostly) by computation.
Fixpoint addn n m := if n is p.+1 then (addn p m).+1 else m.
Fixpoint subn m n : nat := match m, n with | p.+1, q.+1 => subn p q | _ , _ => m end.
Definition leq m n := m - n == 0.
_ < _ is just a notation for _.+1 <= _.
Notice the naming convention.
It is not always the case the computation solves all our problems. In particular here there are no constructors to consume, hence computation is stuck.
To prove negbK we need a case split.
The proof of negbK requires a case analysis: given that b is of type bool, it can only be true or false.
The case: term command performs this proof step.
The constructors of bool have no arguments, but for example the second constructor of nat has one.
In this case one has to complement the command by supplying names for these arguments.
Sometimes case analysis is not enough.
Fixpoint muln (m n : nat) : nat := if m is p.+1 then n + muln p n else 0.
We don't know how to prove this yet. But maybe someone proved it already...
The Search command is quite primitive but also your best friend.
It takes a head pattern, the whildcard _ in the examples above, followed by term or patterns, and finally a location, in this case the ssrnat library.
Our first attempt was unsuccessful because standard properies (associativity, communtativity, ...) are expressed in Mathematical Components using higher order predicates. In this way these lemmas are very consistent, but also harder to find if one does not know that.
The second hit is what we need to complete the proof.
The rewrite tactic uses an equation. If offers many more flags than the ones we will see (hint: check the Coq user manual, SSReflect chapter).
Let's now look at another example to learn more about rewrite.