with_bot.preorder

Stream: general

[Kevin Buzzard]

instance [preorder α] : preorder (with_bot α) :=
{ le          := λ o₁ o₂ : option α, ∀ a ∈ o₁, ∃ b ∈ o₂, a ≤ b,

[Gabriel Ebner]

Is there a question hidden here?

[Kevin Buzzard]

Oh I forgot to add the question! Why is this defined in such a silly way instead of just by pattern matching? I now want the three fundamental lemmas with_bot.le, coe_le_coe_iff and it looks harder to get them this way but of course it's not impossible, it's just hard for a beginner. My question is what is the rationale behind this design decision?

[Reid Barton]

It avoids case analysis in stuff like le_trans I guess

[Chris Wong]

That reminds me of the lemmas about list.head' and list.last', e.g. https://leanprover-community.github.io/mathlib_docs/data/list/basic.html#list.head_mem_head'

a ∈ o is defined as o = option.some a, which I guess could be more convenient than a match expression (as you can rewrite with it)