Library search

This file defines tactics std_exact? and std_apply?, (formerly known as library_search) and a term elaborator std_exact?% that tries to find a lemma solving the current goal (subgoals are solved using solveByElim).

example : x < x + 1 := std_exact?%
example : Nat := by std_exact?

These functions will likely lose their std_ prefix once we are ready to replace the corresponding implementations in Mathlib.

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

Configuration for DiscrTree.

Equations

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

inductive Std.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: Std.Tactic.LibrarySearch.DeclMod

  the original declaration

• mp: Std.Tactic.LibrarySearch.DeclMod

  the forward direction of an iff

• mpr: Std.Tactic.LibrarySearch.DeclMod

  the backward direction of an iff

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

Equations

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

instance Std.Tactic.LibrarySearch.instInhabitedDeclMod : Inhabited Std.Tactic.LibrarySearch.DeclMod

Equations

• Std.Tactic.LibrarySearch.instInhabitedDeclMod = { default := Std.Tactic.LibrarySearch.DeclMod.none }

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

Equations

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

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

Equations

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

@[reducible]

def Std.Tactic.LibrarySearch.CandidateFinder : Type

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

Equations

• Std.Tactic.LibrarySearch.CandidateFinder = (Lean.Expr → Lean.MetaM (Array (Lean.Name × Std.Tactic.LibrarySearch.DeclMod)))

def Std.Tactic.LibrarySearch.DiscrTreeFinder.cachePath : IO System.FilePath

Once we reach Mathlib, and have cache available, we may still want to load a precomputed cache for exact? from a .olean file.

This makes no sense here in Std, where there is no caching mechanism.

Equations

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

def Std.Tactic.LibrarySearch.DiscrTreeFinder.buildImportCache (config : Lean.Meta.WhnfCoreConfig) : Lean.MetaM (Lean.Meta.DiscrTree (Lean.Name × Std.Tactic.LibrarySearch.DeclMod))

Constructs an discriminator tree from the current environment.

Equations

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

def Std.Tactic.LibrarySearch.DiscrTreeFinder.localMatches (config : Lean.Meta.WhnfCoreConfig) (ty : Lean.Expr) : Lean.MetaM (Array (Lean.Name × Std.Tactic.LibrarySearch.DeclMod))

Return matches from local constants.

N.B. The efficiency of this could likely be considerably improved by caching in environment extension.

Equations

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

def Std.Tactic.LibrarySearch.DiscrTreeFinder.mkImportFinder (config : Lean.Meta.WhnfCoreConfig) (importTree : Lean.Meta.DiscrTree (Lean.Name × Std.Tactic.LibrarySearch.DeclMod)) (ty : Lean.Expr) : Lean.MetaM (Array (Lean.Name × Std.Tactic.LibrarySearch.DeclMod))

Candidate finding function that uses strict discrimination tree for resolution.

Equations

• Std.Tactic.LibrarySearch.DiscrTreeFinder.mkImportFinder config importTree ty = do let __do_lift ← Lean.Meta.DiscrTree.getMatch importTree ty config pure (Array.reverse __do_lift)

def Std.Tactic.LibrarySearch.IncDiscrTreeFinder.mkImportFinder : IO Std.Tactic.LibrarySearch.CandidateFinder

Candidate finding function that uses strict discrimination tree for resolution.

Equations

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

opaque Std.Tactic.LibrarySearch.defaultCandidateFinder : IO.Ref Std.Tactic.LibrarySearch.CandidateFinder

The preferred candidate finding function.

def Std.Tactic.LibrarySearch.setDefaultCandidateFinder (cf : Std.Tactic.LibrarySearch.CandidateFinder) : IO Unit

Update the candidate finder used by library search.

Equations

• Std.Tactic.LibrarySearch.setDefaultCandidateFinder cf = ST.Ref.set Std.Tactic.LibrarySearch.defaultCandidateFinder cf

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

Create lemma from name and mod.

Equations

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

@[reducible]

def Std.Tactic.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.

Equations

• Std.Tactic.LibrarySearch.Candidate = ((Lean.MVarId × Lean.MetavarContext) × Lean.Name × Std.Tactic.LibrarySearch.DeclMod)

def Std.Tactic.LibrarySearch.interleaveWith {α : Type u_1} {β : Type u_2} {γ : Type u_3} (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.

Equations

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

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

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

Equations

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

def Std.Tactic.LibrarySearch.SubgoalRankType : Type

A type synonym for our subgoal ranking algorithm.

Equations

• Std.Tactic.LibrarySearch.SubgoalRankType = (Bool × Nat × Int)

instance Std.Tactic.LibrarySearch.instOrdSubgoalRankType : Ord Std.Tactic.LibrarySearch.SubgoalRankType

Equations

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

def Std.Tactic.LibrarySearch.countLocalHypsUsed {m : Type → Type} [Monad m] [Lean.MonadLCtx m] [Lean.MonadMCtx m] (e : Lean.Expr) : m Nat

Count how many local hypotheses appear in an expression.

Equations

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

def Std.Tactic.LibrarySearch.subgoalRanking (goal : Lean.MVarId) (subgoals : List Lean.MVarId) : Lean.MetaM Std.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

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

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

Called to abort speculative execution in library search.

Equations

• Std.Tactic.LibrarySearch.abortSpeculation = throw (Lean.Exception.internal Std.Tactic.LibrarySearch.abortSpeculationId)

def Std.Tactic.LibrarySearch.isAbortSpeculation : Lean.Exception → Bool

Returns true if this is an abort speculation exception.

Equations

• Std.Tactic.LibrarySearch.isAbortSpeculation x = match x with | Lean.Exception.internal id extra => id == Std.Tactic.LibrarySearch.abortSpeculationId | x => false

def Std.Tactic.LibrarySearch.tryOnEach (act : Std.Tactic.LibrarySearch.Candidate → Lean.MetaM (List Lean.MVarId)) (candidates : Array Std.Tactic.LibrarySearch.Candidate) : Lean.MetaM (Option (Array (List Lean.MVarId × Lean.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.

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.

Equations

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

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

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

Equations

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

def Std.Tactic.LibrarySearch.solveByElim (required : List Lean.Expr) (exfalso : Bool) (goals : List Lean.MVarId) (maxDepth : Nat) : Lean.MetaM (List Lean.MVarId)

Shortcut for calling solveByElim.

Equations

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

def Std.Tactic.LibrarySearch.librarySearch (goal : Lean.MVarId) (tactic : Bool → List Lean.MVarId → Lean.MetaM (List Lean.MVarId)) (allowFailure : optParam (Lean.MVarId → Lean.MetaM Bool) fun (x : Lean.MVarId) => pure true) (leavePercentHeartbeats : optParam Nat 10) : Lean.MetaM (Option (Array (List Lean.MVarId × Lean.MetavarContext)))

Try to solve the goal either by:

• calling tactic true
• or applying a library lemma then calling tactic false on the resulting goals.

Typically here tactic is solveByElim, with the Bool flag indicating whether it may retry with exfalso.

If it successfully closes the goal, returns none. 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.

(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 Std.Tactic.LibrarySearch.std_exact?' : Lean.ParserDescr

Syntax for std_exact?

Equations

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

def Std.Tactic.LibrarySearch.std_apply?' : Lean.ParserDescr

Syntax for std_apply?

Equations

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

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

Implementation of the exact? tactic.

Equations

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

def Std.Tactic.LibrarySearch.«termStd_exact?%» : Lean.ParserDescr

Term elaborator using the exact? tactic.

Equations

• Std.Tactic.LibrarySearch.«termStd_exact?%» = Lean.ParserDescr.node `Std.Tactic.LibrarySearch.termStd_exact?% 1024 (Lean.ParserDescr.symbol "std_exact?%")