# Zulip Chat Archive

## Stream: maths

### Topic: nonlinarith

#### Kevin Buzzard (Jan 28 2019 at 23:15):

import data.real.basic example (a b c d A B C D : ℝ) (ha : 0 ≤ a) (hb : 0 ≤ b) (hc : 0 ≤ c) (hd : 0 ≤ d) (hA : a ≤ A) (hB : b ≤ B) (hC : c ≤ C) (hD : d ≤ D) : a * b + c * d ≤ A * B + C * D := sorry

How am I supposed to be solving goals like this? Is there a tactic that Coq has which can just do this? I think that if I were to ask an undergrad they'd say it was "obvious".

#### Kevin Buzzard (Jan 28 2019 at 23:16):

[in my use case a,b,c,d are all of the form `|x|`

]

#### Kevin Buzzard (Jan 28 2019 at 23:16):

import data.real.basic example (a b c d A B C D : ℝ) (ha : 0 ≤ a) (hb : 0 ≤ b) (hc : 0 ≤ c) (hd : 0 ≤ d) (hA : a ≤ A) (hB : b ≤ B) (hC : c ≤ C) (hD : d ≤ D) : a * b + c * d ≤ A * B + C * D := calc a * b + c * d ≤ A * b + c * d : add_le_add_right (mul_le_mul_of_nonneg_right hA hb) _ ... ≤ A * B + c * d : add_le_add_right (mul_le_mul_of_nonneg_left hB (le_trans ha hA)) _ ... ≤ A * B + C * d : add_le_add_left (mul_le_mul_of_nonneg_right hC hd) _ ... ≤ A * B + C * D : add_le_add_left (mul_le_mul_of_nonneg_left hD (le_trans hc hC)) _

I'm assuming this is golfable...

#### Kevin Buzzard (Jan 28 2019 at 23:17):

I just tried goofing around with `apply_rules`

but I'm a first-timer.

#### Kevin Buzzard (Jan 28 2019 at 23:18):

Does `mono`

help?

#### Reid Barton (Jan 28 2019 at 23:28):

`by mono* with [0 ≤ A, 0 ≤ C]; linarith`

#### Reid Barton (Jan 28 2019 at 23:29):

actually it works even without the `with`

part

#### Reid Barton (Jan 28 2019 at 23:30):

Kind of weird that `mono`

can't deduce `0 ≤ A`

from `0 ≤ a`

and `a ≤ A`

itself

#### Kevin Buzzard (Jan 28 2019 at 23:32):

Right -- I was trying

attribute [mono_rules] add_le_add_right add_le_add_left mul_le_mul_of_nonneg_right mul_le_mul_of_nonneg_left le_trans

and then `by apply_rules mono_rules`

but the `le_trans`

makes it loop, and without it it can't do it.

#### Kevin Buzzard (Jan 28 2019 at 23:35):

example (a b c d A B C D : ℝ) (hA : abs a ≤ A) (hB : abs b ≤ B) (hC : abs c ≤ C) (hD : abs d ≤ D) : abs a * abs b + abs c * abs d ≤ A * B + C * D := sorry

Maybe this one is harder. How do I insert the `abs`

into the picture? Note `abs_nonneg : ∀ (a : ?M_1), abs a ≥ 0`

#### Kevin Buzzard (Jan 28 2019 at 23:39):

import data.real.basic tactic.linarith example (a b c d A B C D : ℝ) (hA : abs a ≤ A) (hB : abs b ≤ B) (hC : abs c ≤ C) (hD : abs d ≤ D) : abs a * abs b + abs c * abs d ≤ A * B + C * D := begin have : abs a ≥ 0 := abs_nonneg _, have : abs b ≥ 0 := abs_nonneg _, have : abs c ≥ 0 := abs_nonneg _, have : abs d ≥ 0 := abs_nonneg _, mono*;linarith end

Is there a better way of inserting `abs_nonneg`

into the picture?

#### Reid Barton (Jan 28 2019 at 23:39):

That's basically what I was about to write except with `have := abs_nonneg a`

, etc.

#### Kevin Buzzard (Jan 28 2019 at 23:40):

Still, this is much better than what I had!

#### Reid Barton (Jan 28 2019 at 23:40):

I don't know if we have enough smarts to figure out to prove 0 <= A from the assumption abs a <= A and the lemma 0 <= abs a

#### Kevin Buzzard (Jan 28 2019 at 23:40):

`by undergrad`

#### Kevin Buzzard (Jan 28 2019 at 23:42):

Thanks Reid, by the way! The more my code looks like how a maths undergraduate thinks, the better it is. I don't think they're thinking about `mul_le_mul_of_nonneg_right`

, at least not explicitly.

#### Kevin Buzzard (Jan 28 2019 at 23:42):

It's just "obvious".

#### Reid Barton (Jan 28 2019 at 23:42):

I had never tried out `mono`

before so this was also enlightening for me

#### Kevin Buzzard (Jan 28 2019 at 23:42):

Well thanks @Patrick Massot too.

#### Kevin Buzzard (Jan 28 2019 at 23:44):

https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/linarith.20failure/near/157061326

#### Johan Commelin (Jan 29 2019 at 07:24):

@Kevin Buzzard Can't you ask some former IMO participant to write a tactic that solves IMO-style inequalities? There are probably some among Imperial's first and second year students...

It would be cool if we have all the mean inequalities, and Chebyshev, Jensen, etc...

#### Kevin Buzzard (Jan 29 2019 at 07:44):

Yeah, we should tell Rob to add them to linarith :-) I am not sure how far you can get knowing all of those standard "IMO syllabus" inequalities, it always seemed to me that even if you knew them all you still needed more ideas to prove a random IMO inequality.

Last updated: May 06 2021 at 18:20 UTC