factoring out order_top/bot

Stream: general

[Yakov Pechersky]

I'm thinking of unbundling the order structure from order_{top,bot}, making order_top require [has_le] and extend solely [has_top]. The proofs about it will now have a [partial order] added. This is because I'd like to have a type that is both linear_order and order_top. This should also "simplify" things like linear_add_comm_group_with_top, those should be separated into something like linear_order, add_comm_group, covariant_class _ _, order_top. What do you think?

Some complications are that existing classes like semilattice_{inf,sup}_{bot,top} don't exist anymore, and bounded_distrib_lattice becomes something like [distrib_lattice] [bounded] where [bounded] is [order_top] [order_bot].

Yury asked that I discuss this in #general.

[Floris van Doorn]

This sounds reasonable to me. It is quite unmanageable to put all combinations into a single class.
With your suggested change, we can also get rid of something like docs# conditionally_complete_linear_order_bot.
If a certain class (maybe bounded_lattice?) is popular enough, we could still decide that it deserves to stay a single class (instead of being split up into [distrib_lattice] [...]). I think the order refactor so far has shown that this also works quite well (with something like ordered_comm_monoid being able to use lemmas with covariant_class arguments). I'm not saying that we should do this with any particular class, but it's good to keep in mind as an option.

[Sebastien Gouezel]

+1 for having order_top as a mixin for general purpose lemmas.

[Yaël Dillies]

My personal experience is that I defined distrib_lattice_bot for generalizing < 10 lemmas and I now need lattice_bot for a definition to be in the correct generality.

[Eric Rodriguez]

I've often thought about math libraries with everything being a mixin, e.g. [group α] = [has_mul α] [has_inv α] [has_one α] [is_identity 1] [associative α] [is_left_inverse (*) (⁻¹)] [is_right_inverse (*) (⁻¹)], and then when you prove something for a group/ring/whatever the proof assistant would use the minimal axioms actually required

[Eric Rodriguez]

I wonder how that would be for a proving experience... anyways, I'm 100% for this

[Yakov Pechersky]

branch#pechersky/linear-top-order, where I've started doing it just to order.bounded_lattice first, since that is where the classes are defined.

[Yaël Dillies]

What do you think of unbundling only bot first?

[Yaël Dillies]

I expect both could be refactored quite independently, and if we prioritise one, I'd say order_bot seems to come up more often.

[Yakov Pechersky]

I think with_top comes up often too, in the linear_algebra_structure_with_infty that we have.

[Yury G. Kudryashov]

I think, bot and top should remain order dual, so we should unbundle both of them in one PR.