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.

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

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

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

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

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

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.

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.

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

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

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

Combine two premise selectors, returning the best suggestions.

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

Filter out theorems from grind-annotated modules when the caller is "grind". Modules marked with grind_annotated contain manually reviewed/annotated theorems, so they should be excluded from automatic premise selection for grind. Other callers (like "simp") still receive suggestions from these modules.

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.

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

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

def Lean.LibrarySuggestions.empty : Selector

The trivial premise selector, which returns no suggestions.

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

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

def Lean.LibrarySuggestions.currentFile : Selector

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

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

opaque Lean.LibrarySuggestions.librarySuggestionsAttr : TagAttribute

Attribute for registering library suggestions selectors.

unsafe def Lean.LibrarySuggestions.getSelectorImpl : MetaM (Option Selector)

Get the currently registered library suggestions selector by looking up the stored declaration name. Returns none if no selector is registered or if evaluation fails.

@[implemented_by Lean.LibrarySuggestions.getSelectorImpl]

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

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.

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.

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