finding lemmas

Stream: new members

[Joachim Breitner]

This must be a very FAQ, but what’s the equivalent of Coq’s SearchAbout? E.g. I want to find lemmas that mention one or more identifiers?

[Yaël Dillies]

library_search, suggest, or maybe just browsing the documentation? eg docs#monotone

[Joachim Breitner]

Hmm, close, but not quite what I was hoping for. For example, can I ask lean to show me all lemmas that mention (_ -> bool) ≃ (_ -> bool) in their types?

[Eric Wieser]

#find might work with wildcards

[Alex J. Best]

I tried find and it didn't work :frown:
I think the best we have is suggest

example : true :=
begin
  have : (_ -> bool) ≃ (_ -> bool) := by suggest,
end

it seems like Coq's Search is better for this sort of thing

[Johan Commelin]

@Joachim Breitner Often a regex search can turn up something. But rg ".*→ bool.*≃.*→ bool" returns nothing.

[Johan Commelin]

But one of the most powerful tools is the naming convention. In this case it's some sort of congr construction about arrows. So I search for def.*arrow_congr and indeed:

src/data/equiv/basic.lean
427:@[congr, simps apply] def arrow_congr {α₁ β₁ α₂ β₂ : Sort*} (e₁ : α₁ ≃ α₂) (e₂ : β₁ ≃ β₂) :
428-  (α₁ → β₁) ≃ (α₂ → β₂) :=
429-{ to_fun := λ f, e₂ ∘ f ∘ e₁.symm,
430-  inv_fun := λ f, e₂.symm ∘ f ∘ e₁,
[snip]

[Yakov Pechersky]

Perhaps maps to bool aren't found often because they don't come up often. I think conceptually, you're using the equiv of set a ~- set b when a ~- b, which I can't remember the name for right now

[Yakov Pechersky]

docs#equiv.set_congr, nope that's not it

[Joachim Breitner]

Nevermind too much the concrete question in this case. The lemma I was looking for doesn’t exist, because it’s unprovable in ZFC :face_palm:. But I can make progress in other ways. Thanks for helping, though!

[Alcides Fonseca]

I think Joachim was looking for some kind of Hoogle (https://hoogle.haskell.org) , but for lean.

[Henrik Böving]

The closest we have to that right now would be the find mentioned above.

[Yaël Dillies]

Time for Loogle? :upside_down:

[Henrik Böving]

I've definitely been planning to look into that once doc-gen4 has all the other features :eyes:

[Henrik Böving]

The theoretical foundations and presentations provided by the author (https://github.com/ndmitchell/hoogle#background) are definitely worth a look btw.