15.2 Some examples

We present here few examples of extractions, taken from the theories library of Coq (into the PROGRAMS directory). We choose Caml Light as target language, but all can be done in the other dialects with slight modifications.

15.2.1 Euclidean division

The file Euclid_prog 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.

To use the proof, we begin by loading the module Extraction and the file into the Coq environment:

Coq < Require Extraction.

Coq < Require Euclid_prog.

This module contains a theorem eucl_dev, and its extracted term is of type (b:nat)(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 Caml Light:

Coq < Write CamlLight File "euclid" [ eucl_dev ].
Warning: The constant nat_rec is expanded.
Warning: The constant sumbool_rec is expanded.
Warning: The constant le_gt_dec is expanded.

This produces a file euclid.ml containing all the necessary definitions until let eucl_dev = ... Let us play the resulting program:

# include "euclid";;
# eucl_dev (S (S O)) (S (S (S (S (S O)))));;
- : diveucl = divex (S (S O), S O)

It is easier to test on Caml Light integers:

# let rec nat_of = function 0 -> O
                          | n -> S (nat_of (pred n));;
# let rec int_of = function O   -> 0
                          | S p -> succ (int_of p);;
# let div a b = match eucl_dev (nat_of b) (nat_of a) with
                  divex(q,r) -> (int_of q, int_of r);;
div : int -> int -> int * int = <fun>
# div 173 15;;
- : int * int = 11, 8

15.2.2 Heapsort

Let us see a more complicated example. The file Heap_prog.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. We first load the files:

Coq < Require Extraction.

Coq < Require Heap_prog.

As we saw it above we have to instantiate or realize by hand some of the Coq variables, which are in this case the type of the elements to sort (List_Dom, defined in List.v) and the decidability of the order relation (inf_total). We proceed as in section 15.1:

Coq < ML Import int : Set.
int imported.

Coq < Link List_Dom := int.
Constant List_Dom linked to int

Coq < ML Inductive bool [ true false ] ==
Coq < Inductive BOOL : Set := TRUE : BOOL
Coq < | FALSE : BOOL.
ML inductive type(s) bool imported.

Coq < ML Import lt_int : int->int->BOOL.
lt_int imported.

Coq < Link inf_total :=
Coq < [x,y:int]Cases (lt_int x y) of
Coq < TRUE => left
Coq < | FALSE => right
Coq < end.
Warning: the variable TRUE starts with upper case in a pattern
Warning: the variable FALSE starts with upper case in a pattern
Constant inf_total linked to [_:int][_:int]left

Then we extract the Caml Light program

Coq < Write CamlLight File "heapsort" [ heapsort ].
Warning: The constant inf_total is expanded.
Warning: The constant is_heap_rec is expanded.
Warning: The constant sort_rec is expanded.

and test it


# include "heapsort";;
# let rec listn = function 0 -> nil
                         | n -> cons(random__int 10000,listn (pred n));;
# heapsort (listn 10);;
- : 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 (100000 elements) show that the program is quite efficient for Caml code.

15.2.3 Balanced trees

The file Avl_prog.v contains the proof of insertion in binary balanced trees (AVL). Here we choose to instantiate such trees on the type string of Caml Light (for instance to get efficient dictionary); as above we must realize the decidability of the order relation. It gives the following commands:

Coq < Require Extraction.

Coq < Require Avl_prog.

Coq < ML Import string : Set.
string imported.

Coq < ML Inductive bool [ true false ] ==
Coq < Inductive BOOL : Set := TRUE : BOOL
Coq < | FALSE : BOOL.
ML inductive type(s) bool imported.

Coq < ML Import lt_string : string->string->BOOL.
lt_string imported.

Coq < Link a := string.
Constant a linked to string

Coq < Link inf_dec :=
Coq < [x,y:string]Cases (lt_string x y) of
Coq < TRUE => left
Coq < | FALSE => right
Coq < end.
Warning: the variable TRUE starts with upper case in a pattern
Warning: the variable FALSE starts with upper case in a pattern
Constant inf_dec linked to [_:string][_:string]left

Coq < Write CamlLight File "avl" [rot_d rot_g rot_gd insert].
The axiom False_rec is translated into an exception.
Warning: The constant eq_rec is expanded.
Warning: The constant inf_dec is expanded.
Warning: The constant bal_rec is expanded.
Warning: The constant avl_rec is expanded.
Warning: The constant avl_ins_rec is expanded.
Warning: The constant h_eqc is expanded.
Warning: The constant h_plusc is expanded.

Notice that we do not want the constants rot_d, rot_g and rot_gd to be expanded in the function insert, and that is why we added them in the list of required functions. It makes the resulting program clearer, even if it becomes less efficient.

Let us insert random words in an initially empty tree to check that it remains balanced:

% camllight
# include "avl";;
# let add a t = match insert a t with
                 h_eq x -> x
               | h_plus x -> x ;;
# let rdmw () = let s = create_string 5 in
                for i = 0 to 4 do
                  set_nth_char s i (char_of_int (97+random__int 26))
                done ; s ;;
# let rec built = function 0 -> nil
                         | n -> add (rdmw()) (built (pred n));;
# built 10;;
- : abe = node ("ogccy", node ("gmygy", node ("cwqug", node ("cjyrc", nil, ...


# let rec size = function
    nil -> 0
  | node(_,t1,t2,_) -> 1+(max (size t1) (size t2)) ;;
# let rec check = function
    nil -> true
  | node(_,a1,a2,_) -> 
         let t1 = size a1 and t2 =size a2 in
         if abs(t1-t2)>1 then false else (check a1) & (check a2) ;;

# check (built 100);;
- : bool = true

Retrieved by Memoweb from http://pauillac.inria.fr/coq/doc/node.3.4.1.html at 8/10/98