feat: library_search using (leanprover#503)

Implement the `library_search using X` clause, which only returns results for which `X` appears as a subexpression.

The mathlib3 implementation is still cleverer, but would require full implementation of `solveByElim` with backtracking across multiple goals. I'll get there later.

Co-authored-by: Scott Morrison <[email protected]>

Author: kim-em

Mathlib/Tactic/LibrarySearch.lean

@@ -53,8 +53,24 @@ initialize librarySearchLemmas : DeclCache (DiscrTree Name) ←
 /-- Shortcut for calling `solveByElimImpl`. -/
 def solveByElim (g : MVarId) (depth) := Lean.Tactic.solveByElimImpl false [] depth g
 
-def librarySearch (goal : MVarId) (lemmas : DiscrTree Name) (solveByElimDepth := 6) :
-    MetaM <| Option (Array <| MetavarContext × List MVarId) := do
+/--
+Try to solve the goal either by:
+* calling `solveByElim`
+* or applying a library lemma then calling  `solveByElim` on the resulting goals.
+
+If it successfully closes the goal, returns `none`.
+Otherwise, it returns `some a`, where `a : Array (MetavarContext × List MVarId)`,
+with an entry for each library lemma which was successfully applied,
+containing the metavariable context after the application, and a list of the subsidiary goals.
+
+(Always succeeds, and the metavariable context stored in the monad is reverted,
+unless the goal was completely solved.)
+
+(Note that if `solveByElim` solves some but not all subsidiary goals,
+this is not currently tracked.)
+-/
+def librarySearch (goal : MVarId) (lemmas : DiscrTree Name) (required : List Expr)
+    (solveByElimDepth := 6) : MetaM <| Option (Array <| MetavarContext × List MVarId) := do
   profileitM Exception "librarySearch" (← getOptions) do
   let ty ← goal.getType
   withTraceNode `Tactic.librarySearch (return m!"{exceptOptionEmoji ·} {ty}") do
@@ -65,7 +81,10 @@ def librarySearch (goal : MVarId) (lemmas : DiscrTree Name) (solveByElimDepth :=
 
   try
     solveByElim goal solveByElimDepth
-    return none
+    if (← checkRequired) then
+      return none
+    else
+      set state0
   catch _ =>
     set state0
 
@@ -79,11 +98,16 @@ def librarySearch (goal : MVarId) (lemmas : DiscrTree Name) (solveByElimDepth :=
             newGoal.withContext do
               trace[Tactic.librarySearch] "proving {← addMessageContextFull (mkMVar newGoal)}"
               solveByElim newGoal solveByElimDepth
-          pure $ some $ Sum.inr ()
+          if (← checkRequired) then
+            pure $ some $ Sum.inr ()
+          else
+            set state0
+            pure none
         catch _ =>
           let res := some $ Sum.inl (← getMCtx, newGoals)
+          let check ← checkRequired
           set state0
-          pure res)
+          return if check then res else none)
     catch _ =>
       set state0
       pure none
@@ -93,6 +117,10 @@ def librarySearch (goal : MVarId) (lemmas : DiscrTree Name) (solveByElimDepth :=
     | some (Sum.inl suggestion) => suggestions := suggestions.push suggestion
 
   pure $ some suggestions
+    where
+  /-- Verify that the instantiated goal contains each `Expr` in `required` as a sub-expression.
+  (Make sure to not reset the state before calling.) -/
+  checkRequired : MetaM Bool := return required.all (·.occurs (← instantiateMVars (.mvar goal)))
 
 def lines (ls : List MessageData) :=
   MessageData.joinSep ls (MessageData.ofFormat Format.line)
@@ -101,22 +129,22 @@ open Lean.Parser.Tactic
 
 -- TODO: implement the additional options for `library_search` from Lean 3,
 -- in particular including additional lemmas
--- with `library_search [X, Y, Z]` or `library_search with attr`,
--- or requiring that a particular hypothesis is used in the solution, with `library_search using h`.
+-- with `library_search [X, Y, Z]` or `library_search with attr`.
 syntax (name := librarySearch') "library_search" (config)? (simpArgs)?
-  (" using " (colGt binderIdent)+)? : tactic
+  (" using " (colGt term),+)? : tactic
 syntax (name := librarySearch!) "library_search!" (config)? (simpArgs)?
-  (" using " (colGt binderIdent)+)? : tactic
+  (" using " (colGt term),+)? : tactic
 
 -- For now we only implement the basic functionality.
 -- The full syntax is recognized, but will produce a "Tactic has not been implemented" error.
 
 open Elab.Tactic Elab Tactic in
-elab_rules : tactic | `(tactic| library_search%$tk) => do
+elab_rules : tactic | `(tactic| library_search%$tk $[using $[$required:term],*]?) => do
   let mvar ← getMainGoal
   let (_, goal) ← (← getMainGoal).intros
   goal.withContext do
-    if let some suggestions ← librarySearch goal (← librarySearchLemmas.get) then
+    let required := (← (required.getD #[]).mapM getFVarId).toList.map .fvar
+    if let some suggestions ← librarySearch goal (← librarySearchLemmas.get) required then
       for suggestion in suggestions do
         withMCtx suggestion.1 do
           addExactSuggestion tk (← instantiateMVars (mkMVar mvar))
@@ -129,7 +157,7 @@ elab tk:"library_search%" : term <= expectedType => do
   let goal ← mkFreshExprMVar expectedType
   let (_, introdGoal) ← goal.mvarId!.intros
   introdGoal.withContext do
-    if let some suggestions ← librarySearch introdGoal (← librarySearchLemmas.get) then
+    if let some suggestions ← librarySearch introdGoal (← librarySearchLemmas.get) [] then
       for suggestion in suggestions do
         withMCtx suggestion.1 do
           addTermSuggestion tk (← instantiateMVars goal)

test/librarySearch.lean

@@ -89,25 +89,22 @@ axiom F (a b : ℕ) : f a ≤ f b ↔ a ≤ b
 
 -- TODO theorem nonzero_gt_one (n : ℕ) : ¬ n = 0 → n ≥ 1 := by library_search   -- `exact nat.pos_of_ne_zero`
 
-/- TODO: using
+example (L M : List (List ℕ)) : List ℕ := by library_search using L
 
-example (L : List (List ℕ)) : List ℕ :=
-by library_search using L
+example (P Q : List ℕ) (h : ℕ) : List ℕ := by library_search using h, P
 
-example (n m : ℕ) : ℕ :=
-by library_search using n m
+-- These tests for `using` require moving the required subexpressions check deeper into solveByElim
 
-example (P Q : list ℕ) (h : ℕ) : list ℕ :=
-by library_search using h Q
+-- example (n m : ℕ) : ℕ := by library_search using n, m
 
-example (P Q : list ℕ) (h : ℕ) : list ℕ :=
-by library_search using P Q
+-- example (P Q : List ℕ) (h : ℕ) : List ℕ :=
+-- by library_search using h, Q
 
--- Make sure `library_search` finds nothing when we list too many hypotheses after `using`.
-example (P Q R S T : list ℕ) : list ℕ :=
-begin
-  success_if_fail { library_search using P Q R S T, },
-  exact []
-end
+-- example (P Q : List ℕ) (h : ℕ) : List ℕ :=
+-- by library_search using P, Q
 
--/
+-- -- Make sure `library_search` finds nothing when we list too many hypotheses after `using`.
+-- example (P Q R S T : List ℕ) : List ℕ := by
+--   fail_if_success
+--     library_search using P, Q, R, S, T
+--   exact []