Stream: Coq users

Topic: Sorting out axioms


view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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 :)

view this post on Zulip 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...

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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: Jan 29 2023 at 03:28 UTC