Find command

Stream: new members

[Pedro Minicz]

How to search for theorems within Lean? I haven't been able to successfully use the #find command yet, is there something like the Search command in Coq? Also, #print notation x looks promising, how do I specialize the result to a given instance (e.g. instead of has_add.add show the add instance for \N)?

#print notation + -- Prints the type class.
#find has_add.add -- Prints nothing apparently.
#find add -- Fails?!

[Aniruddh Agarwal]

For mathlib specifically, I've had some success with the search bar at https://leanprover-community.github.io/mathlib_docs/

[Alex J. Best]

Find is difficult to use imo, most of the time I use library search (or suggest), I write out the result I want (as a have or a separate example) and use library_search to find the proof. Otherwise just guess the name and grep for something close to it.

[Alex J. Best]

For something like the nat.add instance I would press cmd + p in vscode (for me) and then type #nat.has_add and hit enter, which takes me to line 429 of /Users/alex/.elan/toolchains/leanprover-community-lean-3.12.0/lib/lean/library/init/core.lean

[Kevin Buzzard]

If you want to know about has_add.add just #check has_add.add and then right-click on has_add.add and go to definition.

[Pedro Minicz]

I am aware of the mathlib documentation and also had some success with the search bar.

I didn't find any documentation on #find's behavior, where can I find it?

[Bryan Gin-ge Chen]

https://leanprover-community.github.io/mathlib_docs/commands.html##find

[Kevin Buzzard]

I'm not sure anyone uses #find. If you want to use it, I suspect that there are other tricks you don't know. Can you give me an example of why you might think you want to use #find?

[Pedro Minicz]

@Bryan Gin-ge Chen thank you!

[Pedro Minicz]

@Kevin Buzzard in Coq using Search add, for example, will list every theorem within scope containing add. This is very useful in the absence of library_search (although, I suspect auto databases are potentially even more useful). I find library_search very slow, and we kind of know what we want, so I thought #find something_with_add_and_le would be a faster way of doing things.

[Pedro Minicz]

Unfortunately, #find seems very slow from running the few examples in the docs. Which is weird and somewhat disappointing.

[Bryan Gin-ge Chen]

Not sure if this was mentioned above but you can also try the VS Code extension's "symbol search" by hitting ctrl+T. It's not very sophisticated since it just does string search, but sometimes that's good enough.

[Kevin Buzzard]

Typing #check add and then pressing ctrl-space will list the (first 100) theorems in scope whose name contains add

[Kevin Buzzard]

Although sometimes you have to press escape and try again

[Bryan Gin-ge Chen]

I think ctrl+T should in principle return the same results as autocomplete, while being less fiddly.

[Bryan Gin-ge Chen]

Actually, I take that back. They send different commands to the Lean server and I haven't checked that part of the C++ code, so they could differ...

[Kevin Buzzard]

There is a pretty rigorous naming convention in Lean and you find after a while that you can have a very good guess at a theorem name from its type. Of course this isn't perfect but I would imagine that listing all the theorems in scope that mention add isn't either

[Jalex Stark]

Kevin Buzzard said:

There is a pretty rigorous naming convention in Lean and you find after a while that you can have a very good guess at a theorem name from its type. Of course this isn't perfect but I would imagine that listing all the theorems in scope that mention add isn't either

I recently wrote the following to try to find a certain lemma... and library_search returned exactly the name that I had picked for it. So it's possible to learn the naming conventions by accident.

import tactic

open_locale big_operators
open finset


lemma sum_le_sum {α M : Type} [ordered_add_comm_monoid M]
(f g : α → M) (x : finset α) (f_le_g : ∀ a ∈ x, f a ≤ g a) :
∑ a in x, f a ≤ ∑ a in x, g a :=
begin
library_search,
end

[Bryan Gin-ge Chen]

For completeness, here are the naming conventions. (Do we need #naming?)

[Mario Carneiro]

Bryan Gin-ge Chen said:

For completeness, here are the naming conventions. (Do we need #naming?)