Zulip Chat Archive

Stream: new members

Topic: le notation


view this post on Zulip 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?

view this post on Zulip Johan Commelin (Feb 17 2021 at 11:36):

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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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) )}

view this post on Zulip Calle Sönne (Feb 17 2021 at 11:39):

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

view this post on Zulip 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: )

view this post on Zulip 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

view this post on Zulip Johan Commelin (Feb 17 2021 at 11:42):

huh, wait

view this post on Zulip Johan Commelin (Feb 17 2021 at 11:43):

Do you already have

instance profinite_limit_category : partial_order (profinite_skeleton X) := _

view this post on Zulip Johan Commelin (Feb 17 2021 at 11:43):

The code suggests you do

view this post on Zulip Calle Sönne (Feb 17 2021 at 11:43):

yeah

view this post on Zulip Johan Commelin (Feb 17 2021 at 11:44):

So how come it doesn't infer that instance?

view this post on Zulip Calle Sönne (Feb 17 2021 at 11:44):

Because it uses the wrong one

view this post on Zulip Johan Commelin (Feb 17 2021 at 11:44):

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

view this post on Zulip Johan Commelin (Feb 17 2021 at 11:44):

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

#print foo

view this post on Zulip Johan Commelin (Feb 17 2021 at 11:44):

what does that return?

view this post on Zulip 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)

view this post on Zulip 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?

view this post on Zulip Johan Commelin (Feb 17 2021 at 11:45):

No, you should scratch that first advice

view this post on Zulip 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.

view this post on Zulip 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))

view this post on Zulip Calle Sönne (Feb 17 2021 at 11:49):

So its the topological space that ruins everything?

view this post on Zulip Johan Commelin (Feb 17 2021 at 11:50):

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

view this post on Zulip Johan Commelin (Feb 17 2021 at 11:50):

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

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Feb 17 2021 at 11:51):

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

view this post on Zulip Johan Commelin (Feb 17 2021 at 11:51):

That should solve these issues with instances.

view this post on Zulip 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

view this post on Zulip Johan Commelin (Feb 17 2021 at 11:53):

lunch time :running: :bread:

view this post on Zulip Calle Sönne (Feb 17 2021 at 11:53):

Thanks!


Last updated: May 12 2021 at 23:13 UTC