Zulip Chat Archive

Stream: new members

Topic: lexicographic ordering on pi types


view this post on Zulip Chris Hughes (Jun 27 2019 at 07:41):

Do we have the lex ordering on Pi types yet?

view this post on Zulip Keeley Hoek (Jun 27 2019 at 07:42):

I vaguely recall maybe Scott did this at one point in time

view this post on Zulip Keeley Hoek (Jun 27 2019 at 07:42):

Around the same time Ico was added

view this post on Zulip Chris Hughes (Jun 27 2019 at 07:47):

Is it in the library?

view this post on Zulip Mario Carneiro (Jun 27 2019 at 07:48):

I don't think it's computable

view this post on Zulip Mario Carneiro (Jun 27 2019 at 07:48):

at least not with arbitrary well orders

view this post on Zulip Chris Hughes (Jun 27 2019 at 07:50):

I'm interested in when the indexing type is finite.

view this post on Zulip Mario Carneiro (Jun 27 2019 at 07:52):

you still need an ordering

view this post on Zulip Mario Carneiro (Jun 27 2019 at 07:53):

If you have a list I enumerating the index set, you should be able to build it out of prod.lex parts

view this post on Zulip Chris Hughes (Jun 27 2019 at 07:58):

Yeah, so the indexing type needs to be ordered.
This is the correct definition right? Maybe r should be some total order.

variables {α : Type*} {β :  α  Type*} (r : α  α  Prop)  (s : Π {a : α}, β a  β a  Prop)

def pi.lex (f g : Π a, β a) : Prop :=
 a, ( b, r b a  f b = g b)  s (f a) (g a)

view this post on Zulip Mario Carneiro (Jun 27 2019 at 08:09):

That works

view this post on Zulip Chris Hughes (Jun 27 2019 at 08:13):

@Scott Morrison Do you already have this somewhere?

view this post on Zulip Scott Morrison (Jun 27 2019 at 08:14):

No.

view this post on Zulip Chris Hughes (Jun 27 2019 at 11:02):

This is actually more complicated than expected in the infinite case. The indexing type has to be well ordered to get a total order.

view this post on Zulip Mario Carneiro (Jun 27 2019 at 11:14):

right

view this post on Zulip Mario Carneiro (Jun 27 2019 at 11:14):

Of course lex order on Z -> Z doesn't work

view this post on Zulip Chris Hughes (Jun 27 2019 at 11:14):

And it's difficult to lift a preorder.

view this post on Zulip Mario Carneiro (Jun 27 2019 at 11:15):

what do you mean?

view this post on Zulip Mario Carneiro (Jun 27 2019 at 11:15):

there is a natural preorder / partial order on pi types, but it's not lex order

view this post on Zulip Chris Hughes (Jun 27 2019 at 11:16):

I ccouldn't think of a natural lex preorder. le on prod is this. But I can't do this on pi without a greatest element.

instance lex_has_le [preorder α] [preorder β] : has_le (lex α β) :=
{ le := prod.lex (<) () }

view this post on Zulip Chris Hughes (Jun 27 2019 at 11:17):

So I did this for lt

def pi.lex (x y : Π i, β i) : Prop :=
 i, ( j, r j i  x j = y j)  s (x i) (y i)

def pilex (α : Type*) (β : α  Type*) : Type* := Π a, β a

instance [has_lt ι] [ a, has_lt (β a)] : has_lt (pilex ι β) :=
{ lt := pi.lex (<) (λ _, (<)) }

And just defined le to be lt or equal

view this post on Zulip Chris Hughes (Jun 27 2019 at 11:18):

But that's not really right for preorders.

view this post on Zulip Chris Hughes (Jun 27 2019 at 11:19):

No idea if anyone wants lexicographic preorders.

view this post on Zulip Mario Carneiro (Jun 27 2019 at 11:19):

that sounds kind of contradictory to me TBH

view this post on Zulip Mario Carneiro (Jun 27 2019 at 11:20):

To me the whole point of lex order is to make it total

view this post on Zulip Mario Carneiro (Jun 27 2019 at 11:20):

If you want a preorder it's \all i, f i <= g i

view this post on Zulip Chris Hughes (Jun 27 2019 at 11:21):

That's what I thought.

view this post on Zulip Chris Hughes (Jun 27 2019 at 11:25):

To me the whole point of lex order is to make it total

That's why dictionaries use it.


Last updated: May 12 2021 at 04:19 UTC