Li-yao (Mar 20 2021 at 15:49): Li-yao (Mar 20 2021 at 15:49):Using 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?
Christian Doczkal (Mar 20 2021 at 16:11):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.
Li-yao (Mar 20 2021 at 16:18):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 :)
Christian Doczkal (Mar 20 2021 at 16:26):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...
Christian Doczkal (Mar 20 2021 at 16:29):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.
Christian Doczkal (Mar 20 2021 at 16:30):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.
Li-yao (Mar 20 2021 at 18:00):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.
Bas Spitters (Mar 20 2021 at 19:11):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: Sep 30 2023 at 07:01 UTC