covariant_class ℝ and ring_nf in calc

Stream: new members

[Patrick Johnson]

While practicing calc proof mode, I got stuck on this simple inequality:

import tactic
import data.real.basic

example {a b : ℝ}
  (h₁ : a > 0)
  (h₂ : b > 0) :
  (a + b) * (1 / a + 4 / b) ≥ 9 :=
begin
  apply sub_nonneg.mp,
  apply (mul_le_mul_right (mul_pos h₁ h₂)).mp,
  rw zero_mul,
  calc _ ≤ (2 * a - b) ^ 2 : sq_nonneg _
  ...    ≤ (a + b) * (b + 4 * a) - 9 * a * b : by ring_nf
  ...    ≤ ((a + b) * (1 / a + 4 / b) - 9) * (a * b) : sorry,
  sorry,
end

So I am interested to know:

• Why can't the first sorry be solved by ring_nf?
• Why does the second sorry ask me to prove covariant_class ℝ ℝ (function.swap has_add.add) has_le.le?
• Can this proof be simplified somehow?

[Kevin Buzzard]

Division isn't a thing in rings, and neither is <=, so the first sorry is out of scope for ringlike tactics for two reasons. There's a "clear denominators" tactic, and you probably want to change the <= to an =.

[Alex J. Best]

Also if things are equalities rather than inequalities you can state them as such, calc will still produce an inequality from a chain of \le and =, edit: oops just saw kevin already wrote this

[Alex J. Best]

P.s. its always easier to help if you include the imports, in this case import data.real.basic

[Kevin Buzzard]

Why if I use the (correct) ring instead of ring_nf the line above the first sorry, does it close the relevant goal and still tell me to use ring_nf? Is this a bug?

[Rob Lewis]

Kevin Buzzard said:

Why if I use the (correct) ring instead of ring_nf the line above the first sorry, does it close the relevant goal and still tell me to use ring_nf? Is this a bug?

Is your mathlib up to date? Mario made a couple changes to ring this week, one to address a bug exactly like this

[Kevin Buzzard]

Is your mathlib up to date?

It is!

[Rob Lewis]

Oh, ring_nf is the right tactic there. ring is for equations, this is proving an inequality by normalizing to 0 <= 0

[Kevin Buzzard]

Why does the second sorry ask me to prove covariant_class ℝ ℝ (function.swap has_add.add) has_le.le?

This goal appeared when you did the unconventional apply sub_nonneg.mp, as you can see if you put your cursor before and after that tactic. apply is not always the cleverest when it comes to type class inference. You would be better off doing rw \l sub_nonneg. You can solve the second goal with apply_instance, the tactic which says "solve this goal using type class inference".

[Kevin Buzzard]

Oh, except the rewrite fails because you have you have not written your example in Lean's normal form: you should use <= not >=.

[Kevin Buzzard]

import data.real.basic
import tactic.field_simp -- clear denominator tactic
example {a b : ℝ}
  (h₁ : 0 < a)
  (h₂ : 0 < b) :
  9 ≤ (a + b) * (1 / a + 4 / b) :=
begin
  rw ← sub_nonneg,
  apply (mul_le_mul_right (mul_pos h₁ h₂)).mp,
  rw zero_mul,
  calc _ ≤ (2 * a - b) ^ 2 : sq_nonneg _
  ...    = (a + b) * (b + 4 * a) - 9 * a * b : by ring
  ...    = ((a + b) * (1 / a + 4 / b) - 9) * (a * b) : _,
  field_simp [(ne_of_gt h₁), (ne_of_gt h₂)],
  ring,
end