Coq's Extraction feature enables you to write a functional program inside Coq; (presumably) use Coq's logic to prove some correctness properties about it; and translate it into an OCaml (or Haskell) program that you can compile with your optimizing OCaml (or Haskell) compiler. The Extraction chapter of Logical Foundations has a simple example of Coq's program extraction features. In this chapter, we'll take a deeper look.

The Extraction command prints out a function as OCaml code.

You can see the translation of "sort" from Coq to Ocaml, in the "Messages" window of your IDE. Examine it there, and notice the similarities and differences. However, we really want the whole program, including the insert function. We get that as follows:

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:

This is better. 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 time proportional to the difference in value between n and m, which is terrible. We'd like natural numbers to be represented as OCaml int. Unfortunately, there are only a finite number of int values in OCaml (2^31, or 2^63, depending on your implementation); so there are theorems you could prove about some Coq programs that wouldn't be true in OCaml. There are two solutions to this problem:

• Instead of using nat, use a more efficient constructive type, such as Z.
• Instead of using nat, use an abstract type, and instantiate it with OCaml integers.

The first alternative uses Coq's Z type, an inductive type with constructors xI xH etc. Z represents 7 as Zpos (xI (xI xH)), that is, +( 1+2*( 1+2* 1 )). A number n is represented as a data structure of size log(n), and the operations (plus, less-than) also take about log(n) each. Z's log-time per operation is much better than linear time; but in OCaml we are used to having constant-time operations. Thus, here we will explore the second alternative: program with abstract types, then use an extraction directive to get efficiency.

We will be using Parameter and Axiom to axiomatize a mathematical theory without actually constructing it. (You can read more about those vernacular commands in the ADT chapter.) This is dangerous! If our axioms are inconsistent, we can prove False, and from that, anything at all. Here, we axiomatize a very weak mathematical theory: We claim that there exists some type int with a function ltb, so that int injects into Z, and ltb corresponds to the < relation on Z. That seems true enough (for example, take int=Z), but we're not proving it here.

Now, we need to axiomatize ltb so that we can reason about programs that use it. We need to take great care here: the axioms had better be consistent with OCaml's behavior, otherwise our proofs will be meaningless. One axiomatization of ltb is just that it's a total order, irreflexive and transitive. This would work just fine. But instead, I choose to claim that there's an injection from int into Coq's Z type. The reason to do this is then we get to use the omega tactic and other Coq libraries about integer comparisons.

Both of these axioms are sound. There does (abstractly) exist a injective function from "int" to Z, and that function is consistent with the ltb_lt axiom. But you should think about this until you are convinced. Notice that we do not give extraction directives for int2Z or ltb_lt. That's because they will not appear in programs, only in proofs that are not meant to be extracted. You could imagine doing the same thing we just did for (<) with (+), but that would be dangerous:
Parameter ocaml_plus : int → int → int.
Extract Inlined Constant ocaml_plus ⇒ "(+)".
Axiom ocaml_plus_plus: ∀ a b c: int,
  ocaml_plus a b = c ↔ int2Z a + int2Z b = int2Z 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,
int2Z max_int + int2Z max_int = int2Z (ocaml_plus max_int max_int)

which is not true in OCaml, because overflow wraps around, modulo 2^(wordsize-1). So we won't axiomatize OCaml addition. The Coq standard library does have an axiomatization of 31-bit integer arithmetic in the Int31 module at https://coq.inria.fr/distrib/current/stdlib/Coq.Numbers.Cyclic.Int31.Int31.html

Utilities for OCaml Integer Comparisons

In Perm we proved several theorems showing that Boolean operators were reflected in propositions. Below, we do that for ltb, our new, axiomatized less-than operator on int. We also do it for the equality and less-than operators on Z.

SearchTrees, Extracted

Trees, on int Instead of nat

We can easily reprove all the three basic laws about insert, lookup, and empty, mostly just by cut-and-paste from the nat-based versions.

Exercise: 2 stars, standard (lookup_insert_neq)

It is similarly easy to port the definition of BST and re-prove the properties of elements for int-keyed trees. The details are not very interesting, so we omit them here.

Now, run this command and examine the results in the "response" window of your IDE:

Next, we will extract it into an OCaml source file, and measure its performance.

Performance Tests

Let's examine the performance of our extracted binary search tree implementation. In the same directory as this file (Extract.v) you will find an OCaml program named test_searchtree.ml. You can run it using the OCaml toplevel with these commands:

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

On my machine that prints:

Insert and lookup 1000000 random integers in 1.076 seconds.
Insert and lookup 20000 random integers in 0.015 seconds.
Insert and lookup 20000 consecutive integers in 5.054 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 my machine that prints,

Insert and lookup 1000000 random integers in 0.468 seconds.
Insert and lookup 20000 random integers in 0. seconds.
Insert and lookup 20000 consecutive integers in 0.374 seconds.

Why is the performance of the algorithm so much worse when the keys are all inserted consecutively? To examine this, let's compute with some search trees inside Coq. We cannot do this with the search trees defined thus far in this file, because they use a key-comparison function ltb that is abstract and uninstantiated (only during extraction to OCaml does ltb get instantiated). So instead, we'll use the SearchTree module, where everything runs inside Coq.

Now we construct a tree by adding the keys 0..5 in consecutive order. The proof that the tree is not equal to E is unimportant; we just want to manipulate the tree to see its structure.

Look here! The tree is completely unbalanced. Looking up 5 will take linear time. That's why the runtime on consecutive integers is so bad.

To achieve robust performance (that stays N log N for a sequence of N operations, and does not degenerate to N^2), we must keep the search trees balanced. A later chapter, Redblack, implements that idea.