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. `Insert_Sort.v`

in
Proof General.

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.

`sort`

function in the same way,
and

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.

`sort`

function with its
specification.

`sort`

function you have just
written in OCaml. `insert_sort.ml`

: you observe that
the `sort_spec`

function has type ```
nat list -> nat
list
```

, the extraction mechanism "forgets" the proof.

`test_sort.ml`

.

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. `sort`

.