The Coq mailing list

[mukesh tiwari <mukeshtiwari.iiitm AT gmail.com>]

How to direct the Coq extraction mechanism to avoid the unnecessary
wrapping and unwrapping of existentials and extract the Coq code as it
is?

In most of my work/research, I write Coq code, prove them correct, and
extract OCaml code. So far, I have used dependent types freely and the
extracted OCaml code is littered with "Obj.magic", which is fine
because those parts are not touched at the run time, but say my goal
is to avoid "Obj.magic", for mostly readability purposes. One way to
achieve this is writing a simple function, using Fixpoint or
Definition, but not every terminating function can be written this
way, especially if the termination measure is some combination of
input arguments. So recently, I have found "Program Fixpoint" which
basically solves my problem, except the extraction part. For example,
when I am extracting the "binary_gcd" function (see the code below), I
get two functions "binary_gcd" and "binary_gcd_func" [1]. However, I
feel that wrapping and unwrapping in existentials (ExistsT data type)
are unnecessary in these two functions, so my question is how can I
direct the extraction mechanism to give a code similar to this [2]
(extracted from a similar Coq but for termination it uses nat as
fuel)?


Best,
Mukesh


[1] https://gist.github.com/mukeshtiwari/5e03d736f662188d9b88660b800ef498
[2] 
https://gist.github.com/mukeshtiwari/5e03d736f662188d9b88660b800ef498#file-gcd-ml-L99


Require Import Coq.NArith.BinNat.
Require Import Coq.Program.Wf.
Require Import Coq.ZArith.Zwf.
Local Open Scope positive_scope.

Lemma poslt_wf : well_founded Pos.lt.
Proof.
 unfold well_founded.
 assert (forall x a, x = Zpos a -> Acc Pos.lt a).
 intros x. induction (Zwf_well_founded 1 x);
 intros a Hxa. subst x.
 constructor; intros y Hy.
 apply H0 with y; trivial.
 split; auto with zarith.
 intros. apply H with a.
 exact eq_refl.
Defined.

Definition poseven (a : positive) : bool :=
 match a with
 | xO _ => true
 | _ => false
 end.

Lemma poseven_div : forall p, true = poseven p -> Pos.div2 p < p.
Proof.
 induction p; simpl; intro H; try (inversion H).
 nia.
Qed.


Program Fixpoint binary_gcd (x y : positive) (u v g : positive) (a b c d : Z)
{measure (Pos.add u v) (Pos.lt)} : Z * Z * positive :=
 match poseven u, poseven v with
  | true, true => binary_gcd x y (Pos.div2 u) (Pos.div2 v) (Pos.mul 2 g) a b 
c d
  | true, false =>
      match Z.even a, Z.even b with
      | true, true => binary_gcd x y (Pos.div2 u) v g (Z.div a 2)
(Z.div b 2) c d
      | _, _ => binary_gcd x y (Pos.div2 u) v g (Z.div (a + y) 2)
(Z.div (b - x) 2) c d
     end
  | false, true =>
     match Z.even c, Z.even d with
     | true, true => binary_gcd x y u (Pos.div2 v) g a b (Z.div c 2) (Z.div d 
2)
     | _, _ => binary_gcd x y u (Pos.div2 v) g a b (Z.div (c + y) 2)
(Z.div (d - x) 2)
    end
  | false, false =>
    match u ?= v with
    | Lt => binary_gcd x y u (Pos.sub v u) g a b (Z.sub c a) (Z.sub d b)
    | Eq => (a, b, Pos.mul g v)
    | Gt => binary_gcd x y (Pos.sub u v) v g (Z.sub a c) (Z.sub b d) c d
    end
 end.
 Next Obligation.
  apply Pos.add_lt_mono.
  apply poseven_div; exact Heq_anonymous.
  apply poseven_div; exact Heq_anonymous0.
 Defined.
 Next Obligation.
  apply Pos.add_lt_mono_r.
  apply poseven_div; exact Heq_anonymous1.
 Defined.
 Next Obligation.
  apply Pos.add_lt_mono_r.
  apply poseven_div; exact Heq_anonymous1.
 Defined.
 Next Obligation.
  apply Pos.add_lt_mono_l.
  apply poseven_div; exact Heq_anonymous2.
 Defined.
 Next Obligation.
  apply Pos.add_lt_mono_l.
  apply poseven_div; exact Heq_anonymous2.
 Defined.
 Next Obligation.
  symmetry in Heq_anonymous.
  pose proof (proj1 (Pos.compare_lt_iff u v) Heq_anonymous).
  rewrite Pos.add_sub_assoc, Pos.add_comm, Pos.add_sub.
  apply Pos.lt_add_r. exact H.
 Defined.
 Next Obligation.
  symmetry in Heq_anonymous.
  pose proof (proj1 (Pos.compare_gt_iff u v) Heq_anonymous).
  nia.
 Defined.
 Next Obligation.
  apply measure_wf.
  apply poslt_wf.
 Defined.

Extraction Language OCaml.
Recursive Extraction binary_gcd.