The Coq mailing list

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

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.