reach of theorems

Stream: mathlib4

[Ralf Stephan]

How to get a list of theorems that are directly or indirectly affected by other theorems? I'd need it in particular to avoid circular reasoning when proving the infinitude of primes.

[Johan Commelin]

So, given a theorem in mathlib, you want to know whether it depends on mathlib's version of the infinitude of primes?

[Johan Commelin]

You could try to adapt forbiddenAxioms from this message: https://leanprover.zulipchat.com/#narrow/stream/348111-batteries/topic/scope.20of.20std/near/412282298

[Ralf Stephan]

Better, given a theorem, which theorems are call-children of it.

[Ralf Stephan]

I.E. x is bad. y calls x so is bad too, etc. Give a list of all bad ones. The whole tree.

[Ralf Stephan]

Sigh, it seems I can no longer avoid metaprogramming...

[Damiano Testa]

In some Zulip thread there is some code that gives you all the "upstream" declarations of a given one. However, running it on all declarations in the environment is expensive.

[Damiano Testa]

This is the thread.

[Joachim Breitner]

Open it in VS Code and use the Call Hierarchy feature? It will only show explicit uses, though, e.g. won't work for simp lemmas.

[Ralf Stephan]

Thanks for the suggestions. I'm not satisfied with knowing if my own specific theorem depends on a bad theorem in Mathlib. I need to see the full picture of how "bad" (from my perspective) the whole situation is, to be able to plan around it.

It looks to me that these scripts, and Lean4 metaprogramming in general, is meant to be run from a .lean file in VScode, and work on the data that is imported there. Contrary to your scripts, my idea is to read all of Mathlib, and list all theorems that depend on a (set of) bad theorem(s). Is that possible by import Mathlib?

If not, or too slow, I'd rather write an external parser, because I don't need the full syntax for this. Parsec may be a choice.

[Damiano Testa]

If you want precise information, I don't think that you will be able to do it more quickly than in Lean itself.

Note that there are many "invisible" lemmas that are stated and used almost exclusively by tactics such as norm_num, norm_cast, ring, simp,... Depending on how "automated" your set of bad lemmas is, you may get unreliable results without actually looking at the proof terms.

In a file with import Mathlib, the environment has access to all the declarations and you can use (some modification of) the scripts above. However, I suspect that unless you work on optimising the algorithms, getting the information that you want can be a fairly long task.