Zulip Chat Archive

Stream: maths

Topic: nonlinarith


view this post on Zulip 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".

view this post on Zulip Kevin Buzzard (Jan 28 2019 at 23:16):

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

view this post on Zulip 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...

view this post on Zulip Kevin Buzzard (Jan 28 2019 at 23:17):

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

view this post on Zulip Kevin Buzzard (Jan 28 2019 at 23:18):

Does mono help?

view this post on Zulip Reid Barton (Jan 28 2019 at 23:28):

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

view this post on Zulip Reid Barton (Jan 28 2019 at 23:29):

actually it works even without the with part

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Reid Barton (Jan 28 2019 at 23:39):

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

view this post on Zulip Kevin Buzzard (Jan 28 2019 at 23:40):

Still, this is much better than what I had!

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Jan 28 2019 at 23:40):

by undergrad

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Jan 28 2019 at 23:42):

It's just "obvious".

view this post on Zulip Reid Barton (Jan 28 2019 at 23:42):

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

view this post on Zulip Kevin Buzzard (Jan 28 2019 at 23:42):

Well thanks @Patrick Massot too.

view this post on Zulip Kevin Buzzard (Jan 28 2019 at 23:44):

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

view this post on Zulip 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...

view this post on Zulip 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