Library search #
This file defines tactics exact?
and apply?
,
(formerly known as library_search
)
and a term elaborator exact?%
that tries to find a lemma
solving the current goal
(subgoals are solved using solveByElim
).
example : x < x + 1 := exact?%
example : Nat := by exact?
- none: Mathlib.Tactic.LibrarySearch.DeclMod
- mp: Mathlib.Tactic.LibrarySearch.DeclMod
- mpr: Mathlib.Tactic.LibrarySearch.DeclMod
A "modifier" for a declaration.
none
indicates the original declaration,mp
indicates that (possibly after binders) the declaration is an↔
, and we want to consider the forward direction,mpr
similarly, but for the backward direction.
Instances For
Prepare the discrimination tree entries for a lemma.
Instances For
Insert a lemma into the discrimination tree.
Instances For
Construct the discrimination tree of all lemmas.
Instances For
Retrieve the current current of lemmas.
Instances For
Shortcut for calling solveByElim
.
Instances For
Try applying the given lemma (with symmetry modifier) to the goal,
then try to close subsequent goals using solveByElim
.
If solveByElim
succeeds, we return []
as the list of new subgoals,
otherwise the full list of subgoals.
Instances For
Returns a lazy list of the results of applying a library lemma,
then calling solveByElim
on the resulting goals.
Instances For
Run librarySearchCore
on both the goal and symm
applied to the goal.
Instances For
A type synonym for our subgoal ranking algorithm.
Instances For
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.
Instances For
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).
Instances For
Try to solve the goal either by:
- calling
solveByElim
- or applying a library lemma then calling
solveByElim
on the resulting goals.
If it successfully closes the goal, returns none
.
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.)