The Coq mailing list

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

Thank you Yannick !!

I do not know you could control let-in inlining. But still that does not
explain why inlining the recursor at extraction time adds let-in when
the parameters are compound terms.

Best,

Dominique

----- Mail original -----
> De: "Yannick Forster" <yannick AT yforster.de>
> À: "coq-club" <coq-club AT inria.fr>
> Envoyé: Mercredi 15 Septembre 2021 15:40:40
> Objet: Re: [Coq-Club] Directing the Coq extraction mechanism to extract a 
> simple code

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