Map a name (typically a head symbol) to a "canonical" definitional synonym. Given a name n, we want a name n' such that a sufficiently applied expression with head symbol n is always definitionally equal to an expression with head symbol n'. Thus, we can search through all lemmas with a result type of n' to solve a goal with head symbol n.

For example, > is mapped to < because a > b is definitionally equal to b < a, and not is mapped to false because ¬ a is definitionally equal to p → false The default is that the original argument is returned, so < is just mapped to <.

normalize_synonym is called for every lemma in the library, so it needs to be fast.

Compute the head symbol of an expression, then normalise synonyms.

This is only used when analysing the goal, so it is okay to do more expensive analysis here.

Determine if, and in which way, a given expression matches the specified head symbol.

Generate a decl_data from the given declaration if it matches the head symbol hs for the current goal.

Retrieve all library definitions with a given head symbol.

We unpack any element of a list of decl_data corresponding to an ↔ statement that could apply in both directions into two separate elements.

This ensures that both directions can be independently returned by suggest, and avoids a problem where the application of one direction prevents the application of the other direction. (See exp_le_exp in the tests.)

Convert a suggest_opt structure to a opt structure suitable for solve_by_elim, by setting the accept parameter to require that all complete solutions use everything in compulsory_hyps.

Apply the lemma e, then attempt to close all goals using solve_by_elim opt, failing if close_goals = tt and there are any goals remaining.

Returns the number of subgoals which were closed using solve_by_elim.

Apply the declaration d (or the forward and backward implications separately, if it is an iff), and then attempt to solve the subgoal using apply_and_solve.

Returns the number of subgoals successfully closed.

The core suggest tactic. It attempts to apply a declaration from the library, then solve new goals using solve_by_elim.

It returns a list of applications consisting of fields:

• state, a tactic state resulting from the successful application of a declaration from the library,
• script, a string of the form Try this: refine ... or Try this: exact ... which will reproduce that tactic state,
• decl, an option declaration indicating the declaration that was applied (or none, if solve_by_elim succeeded),
• num_goals, the number of remaining goals, and
• hyps_used, the number of local hypotheses used in the solution.

See suggest_core.

Returns a list of at most limit applications, sorted by number of goals, and then (reverse) number of hypotheses used.

Returns a list of at most limit strings, of the form Try this: exact ... or Try this: refine ..., which make progress on the current goal using a declaration from the library.

Returns a string of the form Try this: exact ..., which closes the current goal.

suggest tries to apply suitable theorems/defs from the library, and generates a list of exact ... or refine ... scripts that could be used at this step. It leaves the tactic state unchanged. It is intended as a complement of the search function in your editor, the #find tactic, and library_search.

suggest takes an optional natural number num as input and returns the first num (or less, if all possibilities are exhausted) possibilities ordered by length of lemma names. The default for num is 50. For performance reasons suggest uses monadic lazy lists (mllist). This means that suggest might miss some results if num is not large enough. However, because suggest uses monadic lazy lists, smaller values of num run faster than larger values.

You can add additional lemmas to be used along with local hypotheses after the application of a library lemma, using the same syntax as for solve_by_elim, e.g.

example {a b c d: nat} (h₁ : a < c) (h₂ : b < d) : max (c + d) (a + b) = (c + d) :=
begin
  suggest [add_lt_add], -- Says: `Try this: exact max_eq_left_of_lt (add_lt_add h₁ h₂)`
end

You can also use suggest with attr to include all lemmas with the attribute attr.

library_search is a tactic to identify existing lemmas in the library. It tries to close the current goal by applying a lemma from the library, then discharging any new goals using solve_by_elim.

If it succeeds, it prints a trace message exact ... which can replace the invocation of library_search.

Typical usage is:

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

library_search using h₁ h₂ will only show solutions that make use of the local hypotheses h₁ and h₂.

By default library_search only unfolds reducible definitions when attempting to match lemmas against the goal. Previously, it would unfold most definitions, sometimes giving surprising answers, or slow answers. The old behaviour is still available via library_search!.

You can add additional lemmas to be used along with local hypotheses after the application of a library lemma, using the same syntax as for solve_by_elim, e.g.

example {a b c d: nat} (h₁ : a < c) (h₂ : b < d) : max (c + d) (a + b) = (c + d) :=
begin
  library_search [add_lt_add], -- Says: `Try this: exact max_eq_left_of_lt (add_lt_add h₁ h₂)`
end

You can also use library_search with attr to include all lemmas with the attribute attr.

Invoking the hole command library_search ("Use library_search to complete the goal") calls the tactic library_search to produce a proof term with the type of the hole.

Running it on

example : 0 < 1 :=
{!!}

produces

example : 0 < 1 :=
nat.one_pos