Coq : Back To Basics

Before continuing my exploration of the specification and extraction of softwares in Coq, I think I should make a pause and focus a little on Coq basics like the differences between Set and Prop and the meaning of a type like 4>0 ...

In Coq, we have two sorts : Set and Prop. A type of sort Set is a specification and a proof of a specification is a program. A type of sort Prop is a proposition.

Why do we need a sort Prop ? With Set, we already have the proof-as-program correspondence and the type-as-proposition.

We need a sort Set separate from the sort Prop for two main reasons.

1. A program is more than just a proof

A program is indeed a proof of its type but it is much more than that. Let's consider the type:

Int -> Int

From a proof point of view, the previous type is proved by the existence of any program computing an Int from another Int. But, from a computational point of view, those programs are different : they don't compute the same Int or they do not have the same complexity.

So, in Coq when we use the sort Set, proofs (programs) are considered as different even if they prove the same type. For Prop, the details of the programs are not important and we are just interested in the existence of the program.

In practise, it is leading to several differences:

Programs are defined with the keyword Definition. It is just the usual function definition of functional programming. In Haskell you have:

f n = n + 1

In Coq you have:

Definition f n := n + 1.

or

Definition f (n:nat):nat := n+1.

or

Definition f := fun (n:nat) => n+1.

But, proofs of propositions are declared with the keyword pair Theorem/Qed. And, instead of giving the proof as a program using fun, let, match, if .... you use tactics which are like code generators/tranformers.

Indeed, on the proof side, you don't need to know which program is generated. You just need to know that you can generate one program with the right type. So, you use tactics which are helping you to find such a program.

From an algorithmic point of view, tactics can be dangerous since you have no control on the algorithm which is generated. This kind of type driven development is better for proofs. Also, the computational content of a proof is not clear. It would be difficult to find a program just based upon the type.

That's why the code extraction process of Coq is erasing what is related to Prop and is keeping only what is related to Set. Prop is used to specify but has no useful algorithmic content.

Another difference between Definition and Theorem is that a Theorem is opaque. You know that a program is existing but you cannot reuse its code.

In Coq they say you cannot unfold it in another demonstration. In software you would say you cannot inline the function. What is important is the existence of the program not its code.

Let's see one example. The same example on the Set side and on the Prop side.

Definition projection := fun (A B : Set) (H : A * B) => let (x, _) := H in x.

and

Print projection.

is displaying:

projection =
fun (A B : Set) (H : A * B) => let (x, _) := H in x
     : forall A B : Set, A * B -> A

On the Prop side we write:

Lemma proj : forall (A B : Prop), A /\ B -> A.

And now we need to write the program using tactics.

intros A B.
intro H.
elim H.
intros H1 H2.
assumption.
Qed.

And,

Print proj.

is displaying:

proj =
fun (A B : Prop) (H : A /\ B) => and_ind (fun (H1 : A) (_ : B) => H1) H
     : forall A B : Prop, A /\ B -> A

The program is looking similar to the first one. We do not have a let to do the projection but and_ind.

The Coq definition of and is given by:

Inductive and (A B:Prop) : Prop := conj (_:A) (_:B).

So, we see that we need another pattern match on the conj constructor. It is done by and_ind. "Print and_ind" will give you a definition based upon and_rect and "Print and_rect" is giving:

and_rect =
fun (A B : Prop) (P : Type) (f : A -> B -> P) (a : A /\ B) =>
match a with
| conj x x0 => f x x0
end
     : forall (A B : Prop) (P : Type), (A -> B -> P) -> A /\ B -> P

So, now it should look less mysterious. A Theorem in Coq is a function definition ! A function building proofs from other proofs !

2. Meaning of the type 4>0.

Now, we are ready to understand the meaning of the type 4>0. It is of sort Prop. So it is a proposition. A value of a proposition type is a proof of that type ! So, a value of type 4>0 is a proof of 4>0. And we know how we can build functions targetting that type.

So, let's define:

Definition dec (n : nat) (_:n>0) := n-1.

The dec function is requiring two arguments : a natural number n and a value of type n>0. So, the second argument is a proof that n>0. If we want to compute dec with 4 and get 3 we will have to use dec with a proof of 4>0. Let's load the Omega library used for inequalities so that we can easily prove 4>0.

Require Import Omega.
Lemma t : 4 > 0.
omega.
Qed.

t is a proof of 4 > 0 so it is a value of type 4 > 0 and we can use it as second argument of dec.

We can check it and apply dec on 4:

Eval compute in (dec 4 t).

You get 3.

3. Last difference between Set and Prop

There is another big difference between Prop and Set. Prop is impredicative. When defining a new proposition involving a forall quantifier on propositions, the forall is refering to all propositions even the one being defined. This circularity is very powerful and is allowing to define logical connectives from just a very limited set.

So, now that the meaning of Prop, Theorems and types like 4>0 is clearer for you (and for me), next posts will be more practise oriented and we will see how to mix Set and Prop in the same program : a strongly specified function.

(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