BetterFind.lean - a better way to find theorems in Lean

Stream: general

[Kiran]

Hi Lean Folks! Pleased to announce a release of BetterFind.lean, a tactic for an improved search experience for Lean.

Available at: https://github.com/kiranandcode/BetterFind.lean

BetterFind.lean - a better find tactic for lean

This is a work in progress tactic for Lean, based on mathlib's find tactic that provides more functionalities closer to Rocq.

Features

1. Recreates #find -- Running bfind <pattern> does the same thing as the #find you're used to.

theorem myThm x: 1 + x = x + 1 := by
      bfind (?x + _ = _)
/--
Messages here:
Std.HashMap.getElem_insertManyIfNewUnit_list: ...
Nat.add_comm: ...
String.set_next_add.foo: ..
...
--/

2. Adds support for filtering results, by Ident -- bfind <pattern> : <ident> filters generated results to only those that contain the ident

theorem myThm x: 1 + x = x + 1 := by
      bfind (?x + _ = _) : Nat -- only those involving Nats
/--
Messages here:
Std.HashMap.getElem_insertManyIfNewUnit_list: ...
Nat.add_comm: ...
String.set_next_add.foo: ..
...
--/

3. Adds support for filtering results, by fuzzy match

searching for [.ident Nat]
theorem myThm x: 1 + x = x + 1 := by
      bfind (?x + _ = _) : "comm" -- only lemmas whose name fuzzy matches comm (commutativity?)
/--
searching for ["comm"]
Nat.add_comm: ...
Lean.Grind.AddCommMonoid.add_comm: ...
Int.add_right_comm: ...
Lean.Grind.Fin.add_comm: ...
Lean.Grind.AddCommMonoid.add_left_comm: ...
--/

4. Combining constraints -- these constraints can be arbitrarily combined

theorem myThm x: 1 + x = x + 1 := by
      bfind (?x + _ = _) : "comm" Nat -- only lemmas whose name fuzzy matches comm and involve Nats (commutativity?)
/--
Nat.add_comm: ...
Lean.Grind.Fin.add_comm:  ...
Nat.add_right_comm: ...
Nat.add_left_comm:  ...
BitVec.sub_add_comm: ...
--/

5. No mathlib dependency

[Kim Morrison]

Looking forward to having this in a form we could depend on in Mathlib. :-)

How does this compare to #loogle? How fast is it after import Mathlib? Why do the messages above say "Messages here:"? Are the results above real? (If so, what is String.set_next_add.foo?)

The colon syntax reads strangely to me, we always use that for typing in Lean.

[Damiano Testa]

Maybe with instead of the colon?

[Eric Wieser]

To make things more confusing #find is overridden with a better version if you import Loogle!

[Kiran]

Eric Wieser said:

To make things more confusing #find is overridden with a better version if you import Loogle!

Oh that's really annoying. Yes, you're exactly right, the version of find exported by loogle is closer to what I've implemented:

https://github.com/nomeata/loogle/blob/master/Loogle/Find.lean

There's some major discovery problems with the loogle readme, there's no mention it provides an additional #find tactic, only mentions of loogle integration and #loogle, when a dedicated tactic closer to #find was what I wanted

[Michael Sammler]

The #find tactic from loogle looks very nice, but I have troubles getting it to work. I created a separate thread for that here: #general > How to use the #find tactic from Loogle in a custom project? @ 💬