Zulip Chat Archive

Stream: general

Topic: Finding results in mathlib


view this post on Zulip Cyril Cohen (Mar 09 2021 at 11:06):

Hi everyone,

when I am doing proofs in Coq I spend a non-negligible amount of time (or maybe the major part of my time) using the Search command, to list the theory of some definition(s) or find the "best" lemma to apply at key points in my proofs (for smaller lemmas I can almost always guess their name if they come from mathcomp). The little I did with lean led me to use the command #find, but it is so slow that it was faster to browse lean files directly and/or searching strings in files instead.

My question to proficient users is: what is your way of finding results in mathlib?
Do you search strings? Do you read whole files? Do you use #find? Do you guess/remember names? Is there another way?

One reason I ask is because Kevin Buzzard said:

I was talking to Cyril Cohen last week and he said that one reason he liked Coq more than Lean was that Coq's version of #find was so much quicker than Lean's, and I resisted the urge to say "if you're using #find, you're doing it wrong". I too had essentially forgotten that this existed!

So what is the "right" way of doing it? :wink:

view this post on Zulip Sebastien Gouezel (Mar 09 2021 at 11:09):

I do regexp search through all mathlib with the built-in vscode search. It's almost instant, and it gives me what I am looking for most of the time. I'm not sure it can be called the right way of doing things, though (regexps never are) :-)

view this post on Zulip Ruben Van de Velde (Mar 09 2021 at 11:11):

Not sure if I'd call myself "proficient" yet, but I generally start guessing the name ([naming conventions)[https://leanprover-community.github.io/contribute/naming.html]) and use ctrl+space in vscode to see if I find it; otherwise try the two search functions on https://leanprover-community.github.io/mathlib_docs/ or skim through the relevant mathlib .lean

view this post on Zulip Scott Morrison (Mar 09 2021 at 11:11):

tactic#library_search is often helpful (but can be slow)

view this post on Zulip Ruben Van de Velde (Mar 09 2021 at 11:13):

And that, yeah, though it gives up if you're missing hypotheses in the exact form the lemma needs; sometimes tactic#suggest does that better (but it's also very slow, and gives a lot of pointless suggestions)

view this post on Zulip Ruben Van de Velde (Mar 09 2021 at 11:38):

(Case in point: I just tried to make library_search find a lemma on inequalities on int, made sure I had the 1 < 4 hypothesis in scope, and still failed because that was (1 : nat) < 4), not (1 : int) < 4.)

view this post on Zulip Jason Rute (Mar 09 2021 at 13:45):

I hesitate to mention this because it is neither the established "right way" nor is it void of self promotion, but #lean-gptf (an experimental machine learned tactic suggestion tool for Lean) is halfway decent at finding theorems from mathlib. After installing as a dependency to your project, and after getting access to the API, then use gptf to suggest tactics. Or tell gptf what type of tactic you would like with, e.g., gptf {pfx := "rw"} to get a rewrite tactic. This is good for finding lemmas in mathlib. (Note, gptf doesn't have special access to the library. It just memorizes theorems in the course of its training, but it does it pretty well and can flexibly apply them.)

view this post on Zulip Kevin Buzzard (Mar 09 2021 at 13:51):

Every trick I know has been mentioned other than the hint tactic. I use most of the above and I never use #find. Well spotted Cyril :-)

view this post on Zulip Rob Lewis (Mar 09 2021 at 14:20):

To avoid piling on #find too much, let me say that I do find it useful for finding functions instead of theorems. Like, if I forget what list.join is called I can get it with #find list (list _) → list _. This probably works better because I use it relatively low in the import hierarchy so it isn't horribly slow.


Last updated: May 14 2021 at 21:11 UTC