Zulip Chat Archive

Stream: general

Topic: Find all uses of a lemma


Justus Springer (May 04 2021 at 09:48):

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 (May 04 2021 at 10:11):

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

Justus Springer (May 04 2021 at 10:47):

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

Eric Wieser (May 04 2021 at 10:49):

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 (May 04 2021 at 10:50):

Do you mean by simp?

Justus Springer (May 04 2021 at 10:51):

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 (May 04 2021 at 10:51):

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 (May 04 2021 at 10:52):

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

Patrick Massot (May 04 2021 at 10:52):

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

Patrick Massot (May 04 2021 at 10:53):

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

Justus Springer (May 04 2021 at 10:53):

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 (May 04 2021 at 10:54):

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 (May 04 2021 at 10:54):

@Justus Springer There is a search tool in VScode

Kevin Buzzard (May 04 2021 at 10:54):

I use the magnifying glass icon in VS Code?

Justus Springer (May 04 2021 at 10:54):

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

Johan Commelin (May 04 2021 at 10:55):

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

Justus Springer (May 04 2021 at 10:57):

Ok thanks!

Justus Springer (May 04 2021 at 10:57):

So does leancrawler also find hidden uses by simp?

Scott Morrison (May 04 2021 at 10:57):

Yes leancrawler actually looks at the generated proof objects.

Scott Morrison (May 04 2021 at 10:57):

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

Justus Springer (May 04 2021 at 10:58):

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

Scott Morrison (May 04 2021 at 10:58):

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.


Last updated: Dec 20 2023 at 11:08 UTC