# 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`

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)

- mrd's blog
- Login to post comments