In ExtrOcamlNatInt, it is mentioned that:

Disclaimer: trying to obtain efficient certified programs by extracting nat into int is definitively

nota good idea:

But upon going to the https://coq.inria.fr/doc/V8.18.0/stdlib/Coq.extraction.ExtrOcamlZInt.html, the same comment is present.

In ExtrOcamlNatInt, it was also mentioned that:

For serious use of numbers in extracted programs, you are advised to use either coq advanced representations (positive, Z, N, BigN, BigZ) or modular/axiomatic representation.

I suppose `int`

not being infinite is the problem?

What are the other ways to mitigate this? And what does modular/axiomatic representation involve?

Could this be related? https://compcert.org/doc/html/compcert.lib.Integers.html

But that still seem to be using `Z`

, but with a proof that it is within a bound.

modular means to use one of the cyclic groups, like Z/(2^63)Z. There are many ways to do this. Using a bounded subset of Z is one. Another is to just declare axioms, although they wouldn't compute. Now there is a native axiomatization which does compute. https://coq.inria.fr/doc/V8.18.0/stdlib/Coq.Numbers.Cyclic.Int63.Uint63.html

Last updated: Jun 23 2024 at 05:02 UTC