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 Lean.Meta.LibrarySearch.grindDischarger (mvarId : MVarId) : MetaM (Option (List MVarId))

A discharger that tries grind on the goal. The proof is wrapped in Grind.Marker so that suggestions display (by grind) instead of the complex grind proof term. Returns some [] if grind succeeds, none otherwise (leaving the goal as a subgoal).

def Lean.Meta.LibrarySearch.tryDischarger (mvarId : MVarId) : MetaM (Option (List MVarId))

A discharger that tries try? on the goal. The proof is wrapped in Try.Marker so that suggestions display (by try?) instead of the complex proof term. Returns some [] if try? succeeds, none otherwise (leaving the goal as a subgoal).

def Lean.Meta.LibrarySearch.solveByElim (required : List Expr) (exfalso : Bool) (goals : List MVarId) (maxDepth : Nat) (grind try? : Bool := false) : MetaM (List MVarId)

Wrapper for calling `Lean.Meta.SolveByElim.solveByElim with appropriate arguments for library search.

If grind is true, grind will be used as a fallback discharger for subgoals that cannot be closed by other means. If try? is true, try? will be used as a fallback discharger (via grind internally).

inductive Lean.Meta.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 : DeclMod

  the original declaration

• mp : DeclMod

  the forward direction of an iff

• mpr : DeclMod

  the backward direction of an iff

instance Lean.Meta.LibrarySearch.instDecidableEqDeclMod : DecidableEq DeclMod

instance Lean.Meta.LibrarySearch.instInhabitedDeclMod : Inhabited DeclMod

def Lean.Meta.LibrarySearch.instInhabitedDeclMod.default : DeclMod

def Lean.Meta.LibrarySearch.instOrdDeclMod.ord : DeclMod → DeclMod → Ordering

instance Lean.Meta.LibrarySearch.instOrdDeclMod : Ord DeclMod

instance Lean.Meta.LibrarySearch.instHashableDeclMod : Hashable DeclMod

def Lean.Meta.LibrarySearch.instHashableDeclMod.hash : DeclMod → UInt64

@[reducible]

def Lean.Meta.LibrarySearch.CandidateFinder : Type

LibrarySearch has an extension mechanism for replacing the function used to find candidate lemmas.

def Lean.Meta.LibrarySearch.droppedKeys : List (List LazyDiscrTree.Key)

We drop .star and Eq * * * from the discriminator trees because they match too much.

def Lean.Meta.LibrarySearch.libSearchFindDecls (ty : Expr) : MetaM (Array (Name × DeclMod))

Create function for finding relevant declarations. Also captures dropped entries in starLemmasExt for fallback search.

def Lean.Meta.LibrarySearch.getStarLemmas : MetaM (Array (Name × DeclMod))

Get star-indexed lemmas (lazily computed during tree initialization).

def Lean.Meta.LibrarySearch.mkHeartbeatCheck (leavePercent : Nat) : MetaM (MetaM Bool)

Return an action that returns true when the remaining heartbeats is less than the currently remaining heartbeats * leavePercent / 100.

def Lean.Meta.LibrarySearch.interleaveWith {α : Type u_1} {β : Type u_2} {γ : Type} (f : α → γ) (x : Array α) (g : β → γ) (y : Array β) : Array γ

Interleave x y interleaves the elements of x and y until one is empty and then returns final elements in other list.

def Lean.Meta.LibrarySearch.abortSpeculation {m : Type u_1 → Type u_2} {α : Type u_1} [MonadExcept Exception m] : m α

Called to abort speculative execution in library search.

def Lean.Meta.LibrarySearch.isAbortSpeculation : Exception → Bool

Returns true if this is an abort speculation exception.

@[reducible]

def Lean.Meta.LibrarySearch.Candidate : Type

A library search candidate using symmetry includes the goal to solve, the metavar context for that goal, and the name and orientation of a rule to try using with goal.

def Lean.Meta.LibrarySearch.librarySearchSymm (searchFn : CandidateFinder) (goal : MVarId) : MetaM (Array Candidate)

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

def Lean.Meta.LibrarySearch.mkLibrarySearchLemma (lem : Name) (mod : DeclMod) : MetaM Expr

Create lemma from name and mod.

def Lean.Meta.LibrarySearch.tryOnEach (act : Candidate → MetaM (List MVarId)) (candidates : Array Candidate) (collectAll : Bool := false) : MetaM (Option (Array (List MVarId × MetavarContext)))

Sequentially invokes a tactic act on each value in candidates on the current state.

The tactic act should return a list of meta-variables that still need to be resolved. If this list is empty, then no variables remain to be solved, and tryOnEach returns none with the environment set so each goal is resolved (unless collectAll is true, in which case it continues searching and collects complete solutions in the array).

If the action throws an internal exception with the abortSpeculationId id then further computation is stopped and intermediate results returned. If any other exception is thrown, then it is silently discarded.

def Lean.Meta.LibrarySearch.librarySearch (goal : MVarId) (tactic : List MVarId → MetaM (List MVarId) := fun (g : List MVarId) => solveByElim [] false g 6) (allowFailure : MVarId → MetaM Bool := fun (x : MVarId) => pure true) (leavePercentHeartbeats : Nat := 10) (includeStar : Bool := true) (collectAll : Bool := false) : MetaM (Option (Array (List MVarId × MetavarContext)))

Tries to solve the goal by applying a library lemma then calling tactic on the resulting goals.

Typically here tactic is solveByElim.

If it successfully closes the goal, returns none (unless collectAll is true). Otherwise, it returns some a, where a : Array (List MVarId × MetavarContext), with an entry for each library lemma which was successfully applied, containing a list of the subsidiary goals, and the metavariable context after the application. When collectAll is true, complete solutions (with empty remaining goals) are also included in the array instead of returning early.

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