A New Extraction for Coq

Pierre Letouzey

LRI, Université Paris Sud Types 2002

Overview

• Principles

• A taste of extraction via one example • Current situation of extraction in Coq Part I: Principles

Previous works

• Paulin / Werner / Filliâtre:

– First CC to F_{ω}, later with inductives

– Prop/Set distinction

– Realizability technics

• Berardi / Boerio / Prost:

– Dead code analysis

– After collapsing, a dummy constant

– Simulation technics

• Pottier: Embedding untyped λ-calculus inside Ocaml • Severi / Szasz: Specification Logic (internal extraction)

Extraction’s principles

In Coq, proofs are λ-terms, reducible via Eval Compute What more do we ask?

• Creation of standalone programs: adding I/O parts • Integration into a larger unproved development ⇒ Translation to real languages: Ocaml & Haskell ⇒ Provide a readable interface (even readable code)

Extraction’s principles

In Coq, proofs are λ-terms, reducible via Eval Compute What more do we ask?

• Speed! ⇒ Deletion of logical & types arguments in proofs

– A proof λ-term has a particular shape: Prop parts – Computing in types doesn’t influence data results

⇒ A modern reduction machine. Two choices: – Design a new one (Benjamin Grégoire)

– Use existant compilers: Ocaml & Haskell

Why a new extraction?

How to use extraction in Coq V6 Coq V7 :

• Restrain yourself:

– nothing in sort Type

– no use of strong elimination

• Have luck: get ML-typable extracted code

• Still have luck: avoid undue exceptions (False_rec issue)

• Be rich/reasonable: avoid stack or memory overflow

The Type universe

                     Type

                 Set       Prop
                 nat       True

An hybrid Coq term:

if b then O else \begin{matrix}True \\ □ \end{matrix}
   :  if b then nat else Prop
   :  Type

Even logical lambdas could be annoying:

[X:Type][f:nat->X][g:X->nat](g (f O))

[X:Type][f:nat->X][g:X->nat](g (f O)) True [_]I [_]O

[X:Type][f:nat->X][g:X->nat](g (f O)) □  [_]I [_]O

[X:Type][f:nat->X][g:X->nat](g (f O)) □  □ [_]O

[X:Type][f:nat->X][g:X->nat](g (f O)) □  □  O

                           (O (□ O))

Part II: One Example

Predecessor: definition via tactics

Definition pred : (n:nat)~(O = n) -> {p:nat|n=(S p)}.
Destruct n;Intros.
Elim H;Trivial.
Exists n0;Trivial.
Defined.

Predecessor: the Coq term

pred = [n:nat]
<[n0:nat]~(0)=n0->{p:nat | n0=(S p)}>
Cases n of
  0 => [H:(~(0)=(0))]
         (False_rec \begin{matrix}\{p:nat | (0)=(S p)\} \\ □ \end{matrix}
           (H (refl_equal nat (0)))

□

| (S n0) =>
       [_:(~(0)=(S n0))]
         (exist \begin{matrix}nat \\ □ \end{matrix} [p:nat](S n0)=(S p) □ n0

           \begin{matrix}(refl_equal nat (S n0)) \\ □ \end{matrix} )

end

Predecessor: expunged term

pred = [n]
Cases n of
  0 => [H]
         (False_rec □
           □)
| (S n0) =>
       [_]
         (exist □ □ n0

           □)

end

An inductive type: sig

Inductive sig [A : Set; P : A->Prop]  : Set :=
      exist : (x:A)(P x)->(sig A P)

Four arguments to exist: □ □ x □.

We remove the useless ones:

type 'a sig =
   Exist of 'a

One more step for sig

type 'a sig =
   Exist of 'a

sig is an inductive singleton (just a container ...) We remove the container:

 'a sig  becomes 'a
 Exist x  becomes x'
 match e with Exist x -> h becomes let x = e' in h'

False_rec: an exception

Inductive False :  Prop :=

No constructor, since it is an empty type

False_rec = [P:Set; f:False]<P>Cases f f of end
          : (P:Set)False->P

In ML, we use an exception:

let False_rec = function __-> assert false

Predecessor: previous version new version

pred = [n]
Cases n of
  0 => [H]
         (False_rec □

         assert false
           □)
| (S n0) =>
       [_]

         \begin{matrix}(exist □ □ n0 \\ n0 \end{matrix}

            □)
end

Predecessor: in Ocaml and Haskell

Ocaml:

let pred = function
   | O -> (fun _-> assert false (* absurd case *))
   | S n0 -> (fun _-> n0)

Haskell:

pred n = case n of
  O -> (\_-> error "absurd case")
  S n0 -> (\_-> n0)

That was state of the art in Coq 7.1...

A post-extraction optimization

We can push lambdas outside the pattern matching. Situation in Coq 7.2 (latest release). Ocaml:

let pred n _= match n with
   | O -> (fun _-> assert false (* absurd case *)) assert false (* absurd case *)

   | S n0 -> {(fun _-> n0) \atop n0}

Haskell: Same.

And what about types?

Note that produced terms may rarely not type-check in ML. Here: Coq type

  (n:nat)~(O = n) -> {p:nat|n=(S p)}

Extracted type

  nat -> □ -> nat

How to produce types without □

let pred n = match n with
   | O -> assert false (* absurd case *)
   | S n0 -> n0

Dangerous!

In Coq, the following is legal:

(pred O)
     : ~O=O->{p:nat | O=(S p)}

It simply waits forever an absurd argument. But in ML, it will raise an exception (cf Coq 6).

How to produce types without □ (2)

In definitions: versions without □ in signature

Later uses: eta-expansion + missing □ lambdas

Instead of pred :  nat -> □ -> nat,
we write \overline{pred} :  nat -> nat

Then

  let b = pred a in ... becomes
  let b = (fun x _-> \overline{pred} x) a in ... or better
  let b = (fun _-> \overline{pred} a) in ...

Harmless for a total application (even advantageous)

How to produce types without □ (3)

But:

When all arguments are □, we cannot remove all of them:

  let False_rec = function __-> assert false

would give

  let \overline{False_rec} = assert false

and raise an exception during definition in Ocaml.

⇒ We leave just one lambda.

Predecessor, final version

In Coq 7.3 (imminent release)

Ocaml:

let pred = function
   | O -> assert false (* absurd case *)
   | S n0 -> n0

Haskell:

pred n = case n of
  O -> error "absurd case"
  S n0 -> n0

Part III: Extraction Current Status

Theoretical results

t \overline{\begin{matrix}⋆ \\ β_{Coq} \end{matrix} ^{}}u

=

[figure: E(t); \begin{matrix}⋆ \\ β_{X} \end{matrix}; u]

Conditions: t closed, of a data type like nat, bool, ... Two cases for X:

• Weak reduction + Lazy/CBN/Haskell strategy • Weak reduction + Strict/CBV/Ocaml strategy

What about □ in Ocaml?

Open question: translation of □ in Ocaml: Correction proof uses the rule □ x → □ Two choices:

     fun _... -> ()

or

     let rec f x = f

Implementation status (V7.3)

• Follow closely theoretical stuff (still evolve)

• Around 2500 lines of Ocaml code

• Code optimizations like lambda/case

• Inlining of some constants

• Production of Haskell code: freshly debugged • Efficiency: good, but still to be improved • Readability: better than in Coq 6

Users’ Contributions

See demo 13 contribs with extraction tests including:

• Boolean tautology checkers

• A CC type-checker

• First-Order Unification

• Higman’s Lemma (with one manual Obj.magic) One development too huge: Fundamental Theorem of Algebra

Conclusion

Our new extraction:

• Safer than in Coq 6

• Works on all Coq terms

• As a counterpart, some □ in code (far less in 7.3) Future works:

• Guarantee that extracted programs always type-check • Efficiency: more benchmarking & tests This presentation was powered by

Active-DVI

  (see pauillac.inria.fr/advi)