The Coq mailing list

[Frédéric Besson <frederic.besson AT inria.fr>]

On Sat, 2021-01-23 at 00:48 +0530, Suneel Sarswat wrote:
> Dear Frédéric,
> I tried following and it worked without
> Coq.extraction.ExtrOcamlNatInt, but I am still not sure if I can call
> my program certified?

I don't know what is the consensus in the community.
What is for sure is that there are inputs for which the Coq and the
Ocaml code do not compute the same value - in case of overflow.
I would not fly a plane with such "certified" code!

Best,
--
Frédéric

> Require Import ExtrOcamlBasic.
> Require Import ExtrOcamlString.
> 
> Extract Inductive bool => "bool" [ "true" "false" ].
> Extract Inductive nat => "int"
>   [ "0" "(fun x -> x + 1)" ]
>   "(fun zero succ n -> if n=0 then zero () else succ (n-1))".
> Extract Constant plus => "( + )".
> Extract Constant mult => "( * )".
> Extract Constant Nat.eqb => "( = )".
> Extract Constant Nat.leb => "(<=)".
> Extraction  Language OCaml.
> Recursive Extraction Process.
> 
> On Sat, Jan 23, 2021 at 12:42 AM Frédéric Besson <
> frederic.besson AT inria.fr> wrote:
> > Hello,
> > 
> > I would extract to arbitrary precision integers e.g., using the
> > zarith
> > library. As zarith Z.t implements Z and not N, a thin layer will
> > sometimes be needed.
> > For instance, minus : nat -> nat -> nat would be extracted to
> > (fun (x y:Z.t) -> Z.max Z.zero (Z.minus x y))
> > 
> > The technique you mention "Lightweight Extraction to int" is
> > probably
> > also needed on the Coq side (but extract int to Z.t) -- or you need
> > to
> > keep nat morally abstract everywhere on the Coq side e.g., no
> > pattern
> > matching.
> > 
> > Good luck,
> > --
> > Frédéric
> > 
> > 
> > On Sat, 2021-01-23 at 00:14 +0530, Suneel Sarswat wrote:
> > > Dear Members,I am not sure if this question is properly posed. 
> > > 
> > > I have a coq program and its proof.
> > > Now I want to run and test the extracted OCaml code on real
> > data. 
> > > The coq project is completed using natural numbers since the real
> > > problem only involves natural numbers.
> > > In the real data sets the numbers can be as large as millions.
> > > 
> > > In the extracted OCaml code the nat, bool and the list has
> > symbolic
> > > representation besides it is doing unary operations for add,
> > mult,
> > > leb, eqb, sub. 
> > > In order to use the OCaml code I used the library
> > > Coq.extraction.ExtrOcamlNatInt but it has a disclaimer 
> > > "trying to obtain efficient certified programs by
> > > extracting nat into int is definitively *not* a good idea:"
> > > Can I call my program certified? Is there a better solution?
> > > Besides this, the above library does not convert eqb and leb for
> > > some reason?? So, I am doing it like this
> > > 
> > > Extract Constant Nat.eqb => "( = )".
> > > Extract Constant Nat.leb => "( <= )".
> > > 
> > > Is this correct? What are the proof obligations, if any?
> > > 
> > > 
> > > I looked possible at solution on net and found a
> > sulution mentioned
> > > 
> > on 
> > https://softwarefoundations.cis.upenn.edu/vfa-current/Extract.html
> > > .
> > > For this, I need to convert my entire project (10k+ lines) from
> > nat
> > > to int! Is there a quick fix?
> > > 
> > > Thanks in advance,
> > > Suneel
> > 
> >