Strongly specified function in Coq

After my two previous posts about Coq, I am now ready to write a little about strong specification in Coq. A strongly specified function is a function which is containing its specification in its output type.

1. Definitions

Such a strongly specified function is returning a type which is a pair : (a,P b). It is a dependent type because b is generally dependent on a value of type a. For instance, if a is the type nat and the function is generating 4 for a then the second part of the pair is of type P 4. An element of this type is a proof that 4 is satisfying the property P.

So, a strongly specified function is generating a value (natural, string, list etc...) and a proof that the value is respecting a given specification : the certificate.

We have seen in my previous post that the tools used to generate values (functional programming with let, if, match ...) are not so easy to use for writing a proof because the computational content of a proof is less clear. On the contrary, the tactics used to prove a theorem are not very easy to use for writing an algorithm since you have less control on the computational content of the algorithms generated by the tactics.

So, it looks like we have a problem : we need to mix both approaches in writing a strongly specified function. The refine tactic is used for that. With refine you write your function like in any functional programming language but with some holes (_) for the proof parts. Then, you use tactics to fill the goals.

Before studying an example of strongly specified function we need to see how to write the type. I said it is a pair but it is not written as a pair in Coq. There is some additional syntax.

The pair

(a, P a) 

is written

exist a (P a)

So, pattern matching on "exist" may be needed. Moreover, the exist is generally not written in the type since there is a better syntax :

{a | P a}

It looks like the definition of a subset but it is NOT a subset. {a : nat | P a} is not the subset of natural numbers satisfying P because the elements of that type are a pair containing a natural number and a proof.

It is possible to combine these specifications with other operators. For instance

{a | P a} + {b | Q b} 

In Haskell, it is corresponding to the Either type. But the constructors in Coq are inleft and inright.

2. Example

So, let's see how to define the function decrementing by 1 when the argument is not zero.

The type specifying the function is:

Definition dec (n : nat) : {p : nat | n = p + 1} + {n = 0}.

Either there exist a p such that n = p + 1 which means that n is different from 0 or n is 0 and we return a proof of it.

Entering that definition in Coq is giving a goal to prove:

forall n : nat, {p : nat | n = p + 1} + {n = 0}

Let's use the refine tactic.

refine (fun n:nat => match n return {p : nat | n = p + 1} + {n = 0} with
 | 0 => inright _ _
 | S p => inleft _ (exist _ p _)
end
).

What does it mean ?

The match should be obvious but we also need to specify the return type. I am not yet understanding very well why except that without specifying the type I was not able to complete the proof.

In case the argument is 0, we return the right result corresponding to a proof of n = 0. But, we don't know how to generate a proof of it so we use _. The first _ is for the type. inright, inleft, exist are using a type as a first argument. Coq can infer it automatically so that's why I am always using _ as first argument. The second argument of inright is a proof that n=0.

In case n = p + 1 then p is satisfying the property. So we know we can find a proof of it. We generate a exist _ p _ and we will use tactics to prove the property and fill the last _.

As a result of refine, we get two new goals to prove:

2 subgoals

  n : nat
  ============================
   0 = 0

subgoal 2 is:
 S p = p + 1

First one is easy and solved with tactic: auto.

Second one is more difficult and we need to load a library:

Require Import Arith.

Now, we can use the ring tactic that will do the maths used to prove the equality.

ring.

And the proof is completed.

Qed.

We can now extract our function:

Extraction Language Haskell.
Extraction dec.

dec :: Nat -> Sumor Nat
dec n =
  case n of
    O -> Inright
    S p -> Inleft p

It is using the type sumor (Sumor in Haskell) so we need to extract an Haskell definition for it too:

Extraction sumor.

data Sumor a = Inleft a
             | Inright

And we now have an Haskell function which is respecting the specification.

You can see that the Haskell code is very similar to the code written in the refine tactic. The only difference is that the parts related to the sort Prop (the proofs) have been erased by the extraction process.

(This post was imported from my old blog. The date is the date of the import. The comments where not imported.)

blog comments powered by Disqus