## Stream: general

### Topic: unfortunate failures of library_search

#### Scott Morrison (Oct 23 2019 at 04:54):

I'm going to use this thread as a not-quite-bug-tracker for unfortunate failures of library_search / suggest, so I remember them as test cases for potential future improvements.

#### Scott Morrison (Oct 23 2019 at 04:56):

example (a b : ℕ) (h : 0 < b) : (a * b) / b = a := by library_search


works, but

example (a b : ℕ) (h : b ≠ 0) : (a * b) / b = a := by library_search


doesn't. This is a common problem, in fact so common I'm considering just hardwiring something to library_search for exactly this case. (e.g. add zero_lt_iff_ne_zero.mpr into the set of lemmas for solve_by_elim.

(There are "more principled solutions", involving add _lots_ of extra lemmas to solve_by_elim, but this will take some engineering...)

#### Scott Morrison (Oct 30 2019 at 16:43):

Just copying a reported failure of library_search from Kevin:

import tactic.library_search

example (P Q : Prop) [decidable P] [decidable Q]: (¬ Q → ¬ P) → (P → Q) := by library_search -- fails
example (P Q : Prop) [decidable P] [decidable Q]: (¬ Q → ¬ P) ↔ (P → Q) := by library_search -- not_imp_not


I would have thought this one works, so I'll investigate later.

#### Lucas Allen (Nov 03 2019 at 03:14):

I think it'd be cool if library_search gave the proof exact h₃ ⟨h₁,h₂⟩ for

example (a b c : Prop) (h₁ : a) (h₂ : b) (h₃ : a ∧ b → c) : c := by library_search


at the moment library_search fails for this example.

#### Mario Carneiro (Nov 03 2019 at 03:54):

It's not a proof search, it is a library search

#### Mario Carneiro (Nov 03 2019 at 03:55):

it is supposed to help you find a lemma by type rather than by name

#### Mario Carneiro (Nov 03 2019 at 03:56):

Library searching is relatively expensive, particularly if you start throwing in more advanced operations at the same time. If it becomes a full blown proof search it will take forever; use tidy if you are looking for more proof-search like tasks

#### Lucas Allen (Nov 03 2019 at 03:57):

Another thing I think would be cool is if library_search gave the proof exact h₁.left for

example (a b : Prop) (h₁ : a ∧ b) : a := by library_search


I'm using library_search quite heavily at the moment, and I had to use my memory to figure out .left and .right for something just now. I think if library_search could solve some of these things it would decrease the learning curve for Lean somewhat. This would be because people would only ever need to remember library_search, instead of lots of little bits and pieces.

#### Mario Carneiro (Nov 03 2019 at 03:57):

I think tidy is a better fit for this approach

#### Mario Carneiro (Nov 03 2019 at 03:58):

although I agree in this case that it should find the lemma and.left

#### Lucas Allen (Nov 03 2019 at 03:59):

Oh yeah, tidy works. That's quite nice.

#### Mario Carneiro (Nov 03 2019 at 03:59):

I would guess that

example (a b : Prop) : a ∧ b -> a := by library_search


works?

No, not for me.

#### Lucas Allen (Nov 03 2019 at 04:02):

Would it be a good idea if tidy traced a proof that could be cut and pasted into a begin... end block, similar to how library_search traces an exact statement?

It does

#### Mario Carneiro (Nov 03 2019 at 04:04):

I think you have to call tidy? to get the trace output

#### Lucas Allen (Nov 03 2019 at 04:06):

That's great :big_smile:, can't believe I didn't know about tidy before. Thanks.

#### Scott Morrison (Apr 13 2020 at 01:15):

I've transcribed the examples from this thread to an new issue #2394 for complaining about solve_by_elim and library_search.

Last updated: May 08 2021 at 19:11 UTC