Zulip Chat Archive

Stream: new members

Topic: when `library_search` fails you


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

I've been having a recurring situation where I want to prove something relatively obvious, but I don't know the name of the lemma that mathlib gives to it. I generally use library_search, but there isn't always a single lemma that can prove something. I end up adding lots of haves for the assumptions of a lemma that I THINK is the way to prove this.
In the following example, I'm trying to prove abs x * abs y ≤ abs x * ε

import data.real.basic
import tactic

lemma my_lemma2 :  {x y ε : },
  0 < ε  ε  1  abs x < ε  abs y < ε  abs (x * y) < ε :=
begin
  intros x y ε epos ele1 xlt ylt,
  have hx:0  abs x, {exact abs_nonneg x},
  have hy:0  abs y, {exact abs_nonneg y},
  calc
    abs (x * y) = abs x * abs y : abs_mul x y
    ...  abs x * ε             : by library_search
    ... < 1 * ε                 : sorry
    ... = ε                     : one_mul ε
end

To show that abs x * abs y ≤ abs x * ε I tried using library_search but apparently there isn't a single lemma for this. I reasoned that the way to show this is by saying that 0≤a \to a * b ≤ a * c \iff b≤c, which didn't work. However then after reading in the tutorial, they suggested I use mul_le_mul : ?M_3 ≤ ?M_5 → ?M_4 ≤ ?M_6 → 0 ≤ ?M_4 → 0 ≤ ?M_5 → ?M_3 * ?M_4 ≤ ?M_5 * ?M_6. I would not have discovered this without the tutorial telling me.

What general strategy should I adopt to find which lemma's to use in situations like this?

view this post on Zulip Shing Tak Lam (Jul 21 2020 at 05:07):

For finding lemmas, the inequality you need to prove is _ * _ ≤ _ * _, so if you write down the symbols, it's [mul, le, mul]. So searching for mul_le_mul should find that lemma. To search, you can use VSCode search (make sure it can search in mathlib!), grep or Ctrl-P, then #mul_le_mul

Although I think for inequalities like this, just using linarith and nlinarith is probably faster than trying to find the exact lemma which solves it. In this case, you can replace by library_search with by nlinarith.

view this post on Zulip Chris M (Jul 22 2020 at 03:50):

Thanks :)

view this post on Zulip Chris M (Jul 22 2020 at 03:52):

Would it make sense for there to be a tactic that, like library_search, searches the library, but instead merely looks for lemmas that pattern-match with your conclusion, and just lists all of those lemmas and their type signatures, even if it can't find an immediate way to use it.

view this post on Zulip Alex J. Best (Jul 22 2020 at 04:44):

@Chris M Have you seen suggest?

view this post on Zulip Chris M (Jul 22 2020 at 04:46):

No I haven't! Looking at the the docs, it sounds great, I'll look at it. thanks :)

view this post on Zulip Jalex Stark (Jul 22 2020 at 12:04):

(I recommend doing a speed-read of the tactic docs page as a way to get a feel for what exists)

view this post on Zulip Bryan Gin-ge Chen (Jul 22 2020 at 12:10):

Shing Tak Lam said:

To search, you can use VSCode search (make sure it can search in mathlib!), [...] Ctrl-P, then #mul_le_mul

You can also hit Ctrl-T, mul_le_mul.

We usually recommend library_search and suggest now, but #find works (slowly) on patterns like _ * _ ≤ _ * _:

import tactic

#find _ * _  _ * _

Last updated: May 16 2021 at 05:21 UTC