Zulip Chat Archive

Stream: new members

Topic: Using mul_lt_one_of_le_of_lt for reals


Brendan Seamas Murphy (Aug 22 2022 at 21:30):

I have a goal a * b < 1 where I know 0 <= a <= 1 and 0 <= b < 1. I wanted to conclude using mul_lt_one_of_le_of_lt, but I get the error invalid apply tactic, failed to synthesize type class instance for covariant_class ℝ ℝ has_mul.mul has_lt.lt. I've see these covariant_class things before in lemmas but this is the first time I've run into an issue with them. It seems like the issue is that if c <= 0 then x < y does not imply c * x < c * y. What's the easiest way to apply (something equivalent to) this lemma in my situation?

Yaël Dillies (Aug 22 2022 at 21:36):

docs#mul_lt_one_of_nonneg_of_lt_one_left

Yaël Dillies (Aug 22 2022 at 21:37):

Sorry, algebraic order lemmas are a bit of a maze!

Brendan Seamas Murphy (Aug 22 2022 at 21:46):

thanks!

Damiano Testa (Aug 23 2022 at 02:07):

Btw, the covariant_class you mention is the statement that multiplication by any given real on the left is strictly monotone.

The has_mul field tells you which operation to use and the has_lt which relation. The vast majority of covariant classes in mathlib use + or * as operation on the left, their swap for operations on the right, and or < for monotone/strictly monotone.

The first two fields that are both in your case, would be superfluous, if it were easy to deduce from the operation which type is acting on which type.

Damiano Testa (Aug 23 2022 at 02:47):

Btw, if you want to use fancier covariant typeclasses, this also works:

import data.real.basic

example {a b : } (a0 : 0  a) (a1 : a  1) (b0 : 0  b) (b1 : b < 1) : a * b < 1 :=
zero_lt.mul_lt_of_le_of_lt_one' a1 b1 b0 zero_lt_one

Note that docs#zero_lt.mul_lt_of_le_of_lt_one' is a lemma that is not real-specific.
Edit: I see now that Yaël's suggestion is also not real-specific! What I meant is that it does not use the ordered_semiring typeclass.


Last updated: Dec 20 2023 at 11:08 UTC