How does one import native cyclic integers in coq?

Using Coq
1

Hi,
I’m looking to work with native OCaml integers in Coq, with the objective of extracting the program and running it natively.
My problem is that I can’t seem to understand what “Require Import” command to use to import these integers. My understanding is that they are stored in stdlib (as suggested by Standard Library | The Coq Proof Assistant) but all of my attempts (Require Import Numbers, Require Import Int63, etc) have given me the following Error: Cannot find a physical path bound to logical path.

Any hints would be very appreciated.
Best,
MRandl

2

If you look at the page e.g. for Uint63:
https://coq.inria.fr/stdlib/Coq.Numbers.Cyclic.Int63.Uint63.html
you’ll see at the vey top “Library Coq.Numbers.Cyclic.Int63.Uint63”.

That given, in your code you could simply write:
Require Coq.Numbers.Cyclic.Int63.Uint63.

The point is those are logical paths and Coq needs to be told how those map to physical paths on disk. The code above works if you start coqc/coqtop with default options, otherwise there are command line options or the use of _CoqProject files to do that/your mapping (e.g. custom defined paths in _CoqProject files is common to share code among one’s projects).

See the docs for more details, e.g. here: https://coq.inria.fr/refman/practical-tools/utilities.html?highlight=_coqproject#logical-paths-and-the-load-path and here: https://coq.inria.fr/refman/practical-tools/coq-commands.html#command-line-options

3

I see. Thanks a lot, that was very instructive!

MRandl

1 Like
4

From Coq Require Uint63. is sufficient provided that there is only one package matching Coq. … .Uint63

From is not required, but it avoids name clashes if you later load another package that defines its own Uint63.

See https://coq.inria.fr/refman/proof-engine/vernacular-commands.html#coq:cmd.Require

1 Like