nonlinarith

Stream: maths

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

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]

I just tried goofing around with apply_rules but I'm a first-timer.

[Kevin Buzzard]

Does mono help?

[Reid Barton]

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

[Reid Barton]

actually it works even without the with part

[Reid Barton]

Kind of weird that mono can't deduce 0 ≤ A from 0 ≤ a and a ≤ A itself

[Kevin Buzzard]

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]

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]

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]

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

[Kevin Buzzard]

Still, this is much better than what I had!

[Reid Barton]

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]

by undergrad

[Kevin Buzzard]

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]

It's just "obvious".

[Reid Barton]

I had never tried out mono before so this was also enlightening for me

[Kevin Buzzard]

Well thanks @Patrick Massot too.

[Kevin Buzzard]

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

[Johan Commelin]

@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]

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.