How to list all applicable theorems?

Stream: general

[Daniel Donnelly]

Given a list of types, how can I list all applicable rules (definitions, lemmas, theorems, etc) such that you can apply the rule to the list of arguments and get a proof of something?

[Scott Morrison]

I'm not sure the question is well defined. Every single declaration is, after all, a proof of something.

[Scott Morrison]

Do you want to use everything in the list of arguments?

[Scott Morrison]

Or perhaps prove something that is not a Pi-type?

[Daniel Donnelly]

I am thinking about ATP and was wondering what API's Lean offers for automated reasoning

[Daniel Donnelly]

Sort of like "combinatorial chemistry"

[Scott Morrison]

So you'll have to say what you want to do. :-)

[Scott Morrison]

Reading the implementations of library_search and solve_by_elim might give you a sense of how to do this sort of thing. (Not sure what your background is.)

[Daniel Donnelly]

@Scott Morrison thx that helps. I will read those

[Daniel Donnelly]

@Scott Morrison can you give a short and sweet example of using library_search and / or suggest?

[Daniel Donnelly]

For instance given n : N, m : N what are all applicable definitions for example

[Scott Morrison]

That's not at all what library_search does.

[Scott Morrison]

See https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Extensionality.20for.20big.20operators for a recent example of someone finding library_search useful.

[Scott Morrison]

As I said above, your question as posed doesn't make much sense.

[Scott Morrison]

You need to explain what you mean by "applicable".

[Daniel Donnelly]

example (n m k : ℕ) : n * (m - k) = n * m - n * k :=
by library_search -- Try this: exact nat.mul_sub_left_distrib n m k

[Daniel Donnelly]

found some examples on library page, in other words

[Daniel Donnelly]

@Scott Morrison how do I include library_search into the lean file I am editing?

[Scott Morrison]

import tactic.suggest

[Scott Morrison]

or just import tactic which imports the kitchen sink.