Find all uses of a lemma

Stream: general

[Justus Springer]

To get a better feeling for the dependency structure of mathlib, I sometimes wish to look up all places where a lemma of a given name is used in a proof. Is there some tool for this, maybe in VSCode?

[Eric Wieser]

I assume you also want to know when that lemma is used by simp?

[Justus Springer]

Not really, I want to see where a lemma is used at all

[Eric Wieser]

Sorry, what I mean is that if a proof is by simp, and that happens to use the lemma foo, then do you want your search for foo to find that proof?

[Justus Springer]

Do you mean by simp?

[Justus Springer]

No I mean more like this: Sometimes I see a lemma in some part of the library and I wonder why we need it, i.e. where it is used.

[Kevin Buzzard]

simp and simp? are the same tactic. You said "I want to find all the places where a lemma is used" and Eric's question is "what you mean exactly by "used""? Sometimes a lemma is used without its name being explicitly mentioned.

[Kevin Buzzard]

If you just want to see where its name is mentioned, why not just use search?

[Patrick Massot]

Eric, Justus obviously also want to know when simp silently uses a lemma.

[Patrick Massot]

Our only answer is leancrawler as far as I know, which is not very convenient to use.

[Justus Springer]

Patrick Massot said:

Our only answer is leancrawler as far as I know, which is not very convenient to use.

Thanks, that's exactly what I was looking for!

[Justus Springer]

Kevin Buzzard said:

If you just want to see where its name is mentioned, why not just use search?

How can I quickly search through all files of mathlib?

[Johan Commelin]

@Justus Springer There is a search tool in VScode

[Kevin Buzzard]

I use the magnifying glass icon in VS Code?

[Justus Springer]

Sorry this might be a newbie question, someone better move it to "new members" :sweat_smile:

[Johan Commelin]

But you can also use the command line, if you know that

[Justus Springer]

Ok thanks!

[Justus Springer]

So does leancrawler also find hidden uses by simp?

[Scott Morrison]

Yes leancrawler actually looks at the generated proof objects.

[Scott Morrison]

It doesn't care what you wrote in the tactic block.

[Justus Springer]

Great, I'm going to start playing with that then :)

[Scott Morrison]

The search tool in VSCode is absolutely essentially --- learning to use basic regular expressions (even just foo.*bar, to find occurrences of foo and bar on the same line) is probably the #1 way to find results in the library.