# 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 `ring`

tactic 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