Theorem-searching mechanism in Lean?

Stream: new members

[Donald Sebastian Leung]

In Coq, when I wish to invoke a theorem that I believe should already be in the stdlib, I can use the Search vernacular as follows:

Search ({?P} + {~ ?P}). (* Searches for all results of decidable propositions in the stdlib *)

Is there a similar mechanism in Lean by chance?

[Mario Carneiro]

by library_search is probably the most reliable tool for this right now

[Donald Sebastian Leung]

Mario Carneiro said:

by library_search is probably the most reliable tool for this right now

Thanks! I suppose this is just an ordinary tactic which tries to apply a lemma from the stdlib? And where can I learn more about it?

[Marc Huisinga]

https://github.com/leanprover-community/mathlib/blob/master/docs/tactics.md#library_search

[Kevin Buzzard]

There's now a fancier link to the tactics doc isn't there?

[Kevin Buzzard]

https://leanprover-community.github.io/mathlib_docs/tactics.html#library_search

[Donald Sebastian Leung]

Kevin Buzzard said:

https://leanprover-community.github.io/mathlib_docs/tactics.html#library_search

This is very useful, I did not realize there was a dedicated webpage for mathlib documentation.

Bookmarked for future reference

[Kevin Buzzard]

It's quite new. Rob Lewis and others put quite a lot of effort into it. Other goodies are available here. I find that page quite useful.

[Johan Commelin]

Can tactics ask Lean in which file (+ line number?) a certain statement is?

[Patrick Massot]

Yes.

[Johan Commelin]

So library_search could print a link to the docs in the message window?

[Patrick Massot]

leancrawler is doing that for instance.

[Bryan Gin-ge Chen]

I'm not familiar with Coq's Search, but it kind of looks like #find.

[Donald Sebastian Leung]

Bryan Gin-ge Chen said:

I'm not familiar with Coq's Search, but it kind of looks like #find.

Yes, that looks like what I am looking for. Thank you!

[Rob Lewis]

Coq's search is much better than find, in that it's far faster and (I think) can find declarations that are outside the current environment.

[Bryan Gin-ge Chen]

I agree with the replies above that usually library_search (or its parent suggest) are much more useful in practice.