Stream: Coq users

Topic: Comment in ExtrOcamlNatInt


view this post on Zulip Julin Shaji (Oct 28 2023 at 16:41):

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?

view this post on Zulip Julin Shaji (Oct 28 2023 at 18:02):


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.

view this post on Zulip Li-yao (Oct 28 2023 at 21:25):

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