## 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: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

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];
... ≤ 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

@Patrick Massot

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

and I just burnt a lot of my time

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 (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...

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

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

of sentences

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

that create tons of messages and fill

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?!

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?

#### 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: May 09 2021 at 10:11 UTC