The Coq mailing list

[Dominique Larchey-Wendling <dominique.larchey-wendling AT loria.fr>]

Hi Mukesh,

It is true that it is hard to control Extraction when
using Program Fixpoint. To a lesser extent, this might 
also happen with Equations. Have you tried Equations?

Otherwise, if you want stronger control, I suggest sticking
with low-level tactics (and "refine" which is low-level
but very very handy).

The following extracts nearly as what you want, except for the "let"
definitions. Maybe you do not care about them? I do not really
understand why extraction adds them, they could clearly by inlined. 
The code below is Coq 8.13.

Notice that this definition will not give you the fixpoint equations
from which you can show the correctness of your binary_gcd algorithm 
in Coq. Then I suggest you write a strongly specified binary_gcd
such as:

Definition binary_gcd u v g a b c d : { t : Z * Z * positive | 
binary_gcd_spec u v g a b c d t }.

enriching the definition below, so that you define binary_gcd and prove its 
correctness at the same time. 

Orelse provide a version of binary_gcd_spec as a low-level spec that just 
gives
you the fixpoint equations you need and them you show correctness from there.

In any case, you may need to remember the values of "Z.even a" (and b,c,d)
with a "case_eq (Z.even a)" instead of a simple "match" (case_eq is a shortcut
tactic for "match x as a return x = a -> _ with | ... => fun Heq_xa => _ end")

Best,

Dominique

------------------

Require Import Coq.NArith.BinNat.
Require Import ZArith.Zwf BinPos ZArith Lia.

Section measure_rect7.

  Variable (Y : Type) (R : Y -> Y -> Prop) (Rwf : well_founded R)
           (X1 X2 X3 X4 X5 X6 X7 : Type)
           (m : X1 -> X2 -> X3 -> X4 -> X5 -> X6 -> X7 -> Y)
           (P : X1 -> X2 -> X3 -> X4 -> X5 -> X6 -> X7 -> Type)
           (IHP : forall x1 x2 x3 x4 x5 x6 x7,
                    (forall y1 y2 y3 y4 y5 y6 y7, R (m y1 y2 y3 y4 y5 y6 y7) 
(m x1 x2 x3 x4 x5 x6 x7) -> P y1 y2 y3 y4 y5 y6 y7)
                  -> P x1 x2 x3 x4 x5 x6 x7).

  Definition measure_rect7 x1 x2 x3 x4 x5 x6 x7 : P x1 x2 x3 x4 x5 x6 x7.
  Proof.
    generalize (Rwf (m x1 x2 x3 x4 x5 x6 x7)); revert x1 x2 x3 x4 x5 x6 x7.
    refine (fix loop x1 x2 x3 x4 x5 x6 x7 H := _). 
    apply IHP; intros.
    apply loop, Acc_inv with (1 := H); trivial.
  Defined.

End measure_rect7.

Print measure_rect7.

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) as H.
 { intros x; generalize (Zwf_well_founded (1%Z) x).
   induction 1 as [ x Hx IHx ]; intros a ->. 
   constructor; intros y Hy.
   apply IHx with (2 := eq_refl); trivial.
   split; auto with zarith. }
 intro; apply H with (1 := eq_refl).
Qed.

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.

Section binary_gcd.

  Variable (x y : positive).

  Definition binary_gcd (u v g : positive) (a b c d : Z) : Z * Z * positive.
  Proof.
    revert u v g a b c d.
    apply measure_rect7 with (1 := poslt_wf) (m := fun u v g a b c d => 
Pos.add u v).
    intros u v g a b c d binary_gcd.
    case_eq (poseven u); case_eq (poseven v); intros Hv Hu.
    + apply (binary_gcd (Pos.div2 u) (Pos.div2 v) (Pos.mul 2 g) a b c d).
      now apply Pos.add_lt_mono; apply poseven_div.
    + refine (match Z.even a, Z.even b with
        | true, true => binary_gcd (Pos.div2 u) v g (Z.div a 2) (Z.div b 2) c 
d _
        | _   , _    => binary_gcd (Pos.div2 u) v g (Z.div (a + Zpos y) 2) 
(Z.div (b - Zpos x) 2) c d _
      end); now apply Pos.add_lt_mono_r, poseven_div.
    + refine (match Z.even c, Z.even d with
        | true, true => binary_gcd u (Pos.div2 v) g a b (Z.div c 2) (Z.div d 
2) _
        | _   , _    => binary_gcd u (Pos.div2 v) g a b (Z.div (c + Zpos y) 
2) (Z.div (d - Zpos x) 2) _
      end); now apply Pos.add_lt_mono_l, poseven_div.
    + case_eq (u ?= v); intros Huv.
      * exact (a, b, Pos.mul g v).
      * apply (binary_gcd u (Pos.sub v u) g a b (Z.sub c a) (Z.sub d b)).
        rewrite Pos.compare_lt_iff in Huv; nia.
      * apply (binary_gcd (Pos.sub u v) v g (Z.sub a c) (Z.sub b d) c d).
        rewrite Pos.compare_gt_iff in Huv; nia.
  Defined.

End binary_gcd.

Require Import Extraction.

Extraction Inline measure_rect7.

Extraction binary_gcd.



----- Mail original -----
> De: "mukesh tiwari" <mukeshtiwari.iiitm AT gmail.com>
> À: "coq-club" <coq-club AT inria.fr>
> Envoyé: Mardi 14 Septembre 2021 07:20:33
> Objet: [Coq-Club] Directing the Coq extraction mechanism to extract a 
> simple code

> 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.