Extraction

Bas Spitters edited this page Jul 25, 2018 · 18 revisions

(Part of the Coq FAQ)

Program extraction generates a program from a constructive proof. You can extract your programs to Objective Caml, Scheme and Haskell. The extraction function works via an untyped intermediate language CIC_box. Oeuf is a Verified Coq Extraction in Coq.

Resources about Extraction

Tips about Extraction

  • Check the manual pages!
  • Use the Extraction (Inlined) Constant directive for commonly used types (List, String, Ascii, int); it is less reliable than not using it (since you use some axioms, but it improves performances and readability)
  • Check from time to time, that you don't generate some functions of module Obj (for the Ocaml extraction) or unsafeCoerce (for Haskell), if so you may consider rewritting your functions not to contain them (don't worry all with work also with these, but the code won't be as pleasant). For an example, run:
Fixpoint f n :=
 match n with
 | O => nat
 | S n => nat -> (f n)
 end.
Definition sigma: forall n, f n.
 intro n; induction n; simpl.
  exact O.
 intro m.
 destruct n; simpl in *.
  exact m.
 intro o.
 apply IHn.
 exact (m+o).
Defined.
(*Extraction Language Haskell.*)
Recursive Extraction sigma.

In this example using a list of integers and a folding function would not have generated such a thing!

  • Try to follow the conventions of the language (having a type t = Coq_a | Coq_b is not as pleasant as having a type t = A | B, so declare Inductive t: Type := A | B. and not Inductive t: Type := a | b."; note that as non-informative content won't be extracted, you can use lower case for Inductive t: Prop := a | b. and it won't mess with the code.

  • To avoid [type]_ind, [type]_rec and [type]_rect generation for non recursive types (for instance for pairs) you may consider using coinductives.

    In Haskell, it will behave as you want (it is a lazy language after all) but for OCaml, your code will be polluted with the use of Lazy module. A better alternative is to use the following command:

Unset Elimination Scheme.
  • Avoid use of multiple modules with extraction to Haskell, as there will be only one big module containing all.

A good workbench for the last two points is:

Module M.
 Module N.
  CoInductive pair1_type (a b: Type) :=
  | Pair1: a -> b -> pair1_type a b.
  Definition fst1 (a b: Type) (p: pair1_type a b) := let (x, _) := p in x.
  Definition snd1 (a b: Type) (p: pair1_type a b) := let (_, x) := p in x.
 End N.
 Module O.
  Inductive pair2_type (a b: Type) :=
  | Pair2: a -> b -> pair2_type a b.
  Definition fst2 (a b: Type) (p: pair2_type a b) := let (x, _) := p in x.
  Definition snd2 (a b: Type) (p: pair2_type a b) := let (_, x) := p in x.
 End O.
End M.
(*Extraction Language Haskell.*)
Recursive Extraction M.
  • As far as possible, avoid using higher order functions which contains some specification for functions meant to be used by some program
Definition succ_o_f {A: Type} (f: A->{n|1<=n}): A->{n|2<=n}.
intros.
destruct (f X).
exists (S x).
induction l.
left.
right.
exact IHl.
Defined.
Extraction succ_o_f.

does what you expect, but nothing is done to ensure that the f parameter effectively produces a value which is strictly greater than 1. If this was your ultimate goal, then you need some extra care to check that f produces correct values (and tell to do so to the developper; note that no such warning is generated by extraction). If it is not, but that hypothesis is necessary in later functions, you may get an "assert false" triggered later (which is legitime), but not at the place you would have wished.

  • The following definition:
Record unit2 (P: Prop) := { compute: unit; spec: P }.

can help to get rid of the __ in the generated code.

  • You can take a look at this page for a short tutorial (or rather some kind of documented sandbox) on extraction; but it is kind of OCaml oriented tutorial.

  • Contributors are invited to put their own advice here

Clone this wiki locally
You can’t perform that action at this time.
You signed in with another tab or window. Reload to refresh your session. You signed out in another tab or window. Reload to refresh your session.
Press h to open a hovercard with more details.