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.

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.

@[reducible, inline]

abbrev Lean.PremiseSelection.Selector : Type

def Lean.PremiseSelection.empty : Selector

The trivial premise selector, which returns no suggestions.

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

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

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.

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.

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.

def Lean.PremiseSelection.evalSuggestPremises : Elab.Tactic.Tactic