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

Stream: new members

[Marko Grdinić]

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.

[Mario Carneiro]

ring is not a simplifier

[Mario Carneiro]

it's supposed to kill the goal

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Marko Grdinić]

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
    }

[Marko Grdinić]

Thanks.

[Kenny Lau]

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