Proofs-as-programs and extraction in Coq

In Coq so far, you have seen how to define programs (similar to what you would do in OCaml) and how to prove properties, using tactics. In the lesson today, you saw that in fact, there is no difference between programs and proofs! For instance, it means that a proof of A -> B is a program transforming a proof of A intro a proof of B.

A practical application is that you can write proofs using Definition and, conversely, you can write programs using tactics. This last point is very useful to write certified programs: you can at the same time define the program and prove its specification. This is represented in Coq by the notation {p & Q p} which means "the program p such that Q p holds".

After writing such a program using tactics, finish the script with the Defined keyword (instead of Qed), to tell Coq that the proof should not be forgotten but may be used to compute.

Coq also offers the possibility to extract programs into general programming languages, and in particular into OCaml. Once you have defined a certified program {p & Q p}, you can extract the program part p to OCaml. This way, you obtain concrete code which is correct by construction.

Today, you are going to define a certified insert sort program, and to extract it to OCaml. Open the file Insert_Sort.v in Proof General.

Define your first programs using tactics

As a first step, you are going to define the insert sort using tactics, without proving anything about it.

We give you the standard OCaml definition of insert sort, which is composed of two recursive functions: insert inserts an element in a sorted list, and sort actually sorts the list.

We show you how to write insert in Coq using tactics. We give some examples showing that it actually computes this program.

Define the sort function in the same way, and test it on different examples.

Program with specification

We now want to prove that sort indeed sorts its argument when defining it. We first need to express what it means for a list to be sorted: each element is smaller than all the following elements.

We give some properties about the smaller predicate and about natural numbers. In a first time, do not look at the proofs, only at the statements to be able to use them when necessary.

We then define the insert program with the following specification: Definition insert_spec n l : {l' | (forall a, smaller a l -> a <= n -> smaller a l') /\ (sorted l -> sorted l')}. We give you the definition in the base case. Complete the definition in the recursive case.

Define the sort function with its specification.

Extraction

Extract the sort function you have just written in OCaml. Look at the generated OCaml file insert_sort.ml: you observe that the sort_spec function has type nat list -> nat list, the extraction mechanism "forgets" the proof.

Test this code using this OCaml program. You have OCaml on your computers, either directly for Linux and Mac users, or via Cygwin for Windows users. Use this script to compile everything. You can change the example at the end of test_sort.ml.

Complete specification

As you certainly have noticed, our previous specification is not complete: we did not prove that the list we return as anything to do with the initial list. Complete the remaining of the TD, that proves the complete specification of sort. Extract the code in OCaml.