Strongly Specified Functions

Submitted by mrd on Sun, 09/23/2007 - 9:37pm.

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 is nil and a proof of this is reversed_nil."

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.

The 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)