Order on α ⊕ β

Stream: Is there code for X?

[Yaël Dillies]

Do we not have docs#sum.preorder, docs#sigma.preorder and alike?

[Eric Rodriguez]

what exactly what you expect for those instances? not sure there's an obvious choice

[Mario Carneiro]

there are two obvious choices. I think docs#sum.lex might exist

[Adam Topaz]

The following seems pretty canonical to me...

import order.basic

variables (α : Type*) (X : α → Type*) [preorder α] [∀ i, preorder (X i)]

inductive preorder_sigma : Π (a b : Σ i, X i), Prop
| fiber (a : α) (x y : X a) : x ≤ y → preorder_sigma ⟨a,x⟩ ⟨a,y⟩
| base (a b : α) (x : X a) (y : X b) : a < b → preorder_sigma ⟨a,x⟩ ⟨b,y⟩
| trans (a b c) : preorder_sigma a b → preorder_sigma b c → preorder_sigma a c

instance : preorder (Σ i, X i) :=
{ le := λ a b, preorder_sigma _ _ a b,
  lt := _,
  le_refl := begin
    rintros ⟨a,x⟩,
    apply preorder_sigma.fiber,
    apply le_refl,
  end,
  le_trans := begin
    intros a b c h1 h2,
    apply preorder_sigma.trans,
    assumption'
  end }

[Adam Topaz]

And since α ⊕ β ≃ Σ (i : fin 2), if i = 0 then α else β with fin 2 having an order, it seems fairly clear what the order on the sum should be...

[Eric Rodriguez]

I agree with the sigma case, but I don't see why or.inl _ < or.inr _ should be the default at all.

[Adam Topaz]

The only argument is that "we read from left to write" (in English, at least)

[Eric Rodriguez]

Well, bool has a linear order, and if we do this the ltr way then we can upgrade docs#equiv.sum_equiv_sigma_bool to an orderiso

[Eric Rodriguez]

so I guess there is a case

[Mario Carneiro]

The second "obvious" order I was referring to is the one generated only from the fiber variant of that inductive

[Mario Carneiro]

it looks like you have described sigma.lex

[Adam Topaz]

Is that a thing? (Test: docs#sigma.lex )

[Mario Carneiro]

I think that inductive is transitive even without trans

[Adam Topaz]

Probably... I was lazy :wink:

[Yaël Dillies]

I'd have personally expected the disjoint union of the orders to be the default one (as it doesn't require an order on the index type) and the lexicographical one to be on a type alias/be accessible using a locale.

[Yaël Dillies]

Mario Carneiro said:

it looks like you have described sigma.lex

Hmm, I shall PR that then