Stream: new members

Topic: le notation

Calle Sönne (Feb 17 2021 at 11:35):

I have defined a preorder on a bunch of sets and I want to use the ≤ notation, but lean interprets this as the subset relation. Is there anyway I can temporarily "prioritize" the ≤ notation to use this new preorder?

Johan Commelin (Feb 17 2021 at 11:36):

So the "bunch of sets" is actually "all sets"?

Calle Sönne (Feb 17 2021 at 11:37):

Johan Commelin said:

So the "bunch of sets" is actually "all sets"?

Oh no, its a certain set of sets

Johan Commelin (Feb 17 2021 at 11:37):

If you defined bunch_of_sets := _ then Lean shouldn't be able to infer any subset relation whatsoever on it.

Calle Sönne (Feb 17 2021 at 11:38):

Hmm, this is my definition:

def profinite_skeleton (X : Profinite) :=
{ I : set (set (X.to_Top.α)) | (I.finite) ∧ (∀ U ∈ I, is_open U ∧ U.nonempty) ∧
(⋃₀ I = univ) ∧ (∀ U V ∈ I, (U ∩ V : set X.to_Top.α).nonempty → (U = V) )}


Calle Sönne (Feb 17 2021 at 11:39):

So its actually of type set (set (set (X.to_Top.α)))

Calle Sönne (Feb 17 2021 at 11:41):

When I turned it into a category I had to be very specific to use the right le:

instance profinite_limit_category : small_category (profinite_skeleton X) :=
@preorder.small_category _ (@partial_order.to_preorder _ profinite_skeleton.partial_order)


(I had to learn this the hard way :joy: )

Johan Commelin (Feb 17 2021 at 11:42):

Well, you can make that a little bit easier by first declaring

instance profinite_limit_category : preorder (profinite_skeleton X) :=
@partial_order.to_preorder _ profinite_skeleton.partial_order


huh, wait

Johan Commelin (Feb 17 2021 at 11:43):

Do you already have

instance profinite_limit_category : partial_order (profinite_skeleton X) := _


Johan Commelin (Feb 17 2021 at 11:43):

The code suggests you do

yeah

Johan Commelin (Feb 17 2021 at 11:44):

So how come it doesn't infer that instance?

Calle Sönne (Feb 17 2021 at 11:44):

Because it uses the wrong one

Johan Commelin (Feb 17 2021 at 11:44):

Which instance does it find instead when you ask for has_le?

Johan Commelin (Feb 17 2021 at 11:44):

def foo : has_le (profinite_skeleton X) := by apply_instance

#print foo


Johan Commelin (Feb 17 2021 at 11:44):

what does that return?

Calle Sönne (Feb 17 2021 at 11:45):

def Profinite.foo : Π {X : Profinite}, has_le ↥(X.profinite_skeleton) :=
λ {X : Profinite}, preorder.to_has_le ↥(X.profinite_skeleton)

Calle Sönne (Feb 17 2021 at 11:45):

Johan Commelin said:

Well, you can make that a little bit easier by first declaring

instance profinite_limit_category : preorder (profinite_skeleton X) :=
@partial_order.to_preorder _ profinite_skeleton.partial_order


Oh so my problem is since I dont have this, lean infers another preorder?

Johan Commelin (Feb 17 2021 at 11:45):

No, you should scratch that first advice

Johan Commelin (Feb 17 2021 at 11:46):

Could you please print foo with set_option.pp_all true, or maybe pp.implicit if the former yields 5gb of mess.

Calle Sönne (Feb 17 2021 at 11:48):

def Profinite.foo : Π {X : Profinite}, has_le ↥(X.profinite_skeleton) :=
λ {X : Profinite},
@preorder.to_has_le ↥(X.profinite_skeleton)
(@subtype.preorder (set (set (@bundled.α topological_space X.to_Top)))
(@partial_order.to_preorder (set (set (@bundled.α topological_space X.to_Top)))
(@order_bot.to_partial_order (set (set (@bundled.α topological_space X.to_Top)))
(@bounded_lattice.to_order_bot (set (set (@bundled.α topological_space X.to_Top)))
(@complete_lattice.to_bounded_lattice (set (set (@bundled.α topological_space X.to_Top)))
(@set.lattice_set (set (@bundled.α topological_space X.to_Top)))))))
(λ (x : set (set (@bundled.α topological_space X.to_Top))), x ∈ X.profinite_skeleton))


Calle Sönne (Feb 17 2021 at 11:49):

So its the topological space that ruins everything?

Johan Commelin (Feb 17 2021 at 11:50):

Aah! I see. It's the ↥ in has_le ↥(X.profinite_skeleton)

Johan Commelin (Feb 17 2021 at 11:50):

You define profinite_skeleton as a set, instead of as a new type.

Johan Commelin (Feb 17 2021 at 11:51):

I'm not sure if you actually want to treat it as a (sub)set, or as a type.

Johan Commelin (Feb 17 2021 at 11:51):

If you want a type, then change the | into // in the definition of profinite_skeleton.

Johan Commelin (Feb 17 2021 at 11:51):

That should solve these issues with instances.

Johan Commelin (Feb 17 2021 at 11:52):

Of course you loose the ability to write x \in profinite_skeleton X, so you have to decide if that's important

Johan Commelin (Feb 17 2021 at 11:53):

lunch time :running: :bread:

Calle Sönne (Feb 17 2021 at 11:53):

Thanks!

Last updated: Dec 20 2023 at 11:08 UTC