Zulip Chat Archive

Stream: maths

Topic: Cauchy-Schwarz calc


Patrick Massot (May 29 2018 at 21:51):

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 (May 29 2018 at 21:51):

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

Patrick Massot (May 29 2018 at 21:52):

And of course I'm disappointed

Patrick Massot (May 29 2018 at 21:52):

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 (May 29 2018 at 21:52):

It's not only about the banana phone issue

Patrick Massot (May 29 2018 at 21:53):

Everything has been painful

Patrick Massot (May 29 2018 at 21:53):

How should I write such proofs?

Patrick Stevens (May 29 2018 at 21:54):

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 (May 29 2018 at 21:54):

Presumably there are easier proofs to transcribe for Lean

Andrew Ashworth (May 29 2018 at 21:54):

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

Patrick Massot (May 29 2018 at 21:54):

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

Patrick Massot (May 29 2018 at 21:55):

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

Kenny Lau (May 29 2018 at 21:55):

use better theorems

Kenny Lau (May 29 2018 at 21:55):

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

Patrick Massot (May 29 2018 at 21:55):

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

Kenny Lau (May 29 2018 at 21:55):

add_pos_of_pos_of_nonneg x_pos (le_of_lt y_pos)

Kenny Lau (May 29 2018 at 21:56):

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

Patrick Massot (May 29 2018 at 21:56):

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

Patrick Massot (May 29 2018 at 21:57):

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

Kenny Lau (May 29 2018 at 21:57):

a lot of training and familiarity with existing theorems

Patrick Massot (May 29 2018 at 21:58):

I did that as training indeed

Patrick Massot (May 29 2018 at 21:58):

But probably Andrew is right

Patrick Massot (May 29 2018 at 21:58):

We need more automation

Patrick Massot (May 29 2018 at 21:58):

nothing else is viable

Patrick Massot (May 29 2018 at 21:59):

Note that the situation would be much worse without ring

Andrew Ashworth (May 29 2018 at 21:59):

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 (May 29 2018 at 21:59):

I disagree

Kenny Lau (May 29 2018 at 21:59):

but I don't have time to disprove your claim

Patrick Massot (May 29 2018 at 22:00):

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

Patrick Stevens (May 29 2018 at 22:03):

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 (May 29 2018 at 22:05):

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

Patrick Stevens (May 29 2018 at 22:07):

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 (May 29 2018 at 22:08):

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

Patrick Stevens (May 29 2018 at 22:08):

don't know about sage, i'm afraid

Kenny Lau (May 29 2018 at 22:24):

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 (May 29 2018 at 22:24):

ok I did use ring

Kenny Lau (May 29 2018 at 22:24):

@Patrick Massot

Kenny Lau (May 29 2018 at 22:24):

and I just burnt a lot of my time

Kenny Lau (May 29 2018 at 22:24):

I'm busy

Mario Carneiro (May 29 2018 at 22:35):

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 (May 29 2018 at 22:37):

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 (May 29 2018 at 22:52):

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 (May 29 2018 at 23:04):

^. 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 (May 29 2018 at 23:05):

throwbacks

Andrew Ashworth (May 29 2018 at 23:06):

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

Patrick Massot (May 30 2018 at 07:25):

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 (May 30 2018 at 07:27):

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

Patrick Massot (May 30 2018 at 07:28):

it could try to apply ne_of_gt and ne_of_lt on all hypotheses

Patrick Massot (May 30 2018 at 07:29):

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

Johan Commelin (May 30 2018 at 07:29):

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

Patrick Massot (May 30 2018 at 07:30):

Then give another name to the more general tactic

Johan Commelin (May 30 2018 at 07:30):

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

Johan Commelin (May 30 2018 at 07:32):

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 (May 30 2018 at 07:34):

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 (May 30 2018 at 07:36):

We really need to get back Simon

Patrick Massot (May 30 2018 at 07:36):

@Simon Hudon where are you?

Johan Commelin (May 30 2018 at 07:40):

Right. A clear denominator tactic makes sense as well.

Johan Commelin (May 30 2018 at 07:41):

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 (May 30 2018 at 11:31):

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 (May 30 2018 at 11:34):

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

Sean Leather (May 30 2018 at 11:43):

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 (May 30 2018 at 11:45):

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

Simon Hudon (May 30 2018 at 11:46):

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

Patrick Massot (May 30 2018 at 11:53):

We have trouble with thread discipline

Patrick Massot (May 30 2018 at 11:53):

But we try

Simon Hudon (May 30 2018 at 12:31):

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 (May 30 2018 at 12:46):

Many thread actually mix different topics

Mario Carneiro (May 30 2018 at 13:04):

I think Kevin should speak in complete sentences

Mario Carneiro (May 30 2018 at 13:05):

instead of fragments

Mario Carneiro (May 30 2018 at 13:05):

of sentences

Mario Carneiro (May 30 2018 at 13:05):

that create tons of messages and fill

Mario Carneiro (May 30 2018 at 13:05):

my screen

Simon Hudon (May 30 2018 at 13:12):

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 (May 30 2018 at 15:11):

Why did you provoked him?!

Simon Hudon (May 30 2018 at 16:19):

Provoke how?

Patrick Massot (May 30 2018 at 16:20):

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

Patrick Massot (May 30 2018 at 16:20):

That's all your fault :stuck_out_tongue_winking_eye:

Simon Hudon (May 30 2018 at 16:21):

Haha! I'm secretly a terrorist!

Simon Hudon (May 30 2018 at 16:21):

Sorry typo: theorist

Simon Hudon (May 30 2018 at 16:22):

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

Kevin Buzzard (May 30 2018 at 17:08):

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 (May 30 2018 at 17:08):

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

Kevin Buzzard (May 30 2018 at 17:08):

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

Kevin Buzzard (May 30 2018 at 17:08):

"let's see what this entails"

Kevin Buzzard (May 30 2018 at 17:08):

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

Kevin Buzzard (May 30 2018 at 17:09):

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

Kevin Buzzard (May 30 2018 at 17:09):

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

Kevin Buzzard (May 30 2018 at 17:09):

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

Kevin Buzzard (May 30 2018 at 17:10):

and this can surely be done with tactics

Simon Hudon (May 30 2018 at 18:06):

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 (May 30 2018 at 18:38):

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 (May 30 2018 at 18:40):

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

Sebastien Gouezel (May 30 2018 at 18:51):

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 (May 30 2018 at 18:59):

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

Johan Commelin (May 30 2018 at 19:03):

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

Johannes Hölzl (May 30 2018 at 19:14):

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.


Last updated: Dec 20 2023 at 11:08 UTC