compute the head symbol of an expression, but normalise > to < and ≥ to ≤

A declaration can match the head symbol of the current goal in four possible ways:

• ex : an exact match
• mp : the declaration returns an iff, and the right hand side matches the goal
• mpr : the declaration returns an iff, and the left hand side matches the goal
• both: the declaration returns an iff, and the both sides match the goal

a textual representation of a head_symbol_match, for trace debugging.

When we are determining if a given declaration is potentially relevant for the current goal, we compute unfold_head_symbol on the head symbol of the declaration, producing a list of names. We consider the declaration potentially relevant if the head symbol of the goal appears in this list.

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.

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

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

Replace any metavariables in the expression with underscores, in preparation for printing refine ... statements.

Construct a refine ... or exact ... string which would construct g.

Assuming that a goal g has been (partially) solved in the tactic_state l, this function prepares a string of the form exact ... or refine ... (possibly with underscores) that will reproduce that result.

An application records the result of a successful application of a library lemma.

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 refine ... or 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 exact ... or refine ..., which make progress on the current goal using a declaration from the library.

Returns a string of the form 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.

library_search attempts to apply every definition in the library whose head symbol matches the goal, and then discharge any new goals using solve_by_elim.

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