Zulip Chat Archive

Stream: new members

Topic: lexicographic ordering on pi types

Chris Hughes (Jun 27 2019 at 07:41):

Do we have the lex ordering on Pi types yet?

Keeley Hoek (Jun 27 2019 at 07:42):

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

Keeley Hoek (Jun 27 2019 at 07:42):

Around the same time Ico was added

Chris Hughes (Jun 27 2019 at 07:47):

Is it in the library?

Mario Carneiro (Jun 27 2019 at 07:48):

I don't think it's computable

Mario Carneiro (Jun 27 2019 at 07:48):

at least not with arbitrary well orders

Chris Hughes (Jun 27 2019 at 07:50):

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

Mario Carneiro (Jun 27 2019 at 07:52):

you still need an ordering

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

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)

Mario Carneiro (Jun 27 2019 at 08:09):

That works

Chris Hughes (Jun 27 2019 at 08:13):

@Scott Morrison Do you already have this somewhere?

Scott Morrison (Jun 27 2019 at 08:14):

No.

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.

Mario Carneiro (Jun 27 2019 at 11:14):

right

Mario Carneiro (Jun 27 2019 at 11:14):

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

Chris Hughes (Jun 27 2019 at 11:14):

And it's difficult to lift a preorder.

Mario Carneiro (Jun 27 2019 at 11:15):

what do you mean?

Mario Carneiro (Jun 27 2019 at 11:15):

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

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 (<) (≤) }

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

Chris Hughes (Jun 27 2019 at 11:18):

But that's not really right for preorders.

Chris Hughes (Jun 27 2019 at 11:19):

No idea if anyone wants lexicographic preorders.

Mario Carneiro (Jun 27 2019 at 11:19):

that sounds kind of contradictory to me TBH

Mario Carneiro (Jun 27 2019 at 11:20):

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

Mario Carneiro (Jun 27 2019 at 11:20):

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

Chris Hughes (Jun 27 2019 at 11:21):

That's what I thought.

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: Dec 20 2023 at 11:08 UTC