The Coq mailing list

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

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