lexicographic_preorder

Stream: general

[Scott Morrison]

A tactic I'm writing will need

def lexicographic_preorder {α β : Type*} [preorder α] [preorder β] : preorder (α × β) :=
{ le := λ a b, a.1 < b.1 ∨ (a.1 = b.1 ∧ a.2 ≤ b.2),
  le_refl := ...,
  le_trans := ..., }

as a local instance. Last time I asked it didn't seem like this was already in mathlib (explicitly in terms of preorders). Should I PR it ahead of the tactic PR?

[Mario Carneiro]

I like it. No instance, maybe shorten to lex_preorder since lex is used elsewhere for this thing, and also add total order and well order if possible

[Scott Morrison]

Great, will do.

[Scott Morrison]

A suggestion which file it goes in?

[Mario Carneiro]

order.basic I think

[Scott Morrison]

In the meantime I've PR'd it to src/order/lexicographic.lean. Shall I move it back into basic?

[Scott Morrison]

It looks like actually using my lexicographic pre/partial/linear orders is a bit painful, because of the existing pre/partial order on products.

[Scott Morrison]

I'm wondering if we should actually remove those as instances.

[Scott Morrison]

In my mind the two different partial orders on a product are both sensible things, and so by our usual rules about instances neither should be installed by default.

[Scott Morrison]

I'm compiling everything now, but so far it seems there are no breakages at this point.

[Simon Hudon]

I would be in favor of only making the lexicographical order an instance because it yields a total order which the current one does not. We could use a type synonym if we want to select the current order

[Simon Hudon]

Or locally make it an instance and decrease the priority of lexicographical order