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:
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: Oct 13 2024 at 01:02 UTC