The Coq mailing list

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

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