Coq's Extraction feature enables you to write a functional program inside Coq, use Coq's logic to prove some correctness properties about it, and translate it into an OCaml program that you can compile with your optimizing OCaml compiler. Haskell is also supported. The Extraction chapter of Logical Foundations has a simple example of Coq's program extraction features, but it's not required reading. This chapter starts from scratch and goes deeper.

Extraction

As an example, let's extract insertion sort, which we implemented in Sort.

The Extraction command prints out a function as OCaml code.

You can see the translation of sort from Coq to OCaml in your IDE. Examine it there, and notice the similarities and differences. To get the whole program, we need Recursive Extraction:

The first thing you see there is a redefinition of the bool type. But OCaml already has a bool type whose inductive structure is isomorphic. We want our extracted functions to be compatible with, i.e. callable by, ordinary OCaml code. So we want to use OCaml's standard definition of bool in place of Coq's inductive definition, bool. You'll notice the same issue with lists. The following directive causes Coq to use OCaml's definitions of bool and list in the extracted code:

But the program still uses a unary representation of natural numbers: the number 7 is really (S (S (S (S (S (S (S O))))))), which in OCaml will be a data structure that's seven pointers deep. The leb function takes linear time, proportional to the difference in value between n and m. We could instead use Coq's Z, which is a binary representation of integers. But that is logarithmic-time, not constant.

Of course, for that extraction to be meaningful, we would need to prove that sortZ is a sorting algorithm. Other alternatives include:

• Extract nat directly to OCaml int. But int is finite (2^63 in modern implementations), so there are theorems we could prove in Coq that wouldn't hold in OCaml.
• Use Coq's Int63, which faithfully models 63-bit cyclic arithmetic, and extract directly to OCaml int. But that's painful.
• Define and axiomatize our own lightweight abstract type of naturals, but extract it to OCaml int. But, this is dangerous! If our axioms are inconsistent, we can prove anything at all. If they are not faithful to OCaml, our proofs will be meaningless.

Lightweight Extraction to int

We begin by positing a Coq type int that will be extracted to OCaml's int:

We'll abstract OCaml int to Coq Z. Every int does have a representation as a Z, though the other direction cannot hold.

Nothing else is known so far about int. Let's add less-than operators, which are extracted to OCaml's:

Those axioms are sound: OCaml's < and ≤ are consistent with Coq's on any int. Note that we do not give extraction directives for Abs, ltb_lt, or leb_le. They will not appear in programs, only in proofs --which are not meant to be extracted. You could imagine doing the same thing we just did with ( + ), but that would be wrong:
      Parameter ocaml_plus : int → int → int.
      Extract Inlined Constant ocaml_plus ⇒ "( + )".
      Axiom ocaml_plus_plus: ∀ a b c: int,
        ocaml_plus a b = c ↔ Abs a + Abs b = Abs c. The first two lines are OK: there really is a + function in OCaml, and its type really is int → int → int. But ocaml_plus_plus is unsound. From it, you could prove,
      Abs max_int + Abs max_int = Abs (ocaml_plus max_int max_int) which is not true in OCaml because of overflow. In Perm we proved several theorems showing that Boolean operators were reflected in propositions. Below, we do that for int and Z comparisons.

Now we upgrade bdall to work with Z and int.

Insertion Sort, Extracted

We're ready to state insertion sort with int, and to extract it:

Again, for that extraction to be meaningful, we need to prove that sort_int is a sorting algorithm. We can do that with the same techniques we used in Sort. In particular, lia works with Z, so we can enjoy automation without having to do any unnecessary work axiomatizing and proving lemmas about int.

Exercise: 3 stars, standard (sort_int_correct)

Prove the correctness of sort_int by adapting your solution to insertion_sort_correct from Sort. Note that notations such as <=? refer to nat comparisons, so you might need to adjust those in your proof.

Binary Search Trees, Extracted

We can reimplement BSTs with int keys.

Exercise: 1 star, standard (lookup_insert_eq)

Exercise: 2 stars, standard (lookup_insert_neq)

Exercise: 4 stars, standard, optional (int_elements)

Port the definition of BST and re-prove the properties of elements for int-keyed trees. Send us your solution so we can include it! ☐ Now see the extraction in your IDE:

Performance Tests

Let's measure the performance of BSTs. First, we extract to an OCaml file:

Second, in the same directory as this file (Extract.v) you will find the file test_searchtree.ml. You can run it using the OCaml toplevel with these commands:

# #use "searchtree.ml";;
# #use "test_searchtree.ml";;

On a recent machine with a 2.9 GHz Intel Core i₉ that prints:

Insert and lookup 1000000 random integers in .889566 seconds.
Insert and lookup 20000 random integers in 0.009918 seconds.
Insert and lookup 20000 consecutive integers in 2.777335 seconds.

That execution uses the bytecode interpreter. The native compiler will have better performance:

$ ocamlopt -c searchtree.mli searchtree.ml
$ ocamlopt searchtree.cmx -open Searchtree test_searchtree.ml -o test_searchtree
$ ./test_searchtree

On the same machine that prints,

Insert and lookup 1000000 random integers in 0.488973 seconds.
Insert and lookup 20000 random integers in 0.003237 seconds.
Insert and lookup 20000 consecutive integers in 0.387535 seconds.

Of course, the reason why the performance is so much worse with consecutive integers is that BSTs exhibit worst-case performance under that workload: linear time instead of logarithmic. We need balanced search trees to achieve logarithmic. Redblack will do that.