chore: use 'library suggestions' rather than 'premise selection' (#11029)

This PR changes the terminology used from "premise selection" to
"library suggestions". This will be more understandable to users (we
don't assume anyone is familiar with the premise selection literature),
and avoids a conflict with the existing use of "premise" in Lean
terminology (e.g. "major premise" in induction, as well as generally the
synonym for "hypothesis"/"argument").

Author: kim-em

src/Init/Grind/Config.lean

@@ -18,9 +18,9 @@ structure Config where
   /-- If `lax` is `true`, `grind` will silently ignore any parameters referring to non-existent theorems
   or for which no patterns can be generated. -/
   lax : Bool := false
-  /-- If `premises` is `true`, `grind` will invoke the currently configured premise selecor on the current goal,
-  and add attempt to use the resulting suggestions as premises to the `grind` tactic. -/
-  premises : Bool := false
+  /-- If `suggestions` is `true`, `grind` will invoke the currently configured library suggestion engine on the current goal,
+  and add attempt to use the resulting suggestions as additional parameters to the `grind` tactic. -/
+  suggestions : Bool := false
   /-- Maximum number of case-splits in a proof search branch. It does not include splits performed during normalization. -/
   splits : Nat := 9
   /-- Maximum number of E-matching (aka heuristic theorem instantiation) rounds before each case split. -/

src/Init/Notation.lean

@@ -863,12 +863,12 @@ syntax (name := infoTreesCmd)
   "#info_trees" " in" ppLine command : command
 
 /--
-Specify a premise selection engine.
-Note that Lean does not ship a default premise selection engine,
+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.
 -/
-syntax (name := setPremiseSelectorCmd)
-  "set_premise_selector" term : command
+syntax (name := setLibrarySuggestionsCmd)
+  "set_library_suggestions" term : command
 
 namespace Parser
 

src/Init/Tactics.lean

@@ -1759,11 +1759,12 @@ as well as tactics such as `next`, `case`, and `rename_i`.
 syntax (name := exposeNames) "expose_names" : tactic
 
 /--
-`#suggest_premises` will suggest premises for the current goal, using the currently registered premise selector.
+`#suggestions` will suggest relevant theorems from the library for the current goal,
+using the currently registered library suggestion engine.
 
 The suggestions are printed in the order of their confidence, from highest to lowest.
 -/
-syntax (name := suggestPremises) "suggest_premises" : tactic
+syntax (name := suggestions) "suggestions" : tactic
 
 /--
 Close fixed-width `BitVec` and `Bool` goals by obtaining a proof from an external SAT solver and

src/Lean.lean

@@ -40,7 +40,7 @@ public import Lean.LabelAttribute
 public import Lean.AddDecl
 public import Lean.Replay
 public import Lean.PrivateName
-public import Lean.PremiseSelection
+public import Lean.LibrarySuggestions
 public import Lean.Namespace
 public import Lean.EnvExtension
 public import Lean.ErrorExplanation

src/Lean/Elab/Tactic/Grind/Main.lean

@@ -9,7 +9,7 @@ public import Lean.Meta.Tactic.Grind.Main
 public import Lean.Meta.Tactic.TryThis
 public import Lean.Elab.Command
 public import Lean.Elab.Tactic.Config
-public import Lean.PremiseSelection.Basic
+public import Lean.LibrarySuggestions.Basic
 import Lean.Meta.Tactic.Grind.SimpUtil
 import Lean.Meta.Tactic.Grind.EMatchTheoremParam
 import Lean.Elab.Tactic.Grind.Basic
@@ -77,35 +77,35 @@ private def parseModifier (s : String) : CoreM Grind.AttrKind := do
   | .ok stx => Grind.getAttrKindCore stx
   | _ => throwError "unexpected modifier {s}"
 
-open PremiseSelection in
-def elabGrindPremises
-    (params : Grind.Params) (premises : Array Suggestion := #[]) : MetaM Grind.Params := do
+open LibrarySuggestions in
+def elabGrindSuggestions
+    (params : Grind.Params) (suggestions : Array Suggestion := #[]) : MetaM Grind.Params := do
   let mut params := params
-  for p in premises do
+  for p in suggestions do
     let attr ← match p.flag with
     | some flag => parseModifier flag
     | none => pure <| .ematch (.default false)
     match attr with
     | .ematch kind =>
       try
         params ← addEMatchTheorem params (mkIdent p.name) p.name kind false (warn := false)
-      catch _ => pure () -- Don't worry if premise suggestion gave bad suggestions.
+      catch _ => pure () -- Don't worry if library suggestions gave bad theorems.
     | _ =>
       -- We could actually support arbitrary grind modifiers,
       -- and call `processParam` rather than `addEMatchTheorem`,
       -- but this would require a larger refactor.
-      -- Let's only do this if there is a prospect of a premise selector supporting this.
+      -- Let's only do this if there is a prospect of a library suggestion engine supporting this.
       throwError "unexpected modifier {p.flag}"
   return params
 
-open PremiseSelection in
-def elabGrindParamsAndPremises
+open LibrarySuggestions in
+def elabGrindParamsAndSuggestions
     (params : Grind.Params)
     (ps : TSyntaxArray ``Parser.Tactic.grindParam)
-    (premises : Array Suggestion := #[])
+    (suggestions : Array Suggestion := #[])
     (only : Bool) (lax : Bool := false) : MetaM Grind.Params := do
   let params ← elabGrindParams params ps (lax := lax) (only := only)
-  elabGrindPremises params premises
+  elabGrindSuggestions params suggestions
 
 def mkGrindParams
     (config : Grind.Config) (only : Bool) (ps : TSyntaxArray ``Parser.Tactic.grindParam) (mvarId : MVarId) :
@@ -119,12 +119,11 @@ def mkGrindParams
   -/
   let casesTypes ← Grind.getCasesTypes
   let params := { params with ematch, casesTypes, inj }
-  let premises ← if config.premises then
-    let suggestions ← PremiseSelection.select mvarId
-    pure suggestions
+  let suggestions ← if config.suggestions then
+    LibrarySuggestions.select mvarId
   else
     pure #[]
-  let params ← elabGrindParamsAndPremises params ps premises (only := only) (lax := config.lax)
+  let params ← elabGrindParamsAndSuggestions params ps suggestions (only := only) (lax := config.lax)
   trace[grind.debug.inj] "{params.inj.getOrigins.map (·.pp)}"
   return params
 
@@ -201,16 +200,16 @@ def setGrindParams (stx : TSyntax `tactic) (params : Array Syntax) : TSyntax `ta
 def getGrindParams (stx : TSyntax `tactic) : Array Syntax :=
   stx.raw[grindParamsPos][1].getSepArgs
 
-/-- Filter out `+premises` from the config syntax -/
-def filterPremisesFromConfig (config : TSyntax ``Lean.Parser.Tactic.optConfig) : TSyntax ``Lean.Parser.Tactic.optConfig :=
+/-- Filter out `+suggestions` from the config syntax -/
+def filterSuggestionsFromConfig (config : TSyntax ``Lean.Parser.Tactic.optConfig) : TSyntax ``Lean.Parser.Tactic.optConfig :=
   let configItems := config.raw.getArgs
   let filteredItems := configItems.filter fun item =>
-    -- Keep all items except +premises
+    -- Keep all items except +suggestions
     -- Structure: null node -> configItem -> posConfigItem -> ["+", ident]
     match item[0]? with
     | some configItem => match configItem[0]? with
       | some posConfigItem => match posConfigItem[1]? with
-        | some ident => !(posConfigItem.getKind == ``Lean.Parser.Tactic.posConfigItem && ident.getId == `premises)
+        | some ident => !(posConfigItem.getKind == ``Lean.Parser.Tactic.posConfigItem && ident.getId == `suggestions)
         | none => true
       | none => true
     | none => true
@@ -232,7 +231,7 @@ def mkGrindOnly
       else
         let param ← Grind.globalDeclToGrindParamSyntax declName kind minIndexable
         params := params.push param
-  let filteredConfig := filterPremisesFromConfig config
+  let filteredConfig := filterSuggestionsFromConfig config
   let result ← `(tactic| grind $filteredConfig:optConfig only)
   return setGrindParams result params
 

src/Lean/Elab/Tactic/Try.lean

@@ -673,7 +673,7 @@ private def mkTryEvalSuggestStx (info : Try.Info) : MetaM (TSyntax `tactic) := d
 
 -- TODO: vanilla `induction`.
 -- TODO: make it extensible.
--- TODO: premise selection.
+-- TODO: library suggestions.
 
 @[builtin_tactic Lean.Parser.Tactic.tryTrace] def evalTryTrace : Tactic := fun stx => do
   match stx with

src/Lean/PremiseSelection.lean src/Lean/LibrarySuggestions.leansrc/Lean/PremiseSelection.lean renamed to src/Lean/LibrarySuggestions.lean

@@ -6,7 +6,7 @@ Authors: Kim Morrison
 module
 
 prelude
-import Lean.PremiseSelection.Basic
-import Lean.PremiseSelection.SymbolFrequency
-import Lean.PremiseSelection.MePo
-import Lean.PremiseSelection.SineQuaNon
+import Lean.LibrarySuggestions.Basic
+import Lean.LibrarySuggestions.SymbolFrequency
+import Lean.LibrarySuggestions.MePo
+import Lean.LibrarySuggestions.SineQuaNon

src/Lean/PremiseSelection/Basic.lean src/Lean/LibrarySuggestions/Basic.leansrc/Lean/PremiseSelection/Basic.lean renamed to src/Lean/LibrarySuggestions/Basic.lean

@@ -12,19 +12,20 @@ public import Lean.Meta.CompletionName
 public import Init.Data.Random
 
 /-!
-# An API for premise selection algorithms.
+# An API for library suggestion algorithms.
 
-This module provides a basic API for premise selection algorithms,
-which are used to suggest identifiers that should be introduced in a proof.
+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`.
 
-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.
+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.
 -/
 
 namespace Lean.Expr.FoldRelevantConstantsImpl
@@ -113,7 +114,7 @@ public def Lean.MVarId.getRelevantConstants (g : MVarId) : MetaM NameSet := with
 
 @[expose] public section
 
-namespace Lean.PremiseSelection
+namespace Lean.LibrarySuggestions
 
 /--
 A `Suggestion` is essentially just an identifier and a confidence score that the identifier is relevant.
@@ -285,52 +286,52 @@ def random (gen : StdGen := ⟨37, 59⟩) : Selector := fun _ cfg => do
       suggestions := suggestions.push { name := name, score := 1.0 / consts.size.toFloat }
   return suggestions
 
-builtin_initialize premiseSelectorExt : EnvExtension (Option Selector) ←
+builtin_initialize librarySuggestionsExt : EnvExtension (Option Selector) ←
   registerEnvExtension (pure none)
 
-/-- Generate premise suggestions for the given metavariable, using the currently registered premise selector. -/
+/-- Generate library suggestions for the given metavariable, using the currently registered library suggestions engine. -/
 def select (m : MVarId) (c : Config := {}) : MetaM (Array Suggestion) := do
-  let some selector := premiseSelectorExt.getState (← getEnv) |
-    throwError "No premise selector registered. \
-      (Note that Lean does not provide a default premise selector, \
+  let some selector := librarySuggestionsExt.getState (← getEnv) |
+    throwError "No library suggestions engine registered. \
+      (Note that Lean does not provide a default library suggestions engine, \
       these must be provided by a downstream library, \
-      and configured using `set_premise_selector`.)"
+      and configured using `set_library_suggestions`.)"
   selector m c
 
 /-!
 Currently the registration mechanism is just global state.
-This means that if multiple modules register premise selectors,
+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
-premise selectors are configured via options in the `lakefile`, and
+library suggestions engines are configured via options in the `lakefile`, and
 commands are only used to override in a single declaration or file.
 -/
 
-/-- Set the current premise selector.-/
-def registerPremiseSelector (selector : Selector) : CoreM Unit := do
-  modifyEnv fun env => premiseSelectorExt.setState env (some selector)
+/-- Set the current library suggestions engine.-/
+def registerLibrarySuggestions (selector : Selector) : CoreM Unit := do
+  modifyEnv fun env => librarySuggestionsExt.setState env (some selector)
 
 open Lean Elab Command in
-@[builtin_command_elab setPremiseSelectorCmd, inherit_doc setPremiseSelectorCmd]
-def elabSetPremiseSelector : CommandElab
-  | `(command| set_premise_selector $selector) => do
-    if `Lean.PremiseSelection.Basic ∉ (← getEnv).header.moduleNames then
-      logWarning "Add `import Lean.PremiseSelection.Basic` before using the `set_premise_selector` command."
+@[builtin_command_elab setLibrarySuggestionsCmd, inherit_doc setLibrarySuggestionsCmd]
+def elabSetLibrarySuggestions : CommandElab
+  | `(command| set_library_suggestions $selector) => do
+    if `Lean.LibrarySuggestions.Basic ∉ (← getEnv).header.moduleNames then
+      logWarning "Add `import Lean.LibrarySuggestions.Basic` before using the `set_library_suggestions` command."
     let selector ← liftTermElabM do
       try
         let selectorTerm ← Term.elabTermEnsuringType selector (some (Expr.const ``Selector []))
         unsafe Meta.evalExpr Selector (Expr.const ``Selector []) selectorTerm
       catch _ =>
         throwError "Failed to elaborate {selector} as a `MVarId → Config → MetaM (Array Suggestion)`."
-    liftCoreM (registerPremiseSelector selector)
+    liftCoreM (registerLibrarySuggestions selector)
   | _ => throwUnsupportedSyntax
 
 open Lean.Elab.Tactic in
-@[builtin_tactic Lean.Parser.Tactic.suggestPremises] def evalSuggestPremises : Tactic := fun _ =>
+@[builtin_tactic Lean.Parser.Tactic.suggestions] def evalSuggestions : Tactic := fun _ =>
   liftMetaTactic1 fun mvarId => do
     let suggestions ← select mvarId
-    logInfo m!"Premise suggestions: {suggestions.map (·.name)}"
+    logInfo m!"Library suggestions: {suggestions.map (·.name)}"
     return mvarId
 
-end Lean.PremiseSelection
+end Lean.LibrarySuggestions

src/Lean/PremiseSelection/MePo.lean src/Lean/LibrarySuggestions/MePo.leansrc/Lean/PremiseSelection/MePo.lean renamed to src/Lean/LibrarySuggestions/MePo.lean

@@ -6,8 +6,8 @@ Authors: Kim Morrison
 module
 
 prelude
-public import Lean.PremiseSelection.Basic
-import Lean.PremiseSelection.SymbolFrequency
+public import Lean.LibrarySuggestions.Basic
+import Lean.LibrarySuggestions.SymbolFrequency
 import Lean.Meta.Basic
 
 /-!
@@ -21,7 +21,7 @@ It needs to be tuned and evaluated for Lean.
 
 open Lean
 
-namespace Lean.PremiseSelection.MePo
+namespace Lean.LibrarySuggestions.MePo
 
 builtin_initialize registerTraceClass `mepo
 

src/Lean/PremiseSelection/SineQuaNon.lean …/Lean/LibrarySuggestions/SineQuaNon.leansrc/Lean/PremiseSelection/SineQuaNon.lean renamed to src/Lean/LibrarySuggestions/SineQuaNon.lean src/Lean/PremiseSelection/SineQuaNon.lean renamed to src/Lean/LibrarySuggestions/SineQuaNon.lean

@@ -9,8 +9,8 @@ prelude
 public import Lean.CoreM
 public import Lean.Meta.Basic
 import Lean.Meta.Instances
-import Lean.PremiseSelection.SymbolFrequency
-public import Lean.PremiseSelection.Basic
+import Lean.LibrarySuggestions.SymbolFrequency
+public import Lean.LibrarySuggestions.Basic
 
 /-!
 # Sine Qua Non premise selection
@@ -21,7 +21,7 @@ This is an implementation of the "Sine Qua Non" premise selection algorithm, fro
 It needs to be tuned and evaluated for Lean.
 -/
 
-namespace Lean.PremiseSelection.SineQuaNon
+namespace Lean.LibrarySuggestions.SineQuaNon
 
 builtin_initialize registerTraceClass `sineQuaNon
 
@@ -193,4 +193,4 @@ public def sineQuaNonSelector (depthFactor : Float := 1.5) : Selector := fun g c
   let suggestions ← sineQuaNon constants config.maxSuggestions depthFactor
   return suggestions.take config.maxSuggestions
 
-end Lean.PremiseSelection
+end Lean.LibrarySuggestions