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?

def Mathlib.Tactic.LibrarySearch.discrTreeConfig : Lean.Meta.WhnfCoreConfig

Configuration for DiscrTree.

Equations

• Mathlib.Tactic.LibrarySearch.discrTreeConfig = { iota := true, beta := true, proj := Lean.Meta.ProjReductionKind.yesWithDelta, zeta := true }

inductive Mathlib.Tactic.LibrarySearch.DeclMod : Type

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.

• none: Mathlib.Tactic.LibrarySearch.DeclMod
• mp: Mathlib.Tactic.LibrarySearch.DeclMod
• mpr: Mathlib.Tactic.LibrarySearch.DeclMod

instance Mathlib.Tactic.LibrarySearch.instDecidableEqDeclMod : DecidableEq Mathlib.Tactic.LibrarySearch.DeclMod

Equations

• One or more equations did not get rendered due to their size.

instance Mathlib.Tactic.LibrarySearch.instOrdDeclMod : Ord Mathlib.Tactic.LibrarySearch.DeclMod

Equations

• Mathlib.Tactic.LibrarySearch.instOrdDeclMod = { compare := Mathlib.Tactic.LibrarySearch.ordDeclMod✝ }

instance Mathlib.Tactic.LibrarySearch.instToStringDeclMod : ToString Mathlib.Tactic.LibrarySearch.DeclMod

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.Tactic.LibrarySearch.processLemma (name : Lean.Name) (constInfo : Lean.ConstantInfo) : Lean.MetaM (Array (Array Lean.Meta.DiscrTree.Key × Lean.Name × Mathlib.Tactic.LibrarySearch.DeclMod))

Prepare the discrimination tree entries for a lemma.

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.Tactic.LibrarySearch.buildDiscrTree : IO (Std.Tactic.DiscrTreeCache (Lean.Name × Mathlib.Tactic.LibrarySearch.DeclMod))

Construct the discrimination tree of all lemmas.

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.Tactic.LibrarySearch.cachePath : IO System.FilePath

Equations

• One or more equations did not get rendered due to their size.

opaque Mathlib.Tactic.LibrarySearch.librarySearchLemmas : Std.Tactic.DiscrTreeCache (Lean.Name × Mathlib.Tactic.LibrarySearch.DeclMod)

Retrieve the current current of lemmas.

def Mathlib.Tactic.LibrarySearch.solveByElim (goals : List Lean.MVarId) (required : List Lean.Expr) (exfalso : optParam Bool false) (depth : Nat) : Lean.MetaM (List Lean.MVarId)

Shortcut for calling solveByElim.

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.Tactic.LibrarySearch.librarySearchLemma (lem : Lean.Name) (mod : Mathlib.Tactic.LibrarySearch.DeclMod) (required : List Lean.Expr) (solveByElimDepth : optParam Nat 6) (goal : Lean.MVarId) : Lean.MetaM (List Lean.MVarId)

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.

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.Tactic.LibrarySearch.librarySearchCore (goal : Lean.MVarId) (required : List Lean.Expr) (solveByElimDepth : optParam Nat 6) : Nondet Lean.MetaM (List Lean.MVarId)

Returns a lazy list of the results of applying a library lemma, then calling solveByElim on the resulting goals.

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.Tactic.LibrarySearch.librarySearchSymm (goal : Lean.MVarId) (required : List Lean.Expr) (solveByElimDepth : optParam Nat 6) : Nondet Lean.MetaM (List Lean.MVarId)

Run librarySearchCore on both the goal and symm applied to the goal.

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.Tactic.LibrarySearch.subgoalRankType : Type

A type synonym for our subgoal ranking algorithm.

Equations

• Mathlib.Tactic.LibrarySearch.subgoalRankType = (Bool × Nat × Int)

instance Mathlib.Tactic.LibrarySearch.instOrdSubgoalRankType : Ord Mathlib.Tactic.LibrarySearch.subgoalRankType

Equations

• Mathlib.Tactic.LibrarySearch.instOrdSubgoalRankType = let_fun this := lexOrd; lexOrd

def Mathlib.Tactic.LibrarySearch.subgoalRanking (goal : Lean.MVarId) (subgoals : List Lean.MVarId) : Lean.MetaM Mathlib.Tactic.LibrarySearch.subgoalRankType

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.

Equations

• Mathlib.Tactic.LibrarySearch.subgoalRanking goal subgoals = do let __do_lift ← Lean.Meta.countLocalHypsUsed (Lean.Expr.mvar goal) pure (List.isEmpty subgoals, __do_lift, -↑(List.length subgoals))

def Mathlib.Tactic.LibrarySearch.sortResults (goal : Lean.MVarId) (R : Array (List Lean.MVarId × Lean.MetavarContext)) : Lean.MetaM (Array (List Lean.MVarId × Lean.MetavarContext))

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

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.Tactic.LibrarySearch.librarySearch (goal : Lean.MVarId) (required : List Lean.Expr) (solveByElimDepth : optParam Nat 6) (leavePercentHeartbeats : optParam Nat 10) : Lean.MetaM (Option (Array (List Lean.MVarId × Lean.MetavarContext)))

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

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.Tactic.LibrarySearch.exact?' : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.Tactic.LibrarySearch.exact?! : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.Tactic.LibrarySearch.exact!? : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.Tactic.LibrarySearch.apply?' : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.Tactic.LibrarySearch.exact? (tk : Lean.Syntax) (required : Option (Array (Lean.TSyntax `term))) (requireClose : Bool) : Lean.Elab.Tactic.TacticM Unit

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.Tactic.LibrarySearch.tacticLibrary_search : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.Tactic.LibrarySearch.«termExact?%» : Lean.ParserDescr

Equations

• Mathlib.Tactic.LibrarySearch.«termExact?%» = Lean.ParserDescr.node `Mathlib.Tactic.LibrarySearch.termExact?% 1024 (Lean.ParserDescr.symbol "exact?%")