Commit 2021-11-10 17:25 6f10557a

refactor(order): order_{top,bot} as mixin (#10097) This changes order_top α / order_bot α to require has_le α instead of extending partial_order α. As a result, order_top can be combined with other lattice typeclasses. This lends itself to more refactors downstream, such as phrasing lemmas that currently require orders/semilattices and top/bot to provide them as separate TC inference, instead of "bundled" classes like semilattice_inf_top. This refactor also provides the basis for making more consistent the "extended" algebraic classes, like "e(nn)real", "enat", etc. Some proof terms for lemmas about nnreal and ennreal have been switched to rely on more direct coercions from the underlying non-extended type or other (semi)rings. Modify semilattice_{inf,sup}_{top,bot} to not directly inherit from order_{top,bot}. Instead, they are now extending from has_{top,bot}. Extending order_{top,bot} is now only possible is has_le is provided to the TC cache at extends declaration time, when using old_structure_cmd true. That is,

set_option old_structure_cmd true
class mnwe (α : Type u) extends semilattice_inf α, order_top α.

errors with

type mismatch at application
  @semilattice_inf.to_partial_order α top
term
  top
has type
  α
but is expected to have type
  semilattice_inf α

One can make this work through one of three ways: No old_structure_cmd, which is unfriendly to the rest of the class hierarchy Require has_le in class mwe (α : Type u) [has_le α] extends semilattice_inf α, order_top α., which is unfriendly to the existing hierarchy and how lemmas are stated. Provide an additional axiom on top of a "data-only" TC and have a low-priority instance:

class semilattice_inf_top (α : Type u) extends semilattice_inf α, has_top α :=
(le_top : ∀ a : α, a ≤ ⊤)
@[priority 100]
instance semilattice_inf_top.to_order_top : order_top α :=
{ top := ⊤,  le_top := semilattice_inf_top.le_top }

The third option is chosen in this refactor. Pulled out from #9891, without the semilattice refactor.