The Coq mailing list

[Yannick Forster <yannick AT yforster.de>]

You can get rid of the lets without changing the code by enabling the 
extraction option "Use linear let reduction" which is disabled by 
default. Like so:


Test Extraction Flag. (* Current value of Extraction Flag is 495 *)
Set Extraction Flag 1007. (* 495 + 512 = 1007 *)
Test Extraction Flag.


The flag mechanism is documented here: 
https://coq.inria.fr/refman/addendum/extraction.html#coq:opt.Extraction-Flag

The relevant option is bit 9 (thus the addition of 512 above).

I'm not sure this always produces what you want, but at least if the 
extracted code does not contain any Coq-lets it might do the job in general.

Best
Yannick

On 15/09/2021 14:27, Dominique Larchey-Wendling wrote:
> Hi Mukesh,
>
> For some reason I do not understand, inlining measure_rect7 in the Coq code
> instead of asking Extraction to inline it removes the unnecessary let-in
> definitions in the extracted Ocaml code, giving out *exactly* what you asked 
> for.
>
> Please see the code below
>
> Best, Dominique
>
> Section binary_gcd.
>
>    Variable (x y : positive).
>
>    Definition binary_gcd (u v g : positive) (a b c d : Z) : Z * Z * positive.
>    Proof.
>      revert g a b c d.
>      refine ((fix binary_gcd u v (H : Acc Pos.lt (Pos.add u v)) { struct H } 
> := _) u v (poslt_wf _)).
>      intros g a b c d.
>      case_eq (poseven u); case_eq (poseven v); intros Hv Hu.
>      + refine (binary_gcd (Pos.div2 u) (Pos.div2 v) _ (Pos.mul 2 g) a b c d).
>        now apply Acc_inv with (1 := H), 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 Acc_inv with (1 := H), 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 Acc_inv with (1 := H), Pos.add_lt_mono_l, poseven_div.
>      + case_eq (u ?= v); intros Huv.
>        * exact (a, b, Pos.mul g v).
>        * refine (binary_gcd u (Pos.sub v u) _ g a b (Z.sub c a) (Z.sub d b)).
>          apply Acc_inv with (1 := H).
>          rewrite Pos.compare_lt_iff in Huv; nia.
>        * refine (binary_gcd (Pos.sub u v) v _ g (Z.sub a c) (Z.sub b d) c d).
>          apply Acc_inv with (1 := H).
>          rewrite Pos.compare_gt_iff in Huv; nia.
>    Defined.
>
> End binary_gcd.
>
>
> ----- Mail original -----
> > De: "mukesh tiwari" <mukeshtiwari.iiitm AT gmail.com>
> > À: "coq-club" <coq-club AT inria.fr>
> > Envoyé: Mercredi 15 Septembre 2021 00:47:53
> > Objet: Re: [Coq-Club] Directing the Coq extraction mechanism to extract a 
> > simple code
>
> > Hi Dominique,
> >
> > Thank you for the excellent answer. I haven't tried Equations for any
> > serious thing, but I will give it a shot and see how the extraction
> > goes.
> >
> >
> > Best,
> > Mukesh
> >
> > On Tue, Sep 14, 2021 at 6:50 PM Dominique Larchey-Wendling
> > <dominique.larchey-wendling AT loria.fr> wrote:
> > > 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.