total preorder to linear order

Stream: Is there code for X?

[Peter Nelson]

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

[Peter Nelson]

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.

[Bhavik Mehta]

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

[Bhavik Mehta]

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

[Peter Nelson]

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.

[Bhavik Mehta]

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?

[Bhavik Mehta]

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

[Peter Nelson]

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.

[Bhavik Mehta]

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

[Bhavik Mehta]

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

[Peter Nelson]

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

[Bhavik Mehta]

#7142

[Bhavik Mehta]

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

[Bhavik Mehta]

Found it! docs#well_ordering_rel

[Bhavik Mehta]

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?

[Bhavik Mehta]

Specifically where the strict_weak_order comes from something like is_strict_weak_order_of_is_total_preorder

[Peter Nelson]

That looks right, yes

[Peter Nelson]

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