Finding results in mathlib

Stream: general

[Cyril Cohen]

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:

[Sebastien Gouezel]

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) :-)

[Ruben Van de Velde]

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

[Scott Morrison]

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

[Ruben Van de Velde]

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)

[Ruben Van de Velde]

(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.)

[Jason Rute]

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.)

[Kevin Buzzard]

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 :-)

[Rob Lewis]

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.