In ExtrOcamlNatInt, it is mentioned that:
Disclaimer: trying to obtain efficient certified programs by extracting nat into int is definitively not a 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: Oct 13 2024 at 01:02 UTC