Zulip Chat Archive
Stream: maths
Topic: algebra order refactor
Sebastien Gouezel (May 21 2021 at 09:40):
@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 (May 21 2021 at 09:57):
That is a fabulous example :-)
Johan Commelin (May 21 2021 at 10:02):
Johan Commelin (May 21 2021 at 10:03):
It seems to me that there are just too many typeclass assumptions in the lemma.
Damiano Testa (May 21 2021 at 10:04):
Sébastien, thanks for your interesting test case: I am going to take a look now!
Sebastien Gouezel (May 21 2021 at 10:04):
Note that this is a complicated example: it is not true that a < b -> a + c < b + c
.
Damiano Testa (May 21 2021 at 10:05):
... the powers of infinity...
Damiano Testa (May 21 2021 at 10:14):
First of all, here is a lemma with fewer assumptions. I have not yet checked that the typeclasses apply to ennreals, though.
Damiano Testa (May 21 2021 at 10:14):
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 (May 21 2021 at 10:19):
I might have gone down the trap that Sébastien warned about, though... let me try again!
Damiano Testa (May 21 2021 at 11:05):
@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 (May 21 2021 at 11:13):
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 (May 21 2021 at 11:13):
To be more specific:
covariant
states the monotonicity of an operation,contravariant
states the "contrapositive", that is, you deduce an inequalitya < b
if you know an inequalitya + 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 (May 21 2021 at 11:15):
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 (May 21 2021 at 21:31):
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 (May 22 2021 at 09:55):
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.
Last updated: Dec 20 2023 at 11:08 UTC