An API for premise selection algorithms.

This module provides a basic API for premise selection algorithms, which are used to suggest identifiers that should be introduced in a proof.

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.PremiseSelection.empty.

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

structure Lean.PremiseSelection.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.PremiseSelection.Config : Type

• maxSuggestions? : Option Nat

  The maximum number of suggestions to return.

• caller : Option Name

  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.

def Lean.PremiseSelection.Config.maxSuggestions (c : Config) : Nat

Equations

• c.maxSuggestions = c.maxSuggestions?.getD 100

@[reducible, inline]

abbrev Lean.PremiseSelection.Selector : Type

Equations

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

def Lean.PremiseSelection.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.PremiseSelection.ppSelector selector g c = do let __do_lift ← Lean.Meta.ppGoal g selector (toString __do_lift) c

def Lean.PremiseSelection.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.PremiseSelection.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 match c.maxSuggestions? with | none => pure suggestions | some max => pure (suggestions.take max)

def Lean.PremiseSelection.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.

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

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

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

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

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

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

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

Equations

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

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

Equations

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

def Lean.PremiseSelection.empty : Selector

The trivial premise selector, which returns no suggestions.

Equations

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

def Lean.PremiseSelection.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.

opaque Lean.PremiseSelection.premiseSelectorExt : EnvExtension (Option Selector)

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

Generate premise suggestions for the given metavariable, using the currently registered premise selector.

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 premise selectors, the behaviour will be dependent on the order of loading modules.

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

def Lean.PremiseSelection.registerPremiseSelector (selector : Selector) : CoreM Unit

Set the current premise selector.

Equations

• Lean.PremiseSelection.registerPremiseSelector selector = Lean.modifyEnv fun (env : Lean.Environment) => Lean.PremiseSelection.premiseSelectorExt.setState env (some selector)

def Lean.PremiseSelection.elabSetPremiseSelector : Elab.Command.CommandElab

Specify a premise selection engine. Note that Lean does not ship a default premise selection 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.PremiseSelection.evalSuggestPremises : Elab.Tactic.Tactic

Equations

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