Stream: new members

Topic: when library_search fails you

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?

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.

Thanks :)

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.

Alex J. Best (Jul 22 2020 at 04:44):

@Chris M Have you seen suggest?

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 :)

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)

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