redefine has_ordered_sub

Stream: general

[Violeta Hernández]

Here's a petition. Currently, the docs#has_ordered_sub typeclass has ∀ (a b c : α), a - b ≤ c ↔ a ≤ c + b as an assumption. I want it to have ∀ (a b c : α), a - b ≤ c ↔ a ≤ b + c instead. The key difference is that this would allow us to put a has_ordered_sub instance on ordinals. I think every current concrete instance is with commutative addition, so this change shouldn't impact it.

[Violeta Hernández]

I think this may have already been the original intention. Quoting from the docstring:

In other words, a - b is the least c such that a ≤ b + c.

This of course is only true in noncommutative contexts with the redefinition I'm proposing.

[Violeta Hernández]

Also, almost all of the API is proven with the add_comm_semigroup assumption.

[Violeta Hernández]

Oh actually, this change is actually very easy to do

[Violeta Hernández]

It's literally just swapping a few _right lemmas with a few _left lemmas and that's it

[Violeta Hernández]

Yeah let's try this: #15991

[Violeta Hernández]

Oh, wait

[Violeta Hernández]

This change would mean that additive groups no longer have an ordered substraction

[Violeta Hernández]

That's probably undesirable

[Violeta Hernández]

I guess we could make two separate classeshas_left_ordered_sub and has_right_ordered_sub but maybe that's overkill

[Violeta Hernández]

Actually, having two separate classes might not be such a bad idea. We do have a concrete purpose for each, after all.

[Violeta Hernández]

I wish we had more examples of has_left_ordered_sub though, i.e. the one for ordinals

[Violeta Hernández]

I guess docs#nonote would also have a has_left_ordered_sub instance, so that's two examples?

[Violeta Hernández]

Kind of a lame example since that's basically just ordinals again and there's not all that much API on that, but still

[Junyan Xu]

I think ordinal subtraction should really be written -a+b, but mathlib lacks a typeclass/notation for subtraction/division/quotient from the left ... I guess that's partially because mathlib doesn't have https://en.m.wikipedia.org/wiki/Quasigroup

[Junyan Xu]

We're about to get Jordan algebras. How about octonions and Moufang loops?

We also see left exponential notation in https://en.m.wikipedia.org/wiki/Racks_and_quandles

[Floris van Doorn]

The current definition of has_ordered_sub feels a lot more canonical, since you're adding/subtracting b on the right on both sides of the ↔. It's unfortunate that it doesn't apply for ordinals indeed, but I don't think it's worth it to add a separate class just for ordinal (and nonote), unless we find more examples.

[Eric Wieser]

Presumaby things like ordinal × ordinal are also examples, but I don't think they're interesting enough unless you have a convincing use for them

[Violeta Hernández]

I think we also have structures order-isomorphic to subsets of ordinals as examples, such as the lex sum of N and N

[Violeta Hernández]

Though in that case addition is badly behaved too

[Junyan Xu]

I think the docs#add_opposite of ordinals will satisfy has_ordered_sub, if sub is unchanged even though add is swapped.

[Violeta Hernández]

Could we use that to easily port theorems of has_ordered_sub to ordinals?