Library search

This file defines a tactic library_search and a term elaborator library_search% that tries to find a lemma solving the current goal (subgoals are solved using solveByElim).

example : x < x + 1 := library_search%
example : Nat := by library_search

ink

def Lean.Meta.DiscrTree.insertIfSpecific {α : Type} {s : Bool} [inst : BEq α] (d : Lean.Meta.DiscrTree α s) (keys : Array (Lean.Meta.DiscrTree.Key s)) (v : α) : Lean.Meta.DiscrTree α s

Inserts a new key into a discrimination tree, but only if it is not of the form #[*] or #[=, *, *, *].

Equations

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

ink

inductive Mathlib.Tactic.LibrarySearch.DeclMod : Type

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

A "modifier" for a declaration.

• none indicates the original declaration,
• symm indicates that (possibly after binders) the declaration is an =, and we want to consider the symmetric version,
• mp indicates that (possibly after binders) the declaration is an iff, and we want to consider the forward direction,
• mpr similarly, but for the backward direction.

ink

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

Equations

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

ink

opaque Mathlib.Tactic.LibrarySearch.librarySearchLemmas : Mathlib.Tactic.DeclCache (Lean.Meta.DiscrTree (Lean.Name × Mathlib.Tactic.LibrarySearch.DeclMod) true)

ink

def Mathlib.Tactic.LibrarySearch.solveByElim (goals : List Lean.MVarId) (required : List Lean.Expr) (depth : ℕ) : Lean.MetaM PUnit

Shortcut for calling solveByElim.

Equations

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

ink

def Mathlib.Tactic.LibrarySearch.librarySearch {s : Bool} (goal : Lean.MVarId) (lemmas : Lean.Meta.DiscrTree (Lean.Name × Mathlib.Tactic.LibrarySearch.DeclMod) s) (required : List Lean.Expr) (solveByElimDepth : optParam ℕ 6) : Lean.MetaM (Option (Array (Lean.MetavarContext × List Lean.MVarId)))

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

ink

def Mathlib.Tactic.LibrarySearch.lines (ls : List Lean.MessageData) : Lean.MessageData

Equations

• Mathlib.Tactic.LibrarySearch.lines ls = Lean.MessageData.joinSep ls (Lean.MessageData.ofFormat Lean.Format.line)

ink

def Mathlib.Tactic.LibrarySearch.librarySearch' : Lean.ParserDescr

Equations

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

ink

def Mathlib.Tactic.LibrarySearch.librarySearch! : Lean.ParserDescr

Equations

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

ink

def Mathlib.Tactic.LibrarySearch.«termLibrary_search%» : Lean.ParserDescr

Equations

• Mathlib.Tactic.LibrarySearch.«termLibrary_search%» = Lean.ParserDescr.node `Mathlib.Tactic.LibrarySearch.termLibrary_search% 1024 (Lean.ParserDescr.symbol "library_search%")