AUGER_ExtractionTuto

Here is some test file for the extractor. Feel free to modify it if something is not badly written, or a new feature has been added, or for any other reason (I prefix my pages with "AUGER_" to trivially avoid conflicts with already existing pages, not for ownership mark!).

The documentation can be generated by running "coqc [file.v] && coqdoc -utf8 [file.v]" under POSIX systems; for Windows users, there is probably an alternative.

For those of you who would prefer not to have Obj.magic produced code, but would like to use inversions, refer to EqualityFreeInversion. I do not have time to integrate these ideas, but I guess that if someone has time to do it, it would nicely fit in this tutorial; an other feature I was not aware of when I wrote this tutorial is the "Unset Elimination Scheme", which are quite cumbersome in extracted code.

(** * A small tutorial on extraction to OCaml code from Coq 8.3*)
(**
 This tutorial only contains some hints and examples and is not
 intended to replace the documentation page about
 #<A HREF="Reference-Manual027.html">extraction</A>#.
 This is not very OCaml specific;
 it can also be run with the Haskell extraction for example,
 but comments may be inapropriate.
 Notations are used a lot, to make the code readable,
 so do some #<A HREF="Reference-Manual015.html">trip</A>#
 on notations if you are not very familiar to it.
 This tutorial doesn't use the [Section] mechanism,
 since it is not supported for extraction.
 As I am not used to [Program], I have not used it,
 but I develop here some tools to replace it partially
 (I do not care here of well-foundation for programs).
 The monad system was already used in the Compcert project.
 About the coq version, it is just a hint to tell how old this
 tutorial is, all of this should work on all the 8.x line.
 As making a good tutorial is time consuming, I didn't wrote
 a true tutorial, rather a commented benchmark that the user
 may freely modify for its own tests of the different features.
*)
Require Import Utf8_core.
Set Implicit Arguments.
(** ** Extraction of a type: the [spec] type. *)
(** All OCaml types written without using any library/module/extrnal
    such as [Pervasives] when written in Coq are extracted to identity,
    so there is not a lot to tell about them;
    but things are different when Coq types involves propositions
    and/or dependent types. *)
Module Examples1.
 (** The command to extract a coq definition is [Extraction [ident].];
     you cannot extract terms directly. *)
 Extraction True.
(**
<<
(* True : logical inductive *)
(* with constructors : I *)
>>
*)
 (** When there is some dependence with other terms,
     use [Recursive Extraction [ident].]. *)
 Definition dependent_type : Type
 := ∀ b: bool, if b then unit else bool.
 Recursive Extraction dependent_type.
(**
<<
type __ = Obj.t
type bool =
  | True
  | False
type dependent_type = bool -> __
>>
*)
 Definition false_elim_type := False -> nat.
 Extraction false_elim_type.
(**
<<
type false_elim_type = __ -> nat
>>
*)
 (** One last tricky thing, the extraction makes distinction between
     [Type] and [Set]; I guess it can be considered a bug.
 *)
 Inductive testAB: Type := TestA | TestB.
 Inductive testT: Type := TestT.
 Inductive testS: Set := TestS.
 Inductive test2 (T: Type) := Box: T -> test2 T.
 Definition test2AB := test2 testAB.
 Definition test2T := test2 testT.
 Definition test2S := test2 testS.
 Extraction testAB.
(**
<<
type testAB =
  | TestA
  | TestB
>>
*)
 Extraction test2T.
(**
<<
type test2T = __
>>
*)
 Extraction test2S.
(**
<<
type test2S = testS test2
>>
*)
 (** the polymorphism is not always well managed: *)
 Definition u: Type := ∀ (t: Set), t → t.
 Extraction u.
(**
<<
type u = __ -> __ -> __
>>
*)
End Examples1.
(** So if you don't like generating terms using [Obj.t],
  you need to avoid propositions and term dependent types.
  To do so, we will redefine the [sig] type of Coq,
  so that propositions will be boxed inside of [Type]s.
  Note that [Obj.t] is not something to avoid at all costs,
  I just find it awful in the generated code.
*)
Record spec (T: Type) (Spe: T → Prop): Type := Cast {
  spec_val: T;
  π: Spe spec_val
}.
(** *** The [spec] type *)
Extraction spec.
(**
<<
type 't spec = 't
  (* singleton inductive, whose constructor was cast *)
>>
*)
 (** The extractor is clever enough to see that there is
     no need to box such a type;
     but sadly the specification is not extracted as a comment;
     having a line telling that a specification of the type is
     expected would have been a plus. *)
Notation "{ x : T 'st' Π }" :=
 (spec (fun (x: T) =>  Π))
 (x at level 99, format "'[' {  x  :  T  '/' 'st'  Π  } ']'").
Notation "{ x 'st' Π }" := {x:_ st Π}
 (x at level 99, format "'[' {  x  '/' 'st'  Π  } ']'").
Notation "{ x '&' Π }" :=
 (spec (fun (_: x) => Π))
 (x at level 99, format "'[' {  x  '/' '&'  Π  } ']'").
(** *** The [Cast] constructor *)
Extraction Cast.
(**
<<
type 't spec = 't
  (* singleton inductive, whose constructor was cast *)
>>
*)
 (** There is some confusion here between Coq and OCaml; for OCaml,
     for the extractor, [Cast] is a type constructor,
     so that there is no [cast] function generated, but for Coq,
     [Cast] is both a constructor and its associated function,
     so if you want to extract the [Cast] function you have
     to define it. *)
Notation "{: x :}" := {|spec_val:=x|}.
(** This syntax will mark places where a proof is expected
    inside of refine terms (since the [π] term is not provided).
    So in practice, we will find [{: x (*label to a proof*) :}].
    Thus we can refer us to it inside of our term definitions. *)
Module Examples2.
 Definition cast := Cast.
 Extraction cast.
(**
<<
(** val cast : 'a1 -> 'a1 spec **)
let cast spec_val =
  spec_val
>>
*)
 Definition dummy: {unit & True}.
 refine ( {: tt (*tt is such that err... True *) :} ).
 Proof.
  (*tt is such that err... True *)
  trivial.
 Defined.
 Print dummy.
(**
<<
dummy = {:tt:}
     : { unit & True }
>>
*)
 Extraction dummy.
(**
<<
(** val dummy : unit0 spec **)
let dummy =
  Tt
>>
*)
End Examples2.
(** *** The value projection *)
Extraction spec_val.
Notation "'ν'" := spec_val.
(** The function to give us the value of the [spec] type;
    it will be massively used; and is just the identity function.
    So we do not wish this function to be called in real programs,
    as it is simply the identity, so we prefer to inline it
    everywhere; for that there is the [Extraction Inline [ident].]
    command.
*)
Extraction Inline spec_val.
Module Examples3.
 Definition minus2 (x: nat) (y: {n st ∃ m, x=n+m}): {m st x=(ν y)+m }.
 refine ( {: x-(ν y) (*the minus is well specified*) :} ).
 Proof.
  (*the minus is well specified*)
  destruct y; simpl in *.
  destruct π0.
  subst; simpl.
  induction spec_val0 as [|y H]; simpl.
   now destruct x0; simpl.
  now destruct H; simpl.
 Defined.
 (** It is often a good idea to use the [abstract] tactic,
     as it will use less memory when manipulating the term,
     since the subterm (potentially big) is replaced by a simple
     function call. That is what we will do from now.
     Do not forget to end the definition with [Defined] and not
     [Qed], so it will keep transparent.
     This comment is not specific on extraction, it also holds
     for any function made in Coq, that you want to keep transparent
     (such as intermediary definitions for lemmas).
     Do not complain with the fact that you must prove all in one
     tactic with abstract, others have already complained.
     I also hope that in a near future, this feature will appear.
 *)
 Extraction NoInline spec_val.
 Extraction Examples3.minus2.
 Extraction Inline spec_val.
 Extraction Examples3.minus2.
 (** Maybe is there a bug due to experimental status of extraction
     inside modules *)
End Examples3.
Extraction NoInline spec_val.
Extraction Examples3.minus2.
(**
<<
(** val minus2 : nat -> nat spec -> nat spec **)
let minus2 x y =
  minus x (spec_val y)
>>
*)
Extraction Inline spec_val.
Extraction Examples3.minus2.
(**
<<
(** val minus2 : nat -> nat spec -> nat spec **)
let minus2 x y =
  minus x y
>>
*)
(** *** The proof projection *)
Extraction π.
(**
<<
Warning: The identifier __U03c0_ contains __ which is reserved for the extraction
(** val __U03c0_ : __ **)
let __U03c0_ =
  __
>>
*)
(** The support of Unicode in extraction.
    Such awful terms won't matter, as they are not meant to be extracted.
    It also why I defined a field [spec_val] and not [ν];
    as we may want to use [spec_val] in our functions
*)
(** ** Using monads to manages exceptions *)
(** The [result] type manages exceptions through a monad;
    it a rewritting of the [sum] type. *)
Inductive result (E T: Type): Type :=
| Ok: T → result E T
| Err: E → result E T
.
Notation "[ T ! E ]" :=
 (result E T)
 (format "'[' [  T  '/' !  E  ] ']'").
(** the unit binders *)
Notation "'ret' v" := (Ok _ v) (at level 0).
Notation "'fail' v" := (Err _ v) (at level 0).
(** the binding function of the monad *)
Definition bind (E: Type) (X: Type) (x: [X!E])
                          (Y: Type) (f: X → [Y!E])
: result E Y :=
 match x with
 | ret x => match f x with
            | ret y => ret y
            | fail e => fail e
            end
 | fail e => fail e
 end.
(** we may wish to inline this code,
    so that [do x← t; ret {: ν x :}]
    may be extracted to [t]. *)
Extraction Inline bind.
Notation "a >>= b" := (bind a b) (at level 0).
Notation "a >>: b" := (a >>= (fun _ => b)) (at level 0).
Notation "'do' x ← e ; t" :=
 (e >>= (fun x => t))
 (x ident, at level 0, format
  "'[hv' 'do'  x  ←  e ; '/'   t ']'").
Module Example4.
(*
 Class Acc (X: Type) (P: X → X → Prop) (x: X) := Acc_intro {
   wf: forall y, P x y → Acc X P x
 }.
*)
 Inductive PeanoException: Type :=
 | DivideByZero: PeanoException
 | NegativeNumber: PeanoException
 .
 Fixpoint sub (x y: nat): [{z:nat st y+z=x}!PeanoException].
 refine (
  match y with
  | O => ret {:x (*a trivial proof*):}
  | S y => match x with
           | O => fail NegativeNumber
           | S x => do r ← (sub x y); ret {:ν r (*here we use induction*):}
           end
  end
 ); clear sub.
  (**as sub has been cleared, we can check guardedness once and for all*)
 Guarded.
  (**now time for proofs*)
 Proof.
  (*a trivial proof*)
  clear; abstract (split).
   (**Note that letting the raw term wouldn't have obfuscated the proof term,
      but it is a way to tell the reader of the proof term
      that we produced some propositionnal content;
      of course abstracting this proof or not gives the same extraction code.
      Note also that we cleared our hypothesis before calling
      [abstract]; that is because [abstract] will generalize all
      current hypothesis, even not needed ones.
      If you forgot to clear your hypothesis and used the fix tactic,
      an error will be reported, as you will use a fixpoint not
      using structurally smaller argument! *)
 Proof.
  (*here we use induction*)
  clear;
  abstract ( refine (match π r in _=a
                     return S y0 + ν r = S a
                     with eq_refl => eq_refl _
                     end) ).
   (**Of course, we could have proved it using tactics,
      but we can see what awful subterm we avoid in our final
      term, we are avoiding;
      if you want to use tactics here, you may consider destructuring [r].
      (It is an obvious comment, but the used solution doesn't do it.)*)
 Defined.
 Print sub.
(**The output keeps readable:
<<
sub =
fix sub (x y : nat) : [ { z st y + z = x } ! PeanoException ] :=
  match y as x0 return [ { z st x0 + z = x } ! PeanoException ] with
  | 0 => ret ({:x:})
  | S y0 =>
      match x as x0 return [ { z st S y0 + z = x0 } ! PeanoException ] with
      | 0 => fail (NegativeNumber)
      | S x0 => do r ← sub x0 y0;  (ret ({:ν r:}))
      end
  end
     : ∀ x y : nat, [ { z st y + z = x } ! PeanoException ]
Argument scopes are [nat_scope nat_scope]
>>
*)
 (** Now we can have a lemma, making our function available for recursion *)
(*Instance*)
 Lemma sub_acc (x: nat): Acc (fun y x => ∃ z, (S z)+y=x) x.
 Proof.
  split.
  induction x; simpl in *; intros; destruct H.
   discriminate.
  revert IHx; inversion H; clear; intros.
  split; intros; apply IHx; clear IHx.
  destruct H as [x H]; exists (x0+x); subst.
  now induction x0; simpl in *; [|destruct IHx0].
 Qed.
 (** It is useless to use [abstract] here since it is a lemma which
     will never be unfold (since [Qed] terminated). *)
 Definition div (x y: nat): [{qr st (fst qr)*y+(snd qr)=x}!PeanoException].
 refine (
  match y with
  | O => fail DivideByZero
  | S y => (fix div x (H: Acc _ x): [{_ st _=x }!_] :=
            match H with
            Acc_intro H =>
              match sub x (S y) with
              | ret z => do r ← div (ν z) (H _ _(*wf check*));
                         ret {: let (q, r) := (ν r):nat*nat in
                                (S q, r) (*we really compute quo/rem*):}
              | fail NegativeNumber => ret {: (0, x) (*final step*):}
              | fail e => fail e
              end
            end) x (sub_acc x)
  end
 ); clear div H H0.
 Guarded.
 Proof.
  (*wf check*)
  clear -z; abstract (destruct z; eexists; eassumption).
 Proof.
  (*we really compute quo/rem*)
  clear -z r.
  abstract (
   destruct r as [[q r] H]; simpl in *;
   destruct z as [z Hz]; simpl in *;
   subst; clear;
   generalize (q*S y0); clear; intros;
   induction y0; simpl in *; [|destruct IHy0]; split
  ).
 Proof.
  (*final step*)
  simpl; clear.
  abstract ( split ).
 Defined.
 (** Note that the [div] function is not "fully" specified:
     - we have not specified that [DivideByZero] only occurs
       when [y=0]
     - we have not proved that the remain of the division
       is lesser than the divider
     Fully specifying it, would have required a more complex
     monadic system.
     A solution is proposed in the [ExampleFin] module.
  *)
 Definition sub2 := Eval compute in sub.
End Example4.
Extraction Example4.
(**
<<
module Example4 =
 struct
  type coq_PeanoException =
    | DivideByZero
    | NegativeNumber

  (** val sub : nat -> nat -> (coq_PeanoException, nat spec) result **)

  let rec sub x = function
    | O -> Ok x
    | S y0 ->
        (match x with
           | O -> Err NegativeNumber
           | S x0 ->
               (match sub x0 y0 with
                  | Ok x1 -> Ok x1
                  | Err e -> Err e))

  (** val div :
      nat -> nat -> (coq_PeanoException, (nat, nat) prod spec) result **)

  let div x = function
    | O -> Err DivideByZero
    | S y0 ->
        let rec div0 x0 =
          match sub x0 (S y0) with
            | Ok z ->
                (match div0 z with
                   | Ok x1 -> Ok (let Pair (q, r) = x1 in Pair ((S q), r))
                   | Err e -> Err e)
            | Err e ->
                (match e with
                   | DivideByZero -> Err e
                   | NegativeNumber -> Ok (Pair (O, x0)))
        in div0 x

  (** val sub2 : nat -> nat -> (coq_PeanoException, nat spec) result **)

  let rec sub2 x = function
    | O -> Ok x
    | S y0 -> (match x with
                 | O -> Err NegativeNumber
                 | S x0 -> sub2 x0 y0)
 end
>>
*)
(**Some interesting facts:
-the coq function is not tail-recursive
 (since we must cast its specification,
  so we have to destructure the result of the recursion
  to produce our result),
 but the extractor has some optimizations,
 which analyze the code and see that the destructured term is
 equal to the result, so it doesn't have to perform case analysis,
 and the function become tail-recursive
 (at least in [sub2]; for [sub] it seems to be a glitch with
 the [Extraction Inline bind.], since expanding the definition of
 bind in the "do" notation activates this optimization).
-no [Obj.t] is created; that is because we boxed all our propositionnal
 contents into [Type], and did not used dependant types outside of
 these boxes
-all upper-cased definitions are prefixed by "coq_" and
 all lower-cased constructors by "Coq_"
 to fit OCaml requirements; and sometimes numbered to avoid conflicts,
 we will see in next section how to fix it. *)
(** ** Code Tuning for OCaml *)
(** First some warning, this featuren is inherently unsafe,
    so using it needs some extra care!
    All the basic commands for extraction is ok when you don't need
    external libraries, but if you want some efficient code, you may
    want to use [int] instead of the extracted version of [Z];
    use [unit] instead of [unit0], ...
    An other thing is how to avoid generating useless stuff,
    such as induction principles for dummy types.
    And a last thing is how to instantiate axioms.
    All this tuning should be done in a separate file (e.g. "Extraction.v"),
    as well as all the [Extraction Library.] commands.
    This makes things easier to maintain, and don't mess with coq code.
*)
(** *** Using OCaml inductive types *)
(** First, for some basic types, you have the mentionned libraries of
    the extraction chapter of the coq reference manual.
    These are located in the "plugins/extraction" of your coq installation
    directory; if you have the sources, search for the "*.v" files,
    else for the "*.vo" files and run "Require [Lib]. Print [Lib]."
    to know its contents.
    For the lazy guy, here are the libraries:
    Require ExtrOcamlBasic.
    Require ExtrOcamlBigIntConv.
    Require ExtrOcamlIntConv.
    Require ExtrOcamlNatBigInt.
    Require ExtrOcamlNatInt.
    Require ExtrOcamlString.
    Require ExtrOcamlZBigInt.
    Require ExtrOcamlZInt.
    The features of extraction to already defined OCaml types
    are only useful for external or native types like [int];
    else remember to follow OCaml conventions in naming
    types and constructors, and the extraction should be
    straight forward without even identifiers renaming.
    The examples I put can already be found in the reference
    manual; I put it them here, so you won't have to copy paste them.
*)
Module Example5.
 (** Here is a practical example: *)
 Fixpoint sigma l :=
  match l with
  | nil => 0
  | cons (q, n) l => (q*n)+(sigma l)
  end.
  Extraction sigma.
(**
<<
(** val sigma : (nat, nat) prod list -> nat **)
let rec sigma = function
  | Nil -> O
  | Cons (y, l0) -> let Pair (q, n) = y in plus (mult q n) (sigma l0)
>>
*)
 (** So that [unit] is extracted to [unit] and not [unit0] *)
 Extract Inductive unit => "unit" [ "()" ].
 (** So that [bool] is extracted to [bool] and not [bool0];
     note that you have no obligation to give constructors
     beginning with an uppercase. *)
 Extract Inductive bool => "bool" [ "true" "false" ].
 (** But using a constant symbol
     instead of a constructor is not a thing to do!
     (At least if you want to do things in a clean way.)
     In the following example, although [nat] is extracted
     to [int], your program won't be faster, as subtraction
     will be done in a peano maneer and not using the
     [(-)] operator of OCaml; to avoid that you can
     use [Extract Constant minus => "(-)".], but you will
     lose in code confindence, as all your proofs relies
     on another definition for [minus]. *)
 Extract Inductive nat => int [ "0" "succ" ].
 (** You can also extract two types to the same one. *)
 Extract Inductive sumbool => "bool" [ "true" "false" ].
 Extract Inductive list => "list" [ "[]" "(::)" ].
 (** For the [prod], you can find a hack in [ExtrOcamlBasic];
     here is the suggestion of the reference manual, ... *)
 Extract Inductive prod => "(*)" [ "(,)" ].
 (** and here the one of the library: *)
 Extract Inductive prod => "(*)" [ "" ].
 (** Here is a practical example: *)
  Extraction sigma.
(**
<<
(** val sigma : (int*int) list -> int **)
let rec sigma = function
  | [] -> 0
  | y::l0 -> let (q, n) = y in plus (mult q n) (sigma l0)
>>
*)
End Example5.
(** *** Not generating useless stuff *)
(** When defining an inductive, some functions pollute your code;
    and you have no way to remove them.
    If you really don't want to have them, there are two solutions:
    - for non recursive types like [bool], you can define them
      as [CoInductive bool := True | False.];
      - the bad point in
        doing that is that your code will be messed with the [Lazy]
        module; but you won't generate [bool_rec] and [bool_rect]
        which are pretty useless (of course, [bool_ind] is not generated).
        I think that for these types, Coq shouldn't provide these functions,
        as nobody will perform a [induction b.] when [b] is a [bool];
        but will rather use [case b.] or [destruct b.] (at least, it is
        what I do).
      - the good point is that it is easy to put in place.
    - in any case, you can define the inductive out of any submodule,
      then as [Recursive Extraction.] will extract only usefull stuff,
      it won't extract these principles in the extracted code.
      - the bad point is that you cannot put the inductive inside
        of a submodule (since the whole module will be considered usefull).
      - the gool point is that it really does what you want.
    There is also a [Extraction Implicit]. command
    to avoid generating useless arguments for the
    extracted code.
*)
Module Example6.
 CoInductive bool1 := True1 | False1.
 Module Bool2.
  Inductive bool2 := True2 | False2.
 End Bool2.
 Inductive bool3 := True3 | False3.
 Module Tests.
  Definition test1 t := match t with True1 => 0 | _ => 1 end.
  Definition test2 t := match t with Bool2.True2 => 0 | _ => 1 end.
  Definition test3 t := match t with True3 => 0 | _ => 1 end.
 End Tests.
 Extraction Tests.
(**
<<
type bool1 = __bool1 Lazy.t
and __bool1 =
  | True1
  | False1
module Bool2 =
 struct
  type bool2 =
    | True2
    | False2

  (** val bool2_rect : 'a1 -> 'a1 -> bool2 -> 'a1 **)

  let bool2_rect f f0 = function
    | True2 -> f
    | False2 -> f0

  (** val bool2_rec : 'a1 -> 'a1 -> bool2 -> 'a1 **)

  let bool2_rec f f0 = function
    | True2 -> f
    | False2 -> f0
 end
type bool3 =
  | True3
  | False3
module Tests =
 struct
  (** val test1 : bool1 -> int **)

  let test1 t =
    match Lazy.force
    t with
      | True1 -> 0
      | False1 -> succ 0

  (** val test2 : Bool2.bool2 -> int **)

  let test2 = function
    | Bool2.True2 -> 0
    | Bool2.False2 -> succ 0

  (** val test3 : bool3 -> int **)

  let test3 = function
    | True3 -> 0
    | False3 -> succ 0
 end
>>
*)
End Example6.
(** *** The remaining commands to extract code and avoid naming conflicts *)
(** Up to now, we have extracted code to Coq toplevel, but if we want
    some extraction to real "*.ml" files, commands like
    "coqc file.v > file.ml" won't work in most cases, so you need to
    put in your "Extract.v" file all the libraries you want to extract.
    As this tutorial is meant to be runned in a toplevel, I won't use
    these commands, only mention them in this comment;
    the user will be free to uncomment it and try it
    Extraction "coq.ml" Examples1 Examples2 Examples3.
    Require List.
    Extraction Library List.
    The first line will produce a "coq.ml" file containing both
    some of our "Examples" modules; as well as a "coq.mli".
    The third line will produce a "List.ml" file containing only
    the [List] module.
    Note that the file names have an uppercase.
    If you have a lot of libraries to extract,
    you can use the [Recursive Extraction Library [ident].].
    As coq is not aware of the "*.{ml,mli}" files of your program,
    it isn't able to avoid automatically conflicts.
    So a good thing to add in your [Extraction.v] file is a list
    of all used symbols in the program which may enter in conflict
    with generated ones.
    Symbols under ML modules which are not opened are naturally
    protected, so you just have to inform the extractor of
    all the (non-opened) used modules and constants with
    the [Extraction Blacklist [ident].] command.
    This feature is safe of course.
*)
(** ** A final example *)
Module ExampleFin.
 (** This time, we want back-tracking exceptions *)
 Notation "'do_' x ← e ; t" :=
  ( match e with
  | ret x => match t with
             | ret y => ret y
             | fail y => fail y
             end
  | fail y => fail {: ν y :}
  end)
  (x ident, at level 0, format
   "'[hv' 'do_'  x  ←  e ; '/'   t ']'").
 (** As #<A HREF="Reference-Manual.html">classes</A># are not
     extracted to first-class modules, we use a module type
     for them.
 *)
 Module Type Exception.
  Parameter t: Type.
  Parameter dom: Type.
  Parameter exn_spec: t → dom → Prop.
 End Exception.
 Module Exn (E: Exception).
  Definition exn d := {e st E.exn_spec e d}.
 End Exn.
 (** This time, we do not make a big type for all exception,
     as each exception has a domain. *)
 Inductive subException: Set := NegativeNumber.
 Module SubException. (*: Exception*)
  Definition t := subException.
  Definition dom := (nat * nat)%type.
  Definition exn_spec (nn: t) d := ∃ t, (fst d) + S t = (snd d).
 End SubException.
 Module SubExn := Exn SubException.
 (** Remember to use [Set] and not [Type] here! *)
 Fixpoint sub (x y: nat): [{z:nat st y+z=x}!SubExn.exn (x,y)].
 refine (
  match y as y0 return [{_ st y0+_=_} ! SubExn.exn (_,y0)] with
  | O => ret {:x (*a trivial proof*):}
  | S y => match x as x0 return [{_ st _=x0} ! SubExn.exn (x0,_)] with
           | O => fail {: NegativeNumber (*y is bigger than x*):}
           | S x => do_ r ← (sub x y);
                    (*back-track of the exception*)
                    ret {:ν r (*here we use induction*):}
           end
  end
 ); clear sub.
 Guarded.
 Proof.
  (*a trivial proof*)
  clear; abstract (split).
 Proof.
  (*y is bigger than x*)
  clear; simpl; abstract ( exists y0; simpl; split ).
 Proof.
  (*here we use induction*)
  clear; abstract ( now destruct r; subst ).
 Proof.
  (*back-track of the exception*)
  clear -y1;
  abstract ( now destruct y1 as [w [t H]]; exists t; simpl in *; subst ).
 Defined.
 (** Our second exception *)
 Inductive divideException: Set := DivideByZero.
 Module DivException.
  Definition t := divideException.
  Definition dom := nat.
  Definition exn_spec (t: divideException) d := d = 0.
 End DivException.
 Module DivExn := Exn DivException.
 Definition div (x y: nat)
 : [{qr st (fst qr)*y+(snd qr)=x ∧ ∃ t, (snd qr)+(S t) = y}
   !DivExn.exn y].
 refine (
  match y as y0 return [{_ st _}!DivExn.exn y0] with
  | O => fail {: DivideByZero (*y is 0*):}
  | S y => let r :=
           (fix div x (H: Acc _ x)
           : {qr st (fst qr)*(S y)+(snd qr)=x ∧ ∃ t, (snd qr)+(S t) = (S y)} :=
            match H with
            Acc_intro H =>
              match sub x (S y) with
              | ret z => let qr := (div (ν z) (H _ _(*wf check*))) in
                         {: (S (fst (ν qr)), (snd (ν qr)))
                            (*we really compute quo/rem*):}
              | fail {: NegativeNumber :} => {: (0, x) (*final step*):}
              end
            end) x (Example4.sub_acc x)
            in ret {: ν r (*we conclude*):}
  end
 ); try clear div H H0.
 Guarded.
 Proof.
  (*y is 0*)
  clear; abstract ( split ).
 Proof.
  (*wf check*)
  clear -z; abstract (destruct z; eexists; eassumption).
 Proof.
  (*we really compute quo/rem*)
  clear -z;
  abstract (
   simpl; destruct qr as [[q r] [H1 H2]]; simpl in *;
   split; [
    destruct z as [z Hz]; simpl in *;
    subst; clear;
    generalize (q*S y0); clear; intros;
    induction y0; simpl in *; [|destruct IHy0]; split|
  assumption
  ]).
 Proof.
  (*final step*)
  simpl in *; clear - π0.
  abstract ( now split ).
 Proof.
  (*we conclude*)
  clear -r; abstract ( now destruct r; simpl in * ).
 Defined.
End ExampleFin.
Extraction ExampleFin.
(**
<<
(** val fst : ('a1*'a2) -> 'a1 **)
let fst = function
  | (x, y) -> x
(** val snd : ('a1*'a2) -> 'a2 **)
let snd = function
  | (x, y) -> y
type 't spec = 't
  (* singleton inductive, whose constructor was Cast *)
type ('e, 't) result =
  | Ok of 't
  | Err of 'e
module ExampleFin =
 struct
  module type Exception =
   sig
    type t

    type dom
   end

  module Exn =
   functor (E:Exception) ->
   struct
    type exn = E.t spec
   end

  type subException =
    | NegativeNumber

  (** val subException_rect : 'a1 -> subException -> 'a1 **)

  let subException_rect f s =
    f

  (** val subException_rec : 'a1 -> subException -> 'a1 **)

  let subException_rec f s =
    f

  module SubException =
   struct
    type t = subException

    type dom = int*int
   end

  module SubExn = Exn(SubException)

  (** val eq_rew_dep : 'a1 -> 'a2 -> 'a1 -> 'a2 **)

  let eq_rew_dep x f y =
    f

  (** val sub : int -> int -> (SubExn.exn, int spec) result **)

  let rec sub x = function
    | 0 -> Ok x
    | succ y0 ->
        (match x with
           | 0 -> Err NegativeNumber
           | succ x0 -> sub x0 y0)

  type divideException =
    | DivideByZero

  (** val divideException_rect : 'a1 -> divideException -> 'a1 **)

  let divideException_rect f d =
    f

  (** val divideException_rec : 'a1 -> divideException -> 'a1 **)

  let divideException_rec f d =
    f

  module DivException =
   struct
    type t = divideException

    type dom = int
   end

  module DivExn = Exn(DivException)

  (** val div : int -> int -> (DivExn.exn, (int*int) spec) result **)

  let div x = function
    | 0 -> Err DivideByZero
    | succ y0 ->
        let r =
          let rec div0 x0 =
            match sub x0 (succ y0) with
              | Ok z -> let qr = div0 z in ((succ (fst qr)), (snd qr))
              | Err e -> (0, x0)
          in div0 x
        in
        Ok r
 end
>>
*)
(** This time, the bind function was just a notation,
    and the OCaml function is tail recursive without
    the trick of the [Eval compute] *)