Zulip Chat Archive

Stream: new members

Topic: should `library_search` work here?


view this post on Zulip 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)

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Scott Morrison (Jul 04 2020 at 05:04):

What are a and b here? (#mwe)

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Jul 04 2020 at 05:17):

That's probably div_nonneg

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Jul 04 2020 at 05:18):

Maybe suggest would help...

view this post on Zulip 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?

view this post on Zulip Johan Commelin (Jul 04 2020 at 05:20):

Yup, it does.

view this post on Zulip 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

view this post on Zulip Johan Commelin (Jul 04 2020 at 05:21):

And if you replace h5 with ? (Proof norm_num)

view this post on Zulip Chris M (Jul 04 2020 at 05:21):

No doesn't work either

view this post on Zulip 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 .

view this post on Zulip Johan Commelin (Jul 04 2020 at 05:22):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Chris M (Jul 04 2020 at 05:27):

div_nonneg gives me a type error

view this post on Zulip Chris M (Jul 04 2020 at 05:27):

How do I typecast them as \R?

view this post on Zulip Johan Commelin (Jul 04 2020 at 05:27):

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

view this post on Zulip Johan Commelin (Jul 04 2020 at 05:27):

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

view this post on Zulip Johan Commelin (Jul 04 2020 at 05:28):

Chris M said:

div_nonneg gives me a type error

What kind of error?

view this post on Zulip 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
 has_add Type
state:
a b : ,
h3 : 0  (a + b) ^ 2
 abs (a * b)  (a ^ 2 + b ^ 2) / 2

view this post on Zulip Chris M (Jul 04 2020 at 05:29):

same for 0 : \R

view this post on Zulip Johan Commelin (Jul 04 2020 at 05:29):

(0 < \R) < 2

view this post on Zulip Johan Commelin (Jul 04 2020 at 05:29):

I think you have the parens slightly differently

view this post on Zulip Chris M (Jul 04 2020 at 05:29):

oh got it

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Chris M (Jul 04 2020 at 05:31):

It doesn't work without h5

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Jul 04 2020 at 05:32):

It cannot proof any of the hypotheses for the lemma

view this post on Zulip Chris M (Jul 04 2020 at 05:33):

Ok makes sense. Thanks for the help!

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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