Zulip Chat Archive

Stream: new members

Topic: finding lemmas

Joachim Breitner (Jan 12 2022 at 21:36):

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 (Jan 12 2022 at 21:38):

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

Joachim Breitner (Jan 12 2022 at 22:53):

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 (Jan 12 2022 at 22:56):

#find might work with wildcards

Alex J. Best (Jan 12 2022 at 22:57):

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

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

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

Johan Commelin (Jan 13 2022 at 06:04):

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

Johan Commelin (Jan 13 2022 at 06:09):

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:

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₁,

Yakov Pechersky (Jan 13 2022 at 06:35):

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 (Jan 13 2022 at 06:36):

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

Joachim Breitner (Jan 13 2022 at 10:21):

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 (Jan 13 2022 at 10:32):

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

Henrik Böving (Jan 13 2022 at 10:33):

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

Yaël Dillies (Jan 13 2022 at 10:34):

Time for Loogle? :upside_down:

Henrik Böving (Jan 13 2022 at 10:38):

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

Henrik Böving (Jan 13 2022 at 10:40):

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

Last updated: Dec 20 2023 at 11:08 UTC