I've very recently started learning Coq. I can't find the *standard library* code on GitHub. For example there is this : https://coq.inria.fr/library/Coq.Logic.FunctionalExtensionality.html

But it isn't a .v file or anything. It's a mere rendering (and maybe not complete/uptodate - and in any case I would like to see the real code). I thought it would be here:

https://github.com/coq/coq/tree/master/library

But it isn't.

So I thought it was installed externally, via this:

https://github.com/coq/platform

But I can't find what I'm looking for. So I'm obviously doing something dumb. Please help!

I think the library you are looking for is located here:

https://github.com/coq/coq/tree/master/theories

inside coq's source code

Thanks. And in particular this:

https://github.com/coq/coq/blob/master/theories/Logic/FunctionalExtensionality.v

"theories" huh? OK. I can get used to that!

It's not just the standard library that uses this terminology. You will find that many Coq packages have a `theories/`

directory as well. And when there is a `src/`

directory and a `theory/`

directory, it usually means that this is a plugin and the OCaml code is in `src/`

.

Examples:

- https://github.com/coq-community/aac-tactics (plugin)
- https://github.com/coq-community/coq-mmaps (pure Coq library)

Got it. And I should use the same.

I'm uncomfortable about the use of 'Axiom' in https://github.com/coq/coq/blob/master/theories/Logic/FunctionalExtensionality.v, much as I will probably use it. But how do you know you haven't imported a (non-Core) Axiom you don't want, or don't even know about? Or, more subtly, have imported (Require'd!) some code or a proof that uses such an Axiom somewhere deep inside? I mean, you don't want to have to look through imported files and all dependencies to make sure you haven't added Axioms unconsciously, right?

if you use `coq_makefile`

to generate your Makefile as in coq-mmaps, you can run `make validate`

and see what axioms you're using. If the axioms you use are defined in `Coq.Logic`

, you're fine w.r.t. consistency (to the best of what people currently know)

see section 4.1 in this document for advice on how to think about axioms and hypotheses in Coq

You can also `Print Assumptions lemma_name.`

to see which axioms were needed for that particular lemma

Last updated: Jun 24 2024 at 13:02 UTC