Preorder on Option

Stream: Is there code for X?

[Wrenna Robson]

Does Option have any kind of preorder relationship defined (assuming the underlying type does)? I've run myself into a mild pickle through assuming it did but I'm not sure it does.

[Mario Carneiro]

See docs#WithTop and docs#WithBot

[Mario Carneiro]

depending on whether you want none to be at the top or bottom

[Eric Wieser]

I guess you could put an order on Option X that has none as incomparable?

[Wrenna Robson]

Yeah, that's what I was assuming.

[Wrenna Robson]

Or hoping for.

[Wrenna Robson]

Oddly there is an LT instance defined? But it isn't much use.

[Wrenna Robson]

But what I want is
instance (priority := 10) le [LE α] : LE (Option α) := ⟨Option.Rel (. ≤ .)⟩
instance (priority := 10) lt [LT α] : LT (Option α) := ⟨Option.Rel (. < .)⟩

(and then ideally a preorder...)

[Wrenna Robson]

Wait no. I want that for LE, for LT I don't because obviously Bot should not be LT itself as then you can't make a Preorder

[Wrenna Robson]

Urrrgh. That might be a day's work buggered if this is a challenge. I assumed (given that < worked!) that it would just nicely inherit the structure.

[Yaël Dillies]

Just define a < b ↔ a ≤ b ∧ ¬ b ≤ a

[Wrenna Robson]

Sure, that's what I want.

[Wrenna Robson]

But obviously if it doesn't already exist there will be lots of fiddly lemmas to sort.