## Stream: new members

### Topic: should library_search work here?

#### Chris M (Jul 04 2020 at 05:02):

The following usage of library_search doesn't give me a hit.

import data.real.basic tactic

variables a b : ℝ

example : abs (a*b) ≤ (a^2 + b^2) / 2 :=
begin
have h3: (a+b)^2 ≥ 0, {exact pow_two_nonneg (a + b)},
have h4: (a+b)^2/2 ≥ 0, {library_search},
sorry
end


Shouldn't this give me a hit? (I know I can just use linarith btw)

#### Johan Commelin (Jul 04 2020 at 05:04):

@Chris M I'm not surprised that there isn't a lemma in the library that would close that in one go.

#### Scott Morrison (Jul 04 2020 at 05:04):

I don't have a computer nearby --- could you say what you were expecting it to find?

#### Scott Morrison (Jul 04 2020 at 05:04):

What are a and b here? (#mwe)

#### Scott Morrison (Jul 04 2020 at 05:05):

It does seem pretty plausible that library_search could prove h4 from h3, so we should track down what's going on here.

#### Chris M (Jul 04 2020 at 05:06):

I was expecting to find a lemma that says something like, dividing a positive number by a positive number gives a positive number.

#### Johan Commelin (Jul 04 2020 at 05:17):

That's probably div_nonneg

#### Johan Commelin (Jul 04 2020 at 05:18):

But it doesn't know that the two numbers that you are dividing are nonnegative... you'll need additional lemmas for that. And such reasoning is beyond what library_search can do.

#### Johan Commelin (Jul 04 2020 at 05:18):

Maybe suggest would help...

#### Chris M (Jul 04 2020 at 05:19):

doesn't h3 show that the numerator is nonnegative? I'd guess that lean already knows that 2 is nonnegative?

Yup, it does.

#### Chris M (Jul 04 2020 at 05:20):

Actually this also doesn't find a solution:

import data.real.basic tactic

variables a b : ℝ

example : abs (a*b) ≤ (a^2 + b^2) / 2 :=
begin
have h3: (a+b)^2 ≥ 0, {exact pow_two_nonneg (a + b)},
have h5: 2>0, {exact two_pos},
have h4: (a+b)^2/2 ≥ 0, {library_search},
sorry
end


#### Johan Commelin (Jul 04 2020 at 05:21):

And if you replace h5 with ≥? (Proof norm_num)

#### Chris M (Jul 04 2020 at 05:21):

No doesn't work either

#### Johan Commelin (Jul 04 2020 at 05:21):

Maybe you need to swap all the inequalities. Very disappointingly, lean is not so good at ≥ and prefers ≤.

#### Johan Commelin (Jul 04 2020 at 05:22):

Ok, if it still doesn't work, then we are missing some lemma.

#### Johan Commelin (Jul 04 2020 at 05:22):

Can you find div_nonneg manually, or are you missing an import? I would guess that importing the reals should be enough.

#### Chris M (Jul 04 2020 at 05:26):

I think have h5: (0 < 2) , {exact two_pos}, is interpreting 0 and 2 as natural numbers.

#### Chris M (Jul 04 2020 at 05:27):

div_nonneg gives me a type error

#### Chris M (Jul 04 2020 at 05:27):

How do I typecast them as \R?

#### Johan Commelin (Jul 04 2020 at 05:27):

Aah, good point, you need to write (0 : real)

#### Johan Commelin (Jul 04 2020 at 05:27):

(It will then understand that you mean the same for 2

#### Johan Commelin (Jul 04 2020 at 05:28):

Chris M said:

div_nonneg gives me a type error

What kind of error?

#### Chris M (Jul 04 2020 at 05:28):

have h5: (0 : real < 2) , {sorry}, gives me

failed to synthesize type class instance for
a b : ℝ,
h3 : 0 ≤ (a + b) ^ 2
state:
a b : ℝ,
h3 : 0 ≤ (a + b) ^ 2
⊢ abs (a * b) ≤ (a ^ 2 + b ^ 2) / 2


#### Chris M (Jul 04 2020 at 05:29):

same for 0 : \R

#### Johan Commelin (Jul 04 2020 at 05:29):

(0 < \R) < 2

#### Johan Commelin (Jul 04 2020 at 05:29):

I think you have the parens slightly differently

oh got it

#### Johan Commelin (Jul 04 2020 at 05:30):

This works

import data.real.basic tactic

variables a b : ℝ

example : abs (a*b) ≤ (a^2 + b^2) / 2 :=
begin
have h3: 0 ≤ (a+b)^2, {exact pow_two_nonneg (a + b)},
have h5: (0:ℝ) < 2, {exact two_pos},
have h4: (a+b)^2/2 ≥ 0, {library_search},
sorry
end


#### Chris M (Jul 04 2020 at 05:30):

Ok the whole thing works now.
Though maybe surprising that library_search isn't able to know by itself that 2 is a positive real number?

#### Chris M (Jul 04 2020 at 05:31):

It doesn't work without h5

#### Johan Commelin (Jul 04 2020 at 05:31):

Sure, it doesn't. library_search does exactly what it's name says. It searches through the library for a lemma that closes the goal directly.

#### Johan Commelin (Jul 04 2020 at 05:32):

It cannot proof any of the hypotheses for the lemma

#### Chris M (Jul 04 2020 at 05:33):

Ok makes sense. Thanks for the help!

#### Johan Commelin (Jul 04 2020 at 06:14):

@Chris M There is work on a tactic back that would try to do recursive backwards reasoning. But as you can imagine, it's delicate, because you quickly get a combinatorial explosion.

#### Sebastien Gouezel (Jul 04 2020 at 07:32):

What happens if you use $\le$ instead of $\ge$ in your statements? To avoid duplicating all lemmas, everything is normally stated in mathlib using $\le$.

#### Johan Commelin (Jul 04 2020 at 07:40):

The code that I posted above works... library_search finds div_nonneg as expected.

Last updated: May 12 2021 at 04:19 UTC