Zulip Chat Archive

Stream: new members

Topic: Theorem-searching mechanism in Lean?


view this post on Zulip Donald Sebastian Leung (Feb 25 2020 at 10:29):

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?

view this post on Zulip Mario Carneiro (Feb 25 2020 at 10:40):

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

view this post on Zulip Donald Sebastian Leung (Feb 25 2020 at 10:41):

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?

view this post on Zulip Marc Huisinga (Feb 25 2020 at 10:42):

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

view this post on Zulip Kevin Buzzard (Feb 25 2020 at 10:43):

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

view this post on Zulip Kevin Buzzard (Feb 25 2020 at 10:44):

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

view this post on Zulip Donald Sebastian Leung (Feb 25 2020 at 10:46):

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

view this post on Zulip Kevin Buzzard (Feb 25 2020 at 10:47):

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.

view this post on Zulip Johan Commelin (Feb 25 2020 at 13:01):

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

view this post on Zulip Patrick Massot (Feb 25 2020 at 13:01):

Yes.

view this post on Zulip Johan Commelin (Feb 25 2020 at 13:02):

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

view this post on Zulip Patrick Massot (Feb 25 2020 at 13:02):

leancrawler is doing that for instance.

view this post on Zulip Bryan Gin-ge Chen (Feb 25 2020 at 14:22):

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

view this post on Zulip Donald Sebastian Leung (Feb 25 2020 at 14:23):

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!

view this post on Zulip Rob Lewis (Feb 25 2020 at 14:24):

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.

view this post on Zulip Bryan Gin-ge Chen (Feb 25 2020 at 14:24):

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


Last updated: May 11 2021 at 00:31 UTC