## 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