algebra order refactor

Stream: maths

[Sebastien Gouezel]

@Damiano Testa , I need to prove a statement for which a step in the proof is that a + b < c + d when a < c and b < d. I want to state it in enough generality that it would apply both to reals and ennreals. So I had a look at the very general version of add_lt_add we have now, in terms of covariant and contravariant classes, but it seems that this version of the lemma does not apply to ennreal as this is not an add_cancel_monoid. Do you see a way out for me?

[Kevin Buzzard]

That is a fabulous example :-)

[Johan Commelin]

docs#add_lt_add

[Johan Commelin]

It seems to me that there are just too many typeclass assumptions in the lemma.

[Damiano Testa]

Sébastien, thanks for your interesting test case: I am going to take a look now!

[Sebastien Gouezel]

Note that this is a complicated example: it is not true that a < b -> a + c < b + c.

[Damiano Testa]

... the powers of infinity...

[Damiano Testa]

First of all, here is a lemma with fewer assumptions. I have not yet checked that the typeclasses apply to ennreals, though.

[Damiano Testa]

import algebra.ordered_ring

lemma sebastien {R : Type*} [comm_monoid R] [partial_order R] [covariant_class R R (*) (≤)]
  [covariant_class R R (function.swap (*)) (<)] {a b c d : R}
  (ac : a < c) (bd : b < d) :
  a * b < c * d :=
(mul_le_mul_left_n _ bd.le).trans_lt (mul_lt_mul_right' ac d)

[Damiano Testa]

I might have gone down the trap that Sébastien warned about, though... let me try again!

[Damiano Testa]

@Sebastien Gouezel , I am really not sure how to make your example work. As you mention, the top element in ennreal makes (some of) the new typeclasses not apply to this case: the ones that do not apply precisely fail because of top. Thus, it is not missing instances, it is that they do not apply. At the moment, I do not know of an order/operation mix typeclass that would work with ennreal.

[Sebastien Gouezel]

I agree with you that it does not fit in any natural class. Maybe I'll just create a typeclass has_add_lt_add and instantiate it both for ennreal and under the assumptions of your version of add_lt_add.

[Damiano Testa]

To be more specific:

• covariant states the monotonicity of an operation,
• contravariant states the "contrapositive", that is, you deduce an inequality a < b if you know an inequality a + c < b + c.

Thus, + is monotone (i.e. covariant_class ennreal ennreal (+) (≤)). Since the order is linear, it is also contrapositive monotone (i.e. contravariant_class ennreal ennreal (+) (<)).

However, the remaining covariant_class ennreal ennreal (+) (<) and contravariant_class ennreal ennreal (+) (≤)are false precisely because of the top-absorbing element.

[Damiano Testa]

Btw, this add_lt_add really feels like a non-trivial loop: all sides work with \le, you assume some <, but together they still fail to work with the given typeclasses. I really like this example (and I am also disappointed by the fact that it exists!).

[Kevin Buzzard]

Note that on the reals <= and < are one logical not and one noncanonical isomorphism neg : R -> R away from each other. For a general semiring this won't work.

[Damiano Testa]

Indeed, there are instance between the two assuming various levels of preorder, partial_order, linear_order, cancellability. I have not checked, but I think that for real, assuming only ≤ on the left might be enough to get all variations.