Cauchy-Schwarz calc

Stream: maths

[Patrick Massot]

Sometimes when someone new comes here to ask maths questions, I wonder if we have a new mathematician interested in Lean. So I googled @Patrick Stevens and found https://www.patrickstevens.co.uk/cauchy-schwarz-proof/

[Patrick Massot]

So I thought: good opportunity to try again to compute with Lean

[Patrick Massot]

And of course I'm disappointed

[Patrick Massot]

import tactic.ring
import analysis.real


lemma key (a b x y : real) : x > 0 →  y > 0 → (a+b)^2/(x+y) ≤ a^2/x + b^2/y :=
begin
  intros x_pos y_pos,
  have : x + y > 0 := add_pos_of_pos_of_nonneg x_pos (le_of_lt y_pos),
  suffices : (a+b)^2 ≤ (x+y)*(a^2/x + b^2/y),
  { apply div_le_of_le_mul ; assumption  },
  apply le_of_sub_nonneg,
  apply le_of_mul_le_mul_right _ x_pos,
  apply le_of_mul_le_mul_right _ y_pos,
  rw mul_sub_right_distrib,
  rw mul_sub_right_distrib,
  suffices : 0 ≤ -((a + b) ^ 2 * x * y) + (x + y) * (a ^ 2 / x + b ^ 2 / y) * x * y,
  by simp [*],
  conv
  { to_rhs,
    congr,
    skip,
    rw mul_assoc,
    rw mul_assoc,
    congr,
    skip,
    rw right_distrib,
    rw ←mul_assoc,
    rw div_mul_cancel _ (ne_of_gt x_pos),
    rw (show b ^ 2 / y * (x * y) = b ^ 2 / y * (y*x), by simp[mul_comm]),
    rw ←mul_assoc,
    rw div_mul_cancel _ (ne_of_gt y_pos) },
  have : -((a + b) ^ 2 * x * y) + (x + y) * (a ^ 2 * y + b ^ 2 * x) = (a*y-b*x)^2 :=
    begin
      ring,ring,
    end,
  rw this,
  suffices : 0 ≤ (a * y - b * x)*(a * y - b * x),
  { rw pow_succ,
    finish },
  apply mul_self_nonneg,
end

[Patrick Massot]

It's not only about the banana phone issue

[Patrick Massot]

Everything has been painful

[Patrick Massot]

How should I write such proofs?

[Patrick Stevens]

That's quite a collection - it's a direct conversion of the one I linked, isn't it, which is very slick for human consumption

[Patrick Stevens]

Presumably there are easier proofs to transcribe for Lean

[Andrew Ashworth]

someday, https://en.wikipedia.org/wiki/Cylindrical_algebraic_decomposition might show up in Lean

[Patrick Massot]

only the key lemma "Naturally, this lemma is trivial — once it is conceived."

[Patrick Massot]

My interest was not in proving Cauchy-Schwarz. It was this sentence "Naturally, this lemma is trivial — once it is conceived."

[Kenny Lau]

use better theorems

[Kenny Lau]

e.g. you can use add_pos instead of that business

[Patrick Massot]

I did the exercise on paper in 30 seconds and thought I would try in Lean

[Kenny Lau]

add_pos_of_pos_of_nonneg x_pos (le_of_lt y_pos)

[Kenny Lau]

and e.g. there is a theorem linking (x+y)^-1 to x^-1 and y^-1

[Patrick Massot]

I couldn't find add_pos because I was looking for add_pos_of_pos_of_pos

[Patrick Massot]

The question is: I stare at my paper proof, how can I get a Lean proof?

[Kenny Lau]

a lot of training and familiarity with existing theorems

[Patrick Massot]

I did that as training indeed

[Patrick Massot]

But probably Andrew is right

[Patrick Massot]

We need more automation

[Patrick Massot]

nothing else is viable

[Patrick Massot]

Note that the situation would be much worse without ring

[Andrew Ashworth]

there are limits to algorithms such as the above though. they will take forever to run if you have a particularly giant set of real inequalities since the time it takes to run increases exponentially vs the number of terms

[Kenny Lau]

I disagree

[Kenny Lau]

but I don't have time to disprove your claim

[Patrick Massot]

I should be sleeping anyway (of course I thought this calculation would be shorter...)

[Patrick Stevens]

Of course, "expand and clear denominators" should be mechanically easy, right? Is there some reason why an "expand" tactic couldn't exist? and "clear denominators" likewise, though that requires a bit of casewise am-i-negative reasoning in general

[Andrew Ashworth]

if you stuck the same equation into Sage math, what would its simplifier spit out?

[Patrick Stevens]

Mathematica:

In[43]:= (a + b)^2/(x + y) <= a^2/x + b^2/y //
 FullSimplify[#, x > 0 && y > 0] &

Out[43]= (b x - a y)^2 >= 0

[Patrick Stevens]

simplifies to True under the additional assumption that a,b are real

[Patrick Stevens]

don't know about sage, i'm afraid

[Kenny Lau]

import data.real.basic tactic.ring

lemma key (a b x y : ℝ) (Hx : x > 0) (Hy : y > 0) :
  (a+b)^2/(x+y) ≤ a^2/x + b^2/y :=
have H : ((x+y)*x*y)*((a+b)^2/(x+y)) ≤ ((x+y)*x*y)*(a^2/x + b^2/y),
from calc ((x+y)*x*y)*((a+b)^2/(x+y))
    = x*(y*(a+b)^2) : by rw [← mul_div_assoc, mul_assoc, mul_assoc, mul_div_cancel_left];
  from ne_of_gt (add_pos Hx Hy)
... ≤ x*(y*(a+b)^2) + (a*y-b*x)*(a*y-b*x) : le_add_of_nonneg_right $ mul_self_nonneg _
... = (x+y)*(y*a^2) + (x+y)*(x*b^2) : by ring
... = ((x+y)*x*y)*(a^2/x + b^2/y) :
  by rw [mul_add, ← mul_div_assoc, mul_assoc, mul_assoc, mul_assoc, mul_assoc, mul_div_cancel' _ (ne_of_gt Hy), mul_div_assoc, mul_div_cancel_left _ (ne_of_gt Hx)],
le_of_mul_le_mul_left H $ mul_pos (mul_pos (add_pos Hx Hy) Hx) Hy

[Kenny Lau]

ok I did use ring

[Kenny Lau]

@Patrick Massot

[Kenny Lau]

and I just burnt a lot of my time

[Kenny Lau]

I'm busy

[Mario Carneiro]

import tactic.ring data.real.basic

theorem pow_two_nonneg {α} [linear_ordered_ring α] (a : α) : 0 ≤ a ^ 2 :=
by rw pow_two; exact mul_self_nonneg _

lemma key (a b x y : ℝ) (x0 : 0 < x) (y0 : 0 < y) : (a+b)^2/(x+y) ≤ a^2/x + b^2/y :=
begin
  apply (div_le_iff (add_pos x0 y0)).2,
  apply (mul_le_mul_left (mul_pos x0 y0)).1,
  apply sub_nonneg.1,
  refine calc x * y * ((a ^ 2 / x + b ^ 2 / y) * (x + y)) - x * y * (a + b) ^ 2
       = ((x / x * a ^ 2 * y + y / y * b ^ 2 * x) * (x + y)) - x * y * (a + b) ^ 2 : by ring
   ... = ((a ^ 2 * y + b ^ 2 * x) * (x + y)) - x * y * (a + b) ^ 2 : by simp [ne_of_gt x0, ne_of_gt y0]
   ... = (b * x - a * y) ^ 2 : by ring; ring
   ... ≥ 0 : pow_two_nonneg _
end

[Mario Carneiro]

Since ring can handle everything except the divisions, I insert a step in the middle for simp to cancel the x/x terms, but otherwise this is all ring

[Mario Carneiro]

or with a bit more up front cross multiplication:

lemma key (a b x y : ℝ) (x0 : 0 < x) (y0 : 0 < y) : (a+b)^2/(x+y) ≤ a^2/x + b^2/y :=
begin
  rw [div_add_div _ _ (ne_of_gt x0) (ne_of_gt y0),
    div_le_iff (add_pos x0 y0), div_mul_eq_mul_div, le_div_iff (mul_pos x0 y0),
    ← sub_nonneg],
  refine calc 0 ≤ (b * x - a * y) ^ 2 : pow_two_nonneg _
   ... = (a ^ 2 * y + x * b ^ 2) * (x + y) - (a + b) ^ 2 * (x * y) : by ring; ring
end

[Andrew Ashworth]

^. I feel like whenever I have a complicated thing like this, calc is the way to go. And I solve the whole thing by hand on scratch paper, like I time-traveled back to high-school algebra class...

[Kenny Lau]

throwbacks

[Andrew Ashworth]

but if this stuff is super obvious, and you dislike proving it, why not use sorry?

[Patrick Massot]

Thank you very much Kenny and Mario. Kenny's proof is exactly what I don't want to do (and nobody should have to do if proof assistants want to become tools for mathematicians). Mario's proof is what I wanted to do (clear denominators and use ring). I think the most important thing I missed was:

example (a x y : ℝ) : x * y * (a^2 / x) =  y * (a^2 *x / x) := by ring

I thought that, in such a case, ring would see (a^2 / x) as atomic and fail. It makes it even harder for me to understand why ring couldn't be extended to do the whole computation, searching for x > 0 or x ≠ 0 in context

[Johan Commelin]

ring doesn't know anything about orders, right? So it doesn't know what to do with x > 0.

[Patrick Massot]

it could try to apply ne_of_gt and ne_of_lt on all hypotheses

[Patrick Massot]

One more question for Mario: why did you use refine instead of exact, which also works and is more explicit?

[Johan Commelin]

Buth it isn't meant to be a generic tactic. It only uses ring axioms.

[Patrick Massot]

Then give another name to the more general tactic

[Johan Commelin]

But you would want to do something like by schoolkid using ring or something like that

[Johan Commelin]

We want a schoolkid tactic that does the completely easy stuff, and it should have a feature that you can give it a specialised tactic like ring as a hint, so that all of a sudden the schoolkid is lord of the rings.

[Patrick Massot]

What about building a clear_denominator tactic? It would search for all divisions in the goal, generate sub-goals saying denominators are non-zero, try to discharge these goals using assumptions (and ne_of_gt and ne_of_lt of assumptions), check whether the goal is equality or inequality and apply mul_le_mul_left and its friend, followed by ring to simplify, and simp [all stuff ≠ 0 gathered so far]

[Patrick Massot]

We really need to get back Simon

[Patrick Massot]

@Simon Hudon where are you?

[Johan Commelin]

Right. A clear denominator tactic makes sense as well.

[Johan Commelin]

So, here is a proposal for @Kevin Buzzard 's next "Live Zulip": walk through a tactic file, and teach mathematicians how to write tactics (-;

[Simon Hudon]

Hey @Patrick Massot! I haven't completely disappeared. Is it just me or has there been a whole lot more activity in here? It's getting hard to follow part time!

[Simon Hudon]

I'm not sure I get what clear_denominator would do exactly. How does mul_le_mul_left help with division?

[Sean Leather]

Is it just me or has there been a whole lot more activity in here?

It's not just you. Even being away from Zulip for a weekend leaves one with thousands of messages to either wade through or mark as read. :stuck_out_tongue_closed_eyes:

[Simon Hudon]

I thought the Zulip threads would help keeping track of stuff. I'm not sure what would make it easier

[Simon Hudon]

The plus side is, it's awesome that Lean is getting used like this

[Patrick Massot]

We have trouble with thread discipline

[Patrick Massot]

But we try

[Simon Hudon]

Yeah? What kind of trouble? It seems like specific threads are getting created for the right subjects. The problem might just be in the number of threads. I don't know if we need to categorize them better or something else

[Patrick Massot]

Many thread actually mix different topics

[Mario Carneiro]

I think Kevin should speak in complete sentences

[Mario Carneiro]

instead of fragments

[Mario Carneiro]

of sentences

[Mario Carneiro]

that create tons of messages and fill

[Mario Carneiro]

my screen

[Simon Hudon]

Yeah I noticed that too. Also, write one message with one self contained question and wait for an answer. Right now, when I see his messages I don't know when he's going to be done writing and I eventually just stop reading. One message would help me (and I suspect others) decide whether the question is something I can help with

[Patrick Massot]

Why did you provoked him?!

[Simon Hudon]

Provoke how?

[Patrick Massot]

Did you see how many times he hit return in the middle of a sentence since you posted that message?

[Patrick Massot]

That's all your fault :stuck_out_tongue_winking_eye:

[Simon Hudon]

Haha! I'm secretly a terrorist!

[Simon Hudon]

Sorry typo: theorist

[Simon Hudon]

I don't follow that thread so I didn't suffer the consequences of that carnage

[Kevin Buzzard]

So, here is a proposal for @Kevin Buzzard 's next "Live Zulip": walk through a tactic file, and teach mathematicians how to write tactics (-;

So I was just catching up in this thread, and you and Patrick were talking about tactics and "maybe Simon can write us a tactic" -- and who is the only mathematician who knows how to write tactics? I reckon it's @Scott Morrison . Scott -- how did you learn to write tactics? I don't want to keep pestering Simon. I see dumb stuff like the proof that pnat is a comm_monoid, and the proof of every axiom is "it's true for nat so done"

[Kevin Buzzard]

and that happened to me several times myself when doing comm_ring stuff with schemse

[Kevin Buzzard]

"I've got to prove this direct limit satisfies all the ring axioms"

[Kevin Buzzard]

"let's see what this entails"

[Kevin Buzzard]

"it entails invoking that same axiom for that other ring"

[Kevin Buzzard]

It's about time I learnt to automate that. It comes up a lot.

[Kevin Buzzard]

When we start on perfectoid spaces we'll be proving limits of topological rings are topological rings

[Kevin Buzzard]

there's going to be a lot of "this proof is obvious but not rfl" stuff

[Kevin Buzzard]

and this can surely be done with tactics

[Simon Hudon]

I actually enjoy getting your automation challenges. I admit (sorry!) that I'm not as quick to address them as I'd like. And lately, I've only gotten slower as I took a part time job and stepped up my writing efforts

[Sebastien Gouezel]

Just for fun, I checked it in Isabelle to see where next-level automation can get you. It did not work directly, but almost:

lemma
  fixes a b x y::real
  assumes "x > 0" "y > 0"
  shows "(a+b)^2/(x+y) ≤ a^2/x + b^2/y"
proof -
  have "(a * y - b * x)^2 ≥ 0" by simp
  then show ?thesis
    using assms by (simp add: algebra_simps divide_simps power2_eq_square)
qed

I first tried to show the goal just by applying simp with divide_simps and algebra_simps (simplification rules which clear out divisors, and apply associativity, commutativity), but square expansion is not automatic so I had to add it simp. It reduced everything to something which clearly was equivalent to the positivity of (ay-bx)^2, so I added it as an intermediate step, and done. No piece of paper, no computation on my side (and no fancy tactic such as ring or omega, everything was done by the simplifier). I really hope Lean can do the same in the near future!

[Mario Carneiro]

The main problem with using simp for ring equalities is that simp isn't good with cancelling negatives

[Sebastien Gouezel]

To be honest, simp in Isabelle is in fact simp on steroids: it has built-in "simprocs" that will cancel out negatives, group together common factors, and things like that. I guess it makes by (simp add: algebra_simps) as powerful as the ringtactic in Lean. If I understand correctly, Johannes is working on simprocs for Lean, right?

[Johannes Hölzl]

Yes, I'm working on a simplifier tactic with simp proc support.

[Johan Commelin]

Is there a one-line explanation of what "simpprocs" are?

[Johannes Hölzl]

instead of simp rules, it is a tactic which gets invoced by the simplifier. E.g. canellation would be a simproc which is called on a pattern of the form _ = _ where the type of _ has a cancellative monoid, then it tries to find common elements on both sides of the equation and remove them.