17.4 Some examples

We present here two examples of extractions, taken from the Coq Standard Library. We choose Objective Caml as target language, but all can be done in the other dialects with slight modifications. We then indicate where to find other examples and tests of Extraction.

17.4.1 A detailed example: Euclidean division

The file Euclid contains the proof of Euclidean division (theorem eucl_dev). The natural numbers defined in the example files are unary integers defined by two constructors O and S:
Coq < Inductive nat : Set := O : nat | S : nat -> nat.

This module contains a theorem eucl_dev, and its extracted term is of type
(b:nat)(gt b O)->(a:nat)(diveucl a b)
where diveucl is a type for the pair of the quotient and the modulo. We can now extract this program to Objective Caml:

Coq < Require Euclid.

Coq < Extraction Inline Wf_nat.gt_wf_rec Wf_nat.lt_wf_rec. 

Coq < Recursive Extraction eucl_dev.
type sumbool =
  | Left
  | Right
type nat =
  | O
  | S of nat
type diveucl =
  | Divex of nat * nat
let rec minus n m =
  match n with
    | O -> O
    | S k -> (match m with
                | O -> S k
                | S l -> minus k l)
let rec le_lt_dec n m =
  match n with
    | O -> Left
    | S n0 -> (match m with
                 | O -> Right
                 | S n1 -> le_lt_dec n0 n1)
let le_gt_dec x x0 =
  le_lt_dec x x0
let rec eucl_dev b a =
  match le_gt_dec b a with
    | Left ->
        let Divex (x, x0) = eucl_dev b (minus a b) in Divex ((S x), x0)
    | Right -> Divex (O, a)

The inlining of gt_wf_rec and lt_wf_rec is not mandatory. It only enhances readability of extracted code. You can then copy-paste the output to a file euclid.ml or let Coq do it for you with the following command:

Coq < Extraction "euclid" eucl_dev.

Let us play the resulting program:

# #use "euclid.ml";;
type sumbool = Left | Right
type nat = O | S of nat
type diveucl = Divex of nat * nat
val minus : nat -> nat -> nat = <fun>
val le_lt_dec : nat -> nat -> sumbool = <fun>
val le_gt_dec : nat -> nat -> sumbool = <fun>
val eucl_dev : nat -> nat -> diveucl = <fun>
# eucl_dev (S (S O)) (S (S (S (S (S O)))));;
- : diveucl = Divex (S (S O), S O)
It is easier to test on Objective Caml integers:
# let rec i2n = function 0 -> O | n -> S (i2n (n-1));;
val i2n : int -> nat = <fun>
# let rec n2i = function O -> 0 | S p -> 1+(n2i p);;
val n2i : nat -> int = <fun>
# let div a b = 
     let Divex (q,r) = eucl_dev (i2n b) (i2n a) in (n2i q, n2i r);;
div : int -> int -> int * int = <fun>
# div 173 15;;
- : int * int = 11, 8

17.4.2 Another detailed example: Heapsort

The file Heap.v contains the proof of an efficient list sorting algorithm described by Bjerner. Is is an adaptation of the well-known heapsort algorithm to functional languages. The main function is treesort, whose type is shown below:

Coq < Require Heap.

Coq < Check treesort.
treesort
     : (A:Set; leA,eqA:(relation A))
        ((x,y:A){(leA x y)}+{(leA y x)})
        ->(eqA_dec:((x,y:A){(eqA x y)}+{~(eqA x y)}))
           ((x,y,z:A)(leA x y)->(leA y z)->(leA x z))
           ->(l:(list A))
              {m:(list A)| (sort leA m) & (permutation eqA_dec l m)}

Let's now extract this function:

Coq < Extraction NoInline list_to_heap.

Coq < Extraction "heapsort" treesort.

One more time, the Extraction NoInline directive is cosmetic. Without it, everything goes right, but list_to_heap is inlined inside treesort, producing a less readable term. Here is the produced file heapsort.ml:

type sumbool =
  | Left
  | Right

type nat =
  | O
  | S of nat

type 'a tree =
  | Tree_Leaf
  | Tree_Node of 'a * 'a tree * 'a tree

type 'a list =
  | Nil
  | Cons of 'a * 'a list

let rec merge leA_dec eqA_dec x x0 =
  match x with
    | Nil -> x0
    | Cons (a, l) ->
        let rec f = function
          | Nil -> Cons (a, l)
          | Cons (a0, l1) ->
              (match leA_dec a a0 with
                 | Left -> Cons (a,
                     (merge leA_dec eqA_dec l (Cons (a0, l1))))
                 | Right -> Cons (a0, (f l1)))
        in f x0

let rec heap_to_list leA_dec eqA_dec = function
  | Tree_Leaf -> Nil
  | Tree_Node (a, t, t0) -> Cons (a,
      (merge leA_dec eqA_dec (heap_to_list leA_dec eqA_dec t)
        (heap_to_list leA_dec eqA_dec t0)))

let rec insert leA_dec eqA_dec x x0 =
  match x with
    | Tree_Leaf -> Tree_Node (x0, Tree_Leaf, Tree_Leaf)
    | Tree_Node (a, t, t0) ->
        let h3 = fun x1 -> insert leA_dec eqA_dec t x1 in
        (match leA_dec a x0 with
           | Left -> Tree_Node (a, t0, (h3 x0))
           | Right -> Tree_Node (x0, t0, (h3 a)))

let rec list_to_heap leA_dec eqA_dec = function
  | Nil -> Tree_Leaf
  | Cons (a, l) ->
      insert leA_dec eqA_dec (list_to_heap leA_dec eqA_dec l) a

let treesort leA_dec eqA_dec l =
  heap_to_list leA_dec eqA_dec (list_to_heap leA_dec eqA_dec l)
Let's test it:

# #use "heapsort.ml";;
type sumbool = Left | Right
type nat = O | S of nat
type 'a tree = Tree_Leaf | Tree_Node of 'a * 'a tree * 'a tree
type 'a list = Nil | Cons of 'a * 'a list
val merge : ('a -> 'a -> sumbool) -> 'b -> 'a list -> 'a list -> 'a list =
  <fun>
val heap_to_list : ('a -> 'a -> sumbool) -> 'b -> 'a tree -> 'a list = <fun>
val insert : ('a -> 'a -> sumbool) -> 'b -> 'a tree -> 'a -> 'a tree = <fun>
val list_to_heap : ('a -> 'a -> sumbool) -> 'b -> 'a list -> 'a tree = <fun>
val treesort : ('a -> 'a -> sumbool) -> 'b -> 'a list -> 'a list = <fun>
One can remark that the argument of treesort corresponding to eqAdec is never used in the informative part of the terms, only in the logical parts. So the extracted treesort never use it, hence this 'b argument. We will use () for this argument. Only remains the leAdec argument (of type 'a -> 'a -> sumbool) to really provide.

# let leAdec x y = if x <= y then Left else Right;;
val leAdec : 'a -> 'a -> sumbool = <fun>
# let rec listn = function 0 -> Nil
                         | n -> Cons(Random.int 10000,listn (n-1));;
val listn : int -> int list = <fun>
# treesort leAdec () (listn 10);;
- : int list = Cons (136, Cons (760, Cons (1512, Cons (2776, Cons (3064, 
Cons (4536, Cons (5768, Cons (7560, Cons (8856, Cons (8952, Nil))))))))))
Some tests on longer lists (10000 elements) show that the program is quite efficient for Caml code.

17.4.3 The Standard Library

As a test, we propose an automatic extraction of the Standard Library of Coq. In particular, we will find back the two previous examples, Euclid and Heapsort. Go to directory
contrib/extraction/test of the sources of Coq, and run commands:
make tree; make
This will extract all Standard Library files and compile them. It is done via many Extraction Module, with some customization (see subdirectory custom).

The result of this extraction of the Standard Library can be browsed at the address:
http://www.lri.fr/~letouzey/extraction
Reals theory is normally not extracted, since it is an axiomatic development. We propose nonetheless a dummy realization of those axioms, to test, run:
make reals
This test works also with Haskell. In the same directory, run:
make tree; make -f Makefile.haskell
The haskell compiler currently used is hbc. Any other should also work, just adapt the Makefile.haskell. In particular ghc is known to work.

17.4.4 Extraction's horror museum

Some pathological examples of extraction are grouped in the file
contrib/extraction/test_extraction.v of the sources of Coq.

17.4.5 Users' Contributions

Several of the Coq Users' Contributions use extraction to produce certified programs. In particular the following ones have an automatic extraction test (just run make in those directories):

Rocq/HIGMAN is a bit particular. The extracted code is normally not typable in ML due to an heavy use of impredicativity. So we realize one inductive type using an Obj.magic that artificially gives it the good type. After compilation this example runs nonetheless, thanks to the correction of the extraction (proof underway).