unfortunate failures of `library_search`

Stream: general

[Scott Morrison]

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]

Feel free to add your own suggestions!

[Scott Morrison]

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]

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]

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]

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

[Mario Carneiro]

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

[Mario Carneiro]

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]

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]

I think tidy is a better fit for this approach

[Mario Carneiro]

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

[Lucas Allen]

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

[Mario Carneiro]

I would guess that

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

works?

[Lucas Allen]

No, not for me.

[Lucas Allen]

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?

[Mario Carneiro]

It does

[Mario Carneiro]

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

[Lucas Allen]

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

[Scott Morrison]

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