better reporting from library_search

Stream: new members

[Mario Carneiro]

Actually I think we should avoid the "failed" error message entirely. It's really a placeholder for actual error reporting

[Mario Carneiro]

In the case of library_search, it would be good if the failure message gave a lot more information, like a tutorial. Keep in mind that newbies are a major part of the user base for library_search

[Jalex Stark]

does the information you want to display depend on what the failed goal was?

[Mario Carneiro]

a basic troubleshooting guide would be good

library_search failed. If you aren't sure what to do next, you can also try library_search!, suggest, or hint. Possible reasons why library_search failed:

• The goal should be provable by direct application of a lemma from the library. If you haven't already, try stating the theorem you want in its own lemma.

• Sometimes the library has one version of a lemma but not a very similar version obtained by permuting arguments. Try replacing a + b with b + a, or a - b < c with a < b + c, to see if maybe the lemma exists but isn't stated quite the way you would like.

• Make sure that you have all the side conditions for your theorem to be true. For example you won't find a - b + b = a in the library because it's false! Search for b <= a -> a - b + b = a instead.

• If a definition you made is in the lemma, you won't find any theorems about it in the library. Try unfolding the definition using unfold my_definition

• If all else fails, ask on https://leanprover.zulipchat.com/, and maybe we can improve the library and/or library_search for next time.

[Scott Morrison]

This sounds great. I'm not sure what "The goal should be provable by direct application of a lemma from the library." means though. Is this intended to remind the reader what the scope of library_search is?

[Mario Carneiro]

Yes, does "one-step proof" make more sense?

[Mario Carneiro]

That is, it's not a general decision procedure, it's not simp

[Mario Carneiro]

it should be thought of as a search function for the library (which hopefully the name already makes clear)

[Mario Carneiro]

but I can imagine someone confusing it for sledgehammer and needs to be told otherwise