mathlib3 documentation

tactic.suggest

suggest and library_search #

suggest and library_search are a pair of tactics for applying lemmas from the library to the current goal.

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.

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
Instances for tactic.suggest.head_symbol_match

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

meta structure tactic.suggest.decl_data  :

A package of declaration metadata, including the way in which its type matches the head symbol which we are searching for.

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.)

meta structure tactic.suggest.suggest_opt  :

An extension to the option structure for solve_by_elim.

  • compulsory_hyps specifies a list of local hypotheses which must appear in any solution. These are useful for constraining the results from library_search and suggest.
  • try_this is a flag (default: tt) that controls whether a "Try this:"-line should be traced.

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.

meta structure tactic.suggest.application  :

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 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.

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.

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.

suggest lists possible usages of the refine tactic and 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.

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

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.

An example of suggest in action,

example (n : nat) : n < n + 1 :=
begin suggest, sorry end

prints the list,

Try this: exact nat.lt.base n
Try this: exact nat.lt_succ_self n
Try this: refine not_le.mp _
Try this: refine gt_iff_lt.mp _
Try this: refine nat.lt.step _
Try this: refine lt_of_not_ge _
...

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