An API for library suggestion algorithms.

This module provides a basic API for library suggestion algorithms, which are used to suggest relevant theorems from the library for the current goal. In the literature this is usually known as "premise selection", but we mostly avoid that term as most of our users will not be familiar with the term.

The core interface is the Selector type, which is a function from a metavariable and a configuration to a list of suggestions. The Selector is registered as an environment extension, and the trivial (no suggestions) implementation is Lean.LibrarySuggestions.empty.

Lean does not provide a default library suggestion engine, so this module is intended to be used in conjunction with a downstream package which registers a library suggestion engine.

@[implemented_by _private.Lean.LibrarySuggestions.Basic.0.Lean.Expr.FoldRelevantConstantsImpl.foldUnsafe]

opaque Lean.Expr.foldRelevantConstants {α : Type} (e : Expr) (init : α) (f : Name → α → MetaM α) : MetaM α

Apply f to every constant occurring in e once, skipping instance arguments and proofs.

def Lean.Expr.relevantConstants (e : Expr) : MetaM (Array Name)

Collect the constants occuring in e (once each), skipping instance arguments and proofs.

Equations

• e.relevantConstants = e.foldRelevantConstants #[] fun (n : Lean.Name) (ns : Array Lean.Name) => pure (ns.push n)

def Lean.Expr.relevantConstantsAsSet (e : Expr) : MetaM NameSet

Collect the constants occuring in e (once each), skipping instance arguments and proofs.

Equations

• e.relevantConstantsAsSet = e.foldRelevantConstants ∅ fun (n : Lean.Name) (ns : Lean.NameSet) => pure (ns.insert n)

def Lean.MVarId.getConstants (g : MVarId) : MetaM NameSet

Equations

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

def Lean.MVarId.getRelevantConstants (g : MVarId) : MetaM NameSet

Equations

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

structure Lean.LibrarySuggestions.Suggestion : Type

A Suggestion is essentially just an identifier and a confidence score that the identifier is relevant. If the premise selection request included information about the intended use (e.g. in the simplifier, in grind, etc.) the score may be adjusted for that application.

• name : Name
• score : Float

  The score of the suggestion, as a probability that this suggestion should be used.

• flag : Option String

  Optional flag associated with the suggestion, e.g. "←" or "=", if the premise selection algorithm is aware of the tactic consuming the results, and wants to suggest modifiers for this suggestion. E.g. this supports calling simp in the reverse direction, or telling grind or aesop to use the theorem in a particular way.

structure Lean.LibrarySuggestions.Config : Type

• maxSuggestions : Nat

  The maximum number of suggestions to return.

• caller : Option String

  The tactic that is calling the premise selection, e.g. simp, grind, or aesop. This may be used to adjust the score of the suggestions

• filter : Name → MetaM Bool

  A filter on suggestions; only suggestions returning true should be returned. (It can be better to filter on the premise selection side, to ensure that enough suggestions are returned.)

• hint : Option String

  An optional arbitrary "hint" to the premise selection algorithm. There is no guarantee that the algorithm will make any use of the hint.

  Potential use cases include a natural language comment provided by the user (e.g. allowing use of the premise selector as a search engine) or including context from the current proof and/or file.

  We may later split these use cases into separate fields if necessary.

@[reducible, inline]

abbrev Lean.LibrarySuggestions.Selector : Type

Equations

• Lean.LibrarySuggestions.Selector = (Lean.MVarId → Lean.LibrarySuggestions.Config → Lean.MetaM (Array Lean.LibrarySuggestions.Suggestion))

def Lean.LibrarySuggestions.ppSelector (selector : String → Config → MetaM (Array Suggestion)) (g : MVarId) (c : Config) : MetaM (Array Suggestion)

Construct a Selector (which acts on an MVarId) from a function which takes the pretty printed goal.

Equations

• Lean.LibrarySuggestions.ppSelector selector g c = do let __do_lift ← Lean.Meta.ppGoal g selector (toString __do_lift) c

def Lean.LibrarySuggestions.Selector.postFilter (selector : Selector) : Selector

Respect the Config.filter option by implementing it as a post-filter. If a premise selection implementation does not natively handle the filter, it should be wrapped with this function.

Equations

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

def Lean.LibrarySuggestions.Selector.maxSuggestions (selector : Selector) : Selector

Wrapper for Selector that ensures the maxSuggestions field in Config is respected, post-hoc.

Equations

• selector.maxSuggestions g c = do let suggestions ← selector g c pure (suggestions.take c.maxSuggestions)

def Lean.LibrarySuggestions.Selector.combine (selector₁ selector₂ : Selector) : Selector

Combine two premise selectors, returning the best suggestions.

Equations

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

def Lean.LibrarySuggestions.Selector.intersperse (selector₁ selector₂ : Selector) (ratio : Float := 0.5) : Selector

Combine two premise selectors by interspersing their results (ignoring scores). The parameter ratio (defaulting to 0.5) controls the ratio of suggestions from each selector while results are available from both.

Equations

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

opaque Lean.LibrarySuggestions.moduleDenyListExt : SimplePersistentEnvExtension String (List String)

Premises from a module whose name has one of the following components are not retrieved.

Use run_cmd modifyEnv fun env => moduleDenyListExt.addEntry env module to add a module to the deny list.

opaque Lean.LibrarySuggestions.nameDenyListExt : SimplePersistentEnvExtension String (List String)

A premise whose name has one of the following components is not retrieved.

Use run_cmd modifyEnv fun env => nameDenyListExt.addEntry env name to add a name to the deny list.

opaque Lean.LibrarySuggestions.typePrefixDenyListExt : SimplePersistentEnvExtension Name (List Name)

A premise whose type.getForallBody.getAppFn is a constant that has one of these prefixes is not retrieved.

Use run_cmd modifyEnv fun env => typePrefixDenyListExt.addEntry env typePrefix to add a type prefix to the deny list.

def Lean.LibrarySuggestions.isDeniedModule (env : Environment) (moduleName : Name) : Bool

Equations

• Lean.LibrarySuggestions.isDeniedModule env moduleName = (Lean.LibrarySuggestions.moduleDenyListExt.getState env).any fun (p : String) => moduleName.anyS fun (x : String) => x == p

def Lean.LibrarySuggestions.isDeniedPremise (env : Environment) (name : Name) : Bool

Equations

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

def Lean.LibrarySuggestions.empty : Selector

The trivial premise selector, which returns no suggestions.

Equations

• Lean.LibrarySuggestions.empty x✝¹ x✝ = pure #[]

def Lean.LibrarySuggestions.random (gen : StdGen := { s1 := 37, s2 := 59 }) : Selector

A random premise selection algorithm, provided solely for testing purposes.

Equations

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

def Lean.LibrarySuggestions.currentFile : Selector

A library suggestion engine that returns locally defined theorems (those in the current file).

Equations

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

opaque Lean.LibrarySuggestions.librarySuggestionsExt : SimplePersistentEnvExtension Syntax (Option Syntax)

def Lean.LibrarySuggestions.elabAndEvalSelector (stx : Syntax) : MetaM Selector

Helper function to elaborate and evaluate selector syntax. This is shared by both validation (elabSetLibrarySuggestions) and retrieval (getSelector).

Equations

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

def Lean.LibrarySuggestions.getSelector : MetaM (Option Selector)

Get the currently registered library suggestions selector by evaluating the stored syntax. Returns none if no selector is registered or if evaluation fails.

Uses Term.elabTermEnsuringType to elaborate arbitrary syntax (not just identifiers).

Equations

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

def Lean.LibrarySuggestions.select (m : MVarId) (c : Config := { }) : MetaM (Array Suggestion)

Generate library suggestions for the given metavariable, using the currently registered library suggestions engine.

Equations

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

Currently the registration mechanism is just global state. This means that if multiple modules register library suggestions engines, the behaviour will be dependent on the order of loading modules.

We should replace this with a mechanism so that library suggestions engines are configured via options in the lakefile, and commands are only used to override in a single declaration or file.

def Lean.LibrarySuggestions.elabSetLibrarySuggestions : Elab.Command.CommandElab

Specify a library suggestion engine. Note that Lean does not ship a default library suggestion engine, so this is only useful in conjunction with a downstream package which provides one.

Equations

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

def Lean.LibrarySuggestions.evalSuggestions : Elab.Tactic.Tactic

Equations

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