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.
It is not surprising one can equate two numbers.
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.
More statements using equality and predicates in bool
Notice that in the first statement = really means
if and only if
.
The last statement is valid thanks to the is_true
coercion
automatically inserted by Coq.
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.
Notice _ < _ 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.
We learn two tactics. move=> names to introduce hypotheses in the context. apply: term to backchain.
Remark dvdn_addr is an iff used inside a context.
Remark // in rewrite to solve simple goals.
Remark rewrite acepts many rewrite rules.
Remark n <= m <= p is n <= m && m <= p.
This slide corresponds to section 2.3.3 of the Mathematical Components book
The elim: tactic is like case: but gives you an induction hypothesis.
The first pitfall when proving programs by induction is not generalizing enough the property being proved before starting the induction.
This slide corresponds to section 2.3.4 of the Mathematical Components book