The Coq mailing list

[Suneel Sarswat <suneel.sarswat AT gmail.com>]

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?

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