Zulip Chat Archive

Stream: Is there code for X?

Topic: total preorder to linear order


view this post on Zulip Peter Nelson (Apr 09 2021 at 13:44):

Does mathlib contain anything like a proof of the following? (I am interested in the finite case, which can be done by induction, but it presumably holds in general).

lemma total_preorder_to_linear_order {β : Type*} (r : β  β  Prop) [is_total_preorder β r] :
   r', (is_linear_order β r'   x y, r x y  r' x y) :=
sorry

view this post on Zulip Peter Nelson (Apr 09 2021 at 14:14):

On a related note, would it make sense for total_preorder to be a class? It arises naturally as an order lift of a linear order.

view this post on Zulip Bhavik Mehta (Apr 09 2021 at 18:29):

Perhaps I'm missing something, but I don't think this works, since there could be elements x and y in β which are related both ways but aren't equal - ie r' won't be antisymmetric

view this post on Zulip Bhavik Mehta (Apr 09 2021 at 18:29):

If you want an extension of a partial order to a linear order I have code for that lying around somewhere which I can PR

view this post on Zulip Peter Nelson (Apr 09 2021 at 18:38):

ah, you're right. I do still want a preorder though - I suppose I mean that if x < y then x <' y (where < is the preorder and <' is the linear order). What I'm thinking about is sorting a set by the value of some function to a linear order (hence giving a total preorder) with ties being broken arbitrarily. This is a bit annoying to express in terms of the unbundled order typeclasses, though.

view this post on Zulip Bhavik Mehta (Apr 09 2021 at 18:39):

You can convert a preorder to a partial order by taking quotients by the relation r x y or r y x, and then make that into a linear order... Does that work for your use case?

view this post on Zulip Bhavik Mehta (Apr 09 2021 at 18:40):

I suppose it doesn't, it's different from your notion of breaking ties arbitrarily

view this post on Zulip Peter Nelson (Apr 09 2021 at 18:42):

The case where every pair is comparable both ways in the preorder is asking for a linear order on an arbitrary type - i.e. a weak version of the well-ordering principle. I can't see this anywhere in mathlib, though.

view this post on Zulip Bhavik Mehta (Apr 09 2021 at 18:46):

I think it might be with Zorn's lemma if anywhere?

view this post on Zulip Bhavik Mehta (Apr 09 2021 at 18:47):

If not, I have a branch which upgrades any partial order to a linear order, in particular the empty partial order, which also gives a linear order on any type

view this post on Zulip Peter Nelson (Apr 09 2021 at 19:12):

I don't see this in an obvious way in order.zorn. If you could link to the branch, that'd be great!

view this post on Zulip Bhavik Mehta (Apr 09 2021 at 19:35):

#7142

view this post on Zulip Bhavik Mehta (Apr 09 2021 at 19:44):

I'm not finding the well-ordering principle in mathlib anywhere either...

view this post on Zulip Bhavik Mehta (Apr 09 2021 at 20:06):

Found it! docs#well_ordering_rel

view this post on Zulip Bhavik Mehta (Apr 09 2021 at 20:13):

Peter Nelson said:

ah, you're right. I do still want a preorder though - I suppose I mean that if x < y then x <' y (where < is the preorder and <' is the linear order). What I'm thinking about is sorting a set by the value of some function to a linear order (hence giving a total preorder) with ties being broken arbitrarily. This is a bit annoying to express in terms of the unbundled order typeclasses, though.

If I'm understanding correctly, you want an extension of an is_strict_total_order from an is_strict_weak_order?

view this post on Zulip Bhavik Mehta (Apr 09 2021 at 20:13):

Specifically where the strict_weak_order comes from something like is_strict_weak_order_of_is_total_preorder

view this post on Zulip Peter Nelson (Apr 09 2021 at 20:47):

That looks right, yes

view this post on Zulip Peter Nelson (Apr 09 2021 at 20:50):

It looks like this is easy to do, with the heavy lifting done by your extension lemma.


Last updated: May 16 2021 at 05:21 UTC