Strongly Specified Functions
How to make writing easy functions hard.
Kidding aside, a strongly specified function in Coq not only computes but simultaneously provides a proof of some property. The construction of the proof is integrated with the body of the function. This differentiates it from "weakly" specified functions, which are written separately from the proof.
Proving properties about functions is one of the main practical uses of Coq. Unfortunately, it's more difficult than simply writing code. But it is more interesting (and useful) than, say, simple proofs about the monad laws. One thing I learned, the hard way, is that it's better to start small.
The first example to talk about is reverse. It has a simple inductive definition, so that isn't a big deal, like it can be for some things. It uses basic structural induction on lists, so I don't need to define my own well founded induction principle. Hopefully, it illustrates the meaning of "integrated computation and proof."
I've split the property up into two inductive definitions. The first one is the actual "reversed" relation between two lists. Notice that it is not necessarily in
Set. The second definition is what actually gets constructed by the function. It says: in order to construct a reversed list of
xs, you need to supply a list
xs' and a proof of
reversed xs xs'.
The definition is slightly different than other functions you may have seen in Coq (or not). It actually looks more like a theorem proof than a function. This is a good thing.
I use the
refine tactic now extensively. This tactic allows you to specify an exact proof term, like
exact, but also to leave "jokers" to be filled in by further elaboration. The two spots I've left correspond to the base case and the inductive case, which you should be able to figure out from the
match. Side note: the
return type-annotation is necessary, otherwise type reconstruction won't figure it out.
At this point, I've told Coq that there is a
nil case and a "cons" case. The
nil case is easy, so I just supplied an exact proof term. You can read that as saying: "The reverse of
nil and a proof of this is
For the inductive case, I will use
refine again to drill deeper into the function and the proof. Notice that the recursive call is made with
match. This allows me to separate the recursively computed value
xs' from the usage of the induction hypothesis
Hxs'. There is a little trap here -- if you use automation prior to making the recursive call you may get a "Proof completed" message. But you won't be able to save the proof, because the "termination checker" will yell at you. The same thing happens if you incorrectly invoke the recursion.
The "proof completed" message isn't bogus -- it's just that the function the
auto tactic had proven was not the function for which we were looking.
refine statement provides the necessary hint to the theorem prover. I construct the returned data in a separate
refine just to illustrate how you can drill down with the tool. This just leaves the simple proof that
xs'++(x::nil) is in fact, the reverse.
Recursive Extraction pulls out all the computation-related (stuff in
Set) bits while leaving behind the proof-related bits. If you want it in Haskell, as always, change the language with
Extraction Language Haskell.
(All examples were written using Coq 8.1pl1)