List Example for Extracting OCaml from Coq

In this post I will show how to extract a simple list append function written in Coq as OCaml code.

First let us create an inductive type in Coq to define our lists as follows.

Inductive mylist : Type :=

| nil : mylist 

| cons : nat -> mylist -> mylist.

Next, we will define an append function over these lists using the "Function" keyword.

Function myappend (l1:mylist) (l2:mylist) {struct l1} : mylist :=

match l1 with

| nil => l2

| cons x xs => cons x (myappend xs l2)

end.

The append function has a special "struct" which tells Coq that the first argument l1 is the recursive parameter to the function. This is essential as without that Coq will not let you define a function. In this particular case the recursive call is always made on a smaller list thus termination can be proven as an instance of structural recursion. However if we write a function where we want to use more general recursion we have to define a "measure" and prove that it decreases with every recursive call. Once the myappend function is defined in Coq it is easy to state and prove properties about append. The following theorem shows that myappend function is associative. 

Theorem myappend_assoc : forall l1 l2 l3 : mylist , myappend (myappend l1 l2) l3 =

(myappend l1 (myappend l2 l3)).

Proof.

intros.

induction l1.

simpl.

trivial.

simpl.

rewrite IHl1.

trivial.

Qed.

Once we have stated the desired properties and proven their correctness we can also generate OCaml (or Haskell) code from Coq using extraction process. The extraction process will recursively remove the proof terms from the code and convert the program to a corresponding OCaml program. Extraction for the myappend function can be using the following statements in Coq.

Extraction Language Ocaml.

Extraction "mylist.ml" myappend.

The generated code in mylist.ml file looks as below.

type nat =

| O

| S of nat

type mylist =

| Nil

| Cons of nat * mylist

(** val myappend : mylist -> mylist -> mylist **)

let rec myappend l1 l2 =

match l1 with

| Nil -> l2

| Cons (x, xs) -> Cons (x, (myappend xs l2))

The OCaml code extracted from Coq includes all the corresponding data types - nat and mylist used in the program. Also the function myappend is extracted without the proof of termination. Other proof constructs like theorems are also dropped from the extracted code. The extracted code can now be used inside a larger OCaml program.