Zulip Chat Archive

Stream: new members

Topic: How to prove `(-2) * m * m + m ^ 2 ≤ (-2) * m * m' + m' ^ 2`


view this post on Zulip Marko Grdinić (Oct 16 2019 at 14:09):

More specifically example (m m' : rat) : (-2) * m * m + m ^ 2 ≤ (-2) * m * m' + m' ^ 2. The way to solve this is to add m ^ 2 on both sides which after simplifying should result in 0 <= (m - m')^2. The issue I am having is that for some reason ring is acting crazy and not simplifying anything. Sure I could pry this problem into shape using step by step tactics, but I am wondering if there is an elegant approach to this.

view this post on Zulip Mario Carneiro (Oct 16 2019 at 14:12):

ring is not a simplifier

view this post on Zulip Mario Carneiro (Oct 16 2019 at 14:12):

it's supposed to kill the goal

view this post on Zulip Mario Carneiro (Oct 16 2019 at 14:12):

it sometimes simplifies as a side effect but you shouldn't rely on it

view this post on Zulip Mario Carneiro (Oct 16 2019 at 14:13):

Also, those two expressions are already "simplified" from the POV of ring

view this post on Zulip Mario Carneiro (Oct 16 2019 at 14:22):

example (m m' : rat) : (-2) * m * m + m ^ 2  (-2) * m * m' + m' ^ 2 :=
@le_of_add_le_add_right _ _ _ (m^2) _ $
by convert (pow_two_nonneg (m - m')); ring

view this post on Zulip Marko Grdinić (Oct 16 2019 at 14:50):

Here is what I came up with. I definitely like your solution better.

example (m m' : rat) : (-2) * m * m + m ^ 2  (-2) * m * m' + m' ^ 2 :=
    by {
        simp,
        rw [mul_assoc,  pow_two,  add_assoc],
        rw add_comm (m' ^ 2) (2 * m ^ 2),
        rw two_mul,
        repeat {rw add_assoc},
        rw le_add_iff_nonneg_right,
        rw add_comm (m' ^ 2) (-(2 * m * m')),
        have : (m - m') ^ 2 = m ^ 2 + ((- (2 * m * m')) + m' ^ 2), by ring,
        rw  this,
        apply pow_two_nonneg
    }

view this post on Zulip Marko Grdinić (Oct 16 2019 at 14:50):

Thanks.

view this post on Zulip Kenny Lau (Oct 16 2019 at 23:39):

import data.rat tactic.ring

example (m m' : rat) : (-2) * m * m + m ^ 2  (-2) * m * m' + m' ^ 2 :=
calc  (-2) * m * m + m ^ 2
     (-2) * m * m + m ^ 2 + (m-m')^2 : le_add_of_nonneg_right (pow_two_nonneg _)
... = (-2) * m * m' + m' ^ 2          : by ring

Last updated: May 18 2021 at 17:44 UTC