should `library_search` work here?

Stream: new members

[Chris M]

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]

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

[Scott Morrison]

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

[Scott Morrison]

What are a and b here? (#mwe)

[Scott Morrison]

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]

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]

That's probably div_nonneg

[Johan Commelin]

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]

Maybe suggest would help...

[Chris M]

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

[Johan Commelin]

Yup, it does.

[Chris M]

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]

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

[Chris M]

No doesn't work either

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Chris M]

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

[Chris M]

div_nonneg gives me a type error

[Chris M]

How do I typecast them as \R?

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

Chris M said:

div_nonneg gives me a type error

What kind of error?

[Chris M]

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

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

[Chris M]

same for 0 : \R

[Johan Commelin]

(0 < \R) < 2

[Johan Commelin]

I think you have the parens slightly differently

[Chris M]

oh got it

[Johan Commelin]

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]

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]

It doesn't work without h5

[Johan Commelin]

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]

It cannot proof any of the hypotheses for the lemma

[Chris M]

Ok makes sense. Thanks for the help!

[Johan Commelin]

@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]

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]

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