Print Assumptions in Coq or
make validate on the command-line, I can find out what axioms a codebase depends on, but is there a way to know which of my definitions introduce axioms?
I'm not entirely sure I understand your question. A "Definition" should not introduce any axioms. One known exception is "Program Definition" which does much more than just create a definition and, IIRC, relies on proof irrelevance (or UIP). If you're asking which of the lemmas (from some other library you're using) depends on a given axiom, that's harder to find out.
If you're asking which of the lemmas (from some other library you're using) depends on a given axiom, that's harder to find out.
That is what I am looking for :)
Well, one option is to make a few well-educated guesses and run
Print Assumptions on interesting lemmas until you find the one you're looking for. Another option is to do a (manual) binary search on your development to find the first of your lemmas depending on a given axiom. Not sure whether there is an easier way, I only use libraries that I know to be axiom-free...
Just hope that the library you've been using does not add lemmas depending on axioms to the global hint data base used by auto. In that case there may not even be a trace in the .v file.
Another possibility might be to use coq-dpdgraph and run in on your development together with the library relying on axioms. This should give you a (huge) graph with an axiom node somewhere and path of all the things that depend on it.
I'm currently making lucky guesses, but I think next time I have to do a tree search I'm going to write a script to
Print Assumptions on every single lemma/theorem, unless there is already a tool for the job.
There isn't I recently asked the same question. If you happen to write a script please make it available to others too.
Last updated: Jan 29 2023 at 03:28 UTC