Find and Unfold Notation

Stream: new members

[Rudy Peterson]

Hello,

I am trying to find the definition of and unfold a particular notation in my Lean 4 proofs.

Specifically, I am trying to unfold the ⋃ _ ∈ _, _ notation, which I believe is for union of indexed families of sets. I believe this is for Set.iUnion, but I would like to unfold this notation in the proof context to see exactly what is happenning and if there are any implicit arguments.

Furthermore, I was attempting to find lemmas with ⋃ _ ∈ _, _ via

 #find "⋃ _ ∈ _, _" -- does not show anything?
 #find (⋃ _ ∈ _, _) -- gives an error

elaboration function for 'Mathlib.Notation3.«termExpand_binders%(_=>_)_,_»' has not been implemented
  expand_binders% (f => iUnion f) (_ ∈ _), _

Is there a way for me to unfold and find lemmas with these notations?

Thanks!

[Kevin Buzzard]

Those lemmas will probably have the word biUnion in their name, e.g. docs#Set.biUnion_pair . You hopefully don't need to unfold the notation to figure out what's going on.

[Kevin Buzzard]

import Mathlib

--set_option pp.notation false , or just hover on notation to see the declaration
example (α β : Type) (s : Set α) (F : α → Set β) : ⋃ i ∈ s, F i = ⊤ := by
  unfold Set.iUnion
  -- ⊢ ⨆ i ∈ s, F i = ⊤
  unfold iSup
  unfold sSup
  unfold Set.instSupSet
  dsimp
  -- you'll probably not get any further than this
  sorry

But as I say, this is not really the way to do it; hopefully the lemmas you need are there for bounded indexed unions.

[Kyle Miller]

Notations don't need unfolding, they're purely a pretty printing phenomenon. If you hover over a notation in the Infoview, you can see what it stands for.

You can use set_option pp.notations false outside your proof if you don't want to see any notations pretty printed.

[Rudy Peterson]

Is there a way to search for lemmas and theorems with notations?

My background is mainly from Coq where you can do stuff like:

Search (⋃ _ ∈ _, _) (_ ∈ _).

Does the #find command in lean 4 allow one to do something similar?

Thanks!

[Rudy Peterson]

Also, in my case, I was trying to rewrite the goal, and while the notation made the goal and the lemma appear exactly the same, the lemma had match_2, whereas the goal had match_1.

What is the difference in lean 4?

[Edward van de Meent]

i believe #loogle is something which might suit your needs... As for your second question, can you provide a #mwe ?

[Rudy Peterson]

Edward van de Meent said:

i believe #loogle is something which might suit your needs... As for your second question, can you provide a #mwe ?

I tried using #loogle but maybe this specific notation is not supported?

#loogle (⋃ _ ∈ _, _) (_ ∈ _)

Loogle search failed with error: elaboration function for 'Mathlib.Notation3.«termExpand_binders%(_=>_)_,_»' has not been implemented
  expand_binders% (f => iUnion f) (_ ∈ _), _

I'll do my best to come up with a MWE for the match_1 match_2 thing.

[Edward van de Meent]

the issue there is that the notation ⋃ _ ∈ _, _ refers to does not accept an underscore as bound variable, so it doesn't elaborate. replacing it with x instead does work

[Edward van de Meent]

i.e. #loogle (⋃ x ∈ _, _), (_ ∈ _) works

[Edward van de Meent]

(this is not a flaw of loogles, it's a flaw of how the notation for unions is implemented)

[Yaël Dillies]

Are you sure it's not just the missing comma before (_ ∈ _)?

[Edward van de Meent]

oh right, that was another issue

[Rudy Peterson]

Ah, my bad. Thanks!

[Kyle Miller]

I'm surprised no one's reported that you can't use _ for a binder for scoped notation yet! I guess everyone writes _x or something for unused binders?

[Kyle Miller]

Ah, I see why it's not currently supported: expanding ⋃ _ ∈ _, _ to Set.iUnion fun _ ↦ Set.iUnion fun (h : _ ∈ _) ↦ _ would be a mistake. We need to generate a new name x to instead expand it to Set.iUnion fun x ↦ Set.iUnion fun (h : x ∈ _) ↦ _, to link the variable to the binder predicate

[Kyle Miller]

#21924 makes it possible to use _ for the binder in ⋃ _ ∈ _, _