Library search #
This file defines tactics
(formerly known as
and a term elaborator
that tries to find a lemma
solving the current goal
(subgoals are solved using
- none: Mathlib.Tactic.LibrarySearch.DeclMod
- mp: Mathlib.Tactic.LibrarySearch.DeclMod
- mpr: Mathlib.Tactic.LibrarySearch.DeclMod
A "modifier" for a declaration.
noneindicates the original declaration,
mpindicates that (possibly after binders) the declaration is an
↔, and we want to consider the forward direction,
mprsimilarly, but for the backward direction.
Insert a lemma into the discrimination tree.
Try applying the given lemma (with symmetry modifier) to the goal,
then try to close subsequent goals using
solveByElim succeeds, we return
 as the list of new subgoals,
otherwise the full list of subgoals.
Returns a tuple:
- are there no remaining goals?
- how many local hypotheses were used?
- how many goals remain, negated?
Larger values (i.e. no remaining goals, more local hypotheses, fewer remaining goals) are better.
Sort the incomplete results from
librarySearchCore according to
- the number of local hypotheses used (the more the better) and
- the number of remaining subgoals (the fewer the better).
Try to solve the goal either by:
If it successfully closes the goal, returns
Otherwise, it returns
some a, where
a : Array (MetavarContext × List MVarId),
with an entry for each library lemma which was successfully applied,
containing the metavariable context after the application, and a list of the subsidiary goals.
(Always succeeds, and the metavariable context stored in the monad is reverted, unless the goal was completely solved.)
(Note that if
solveByElim solves some but not all subsidiary goals,
this is not currently tracked.)