when `library_search` fails you

Stream: new members

[Chris M]

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?

[Shing Tak Lam]

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.

[Chris M]

Thanks :)

[Chris M]

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.

[Alex J. Best]

@Chris M Have you seen suggest?

[Chris M]

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

[Jalex Stark]

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

[Bryan Gin-ge Chen]

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 _ * _ ≤ _ * _