fix: prevent exact? and apply? from suggesting invalid tactics (#…

…7192)

This PR prevents `exact?` and `apply?` from suggesting tactics that
correspond to correct proofs but do not elaborate, and it allows these
tactics to suggest `expose_names` when needed.

These tactics now indicate that a non-compiling term was generated but
do not suggest that that term be inserted. `exact?` also no longer
suggests that the user try `apply?` if no partial suggestions were
found.

This addresses part of #5407 but does not achieve the exact expected
behavior therein (due to #6122).

src/Lean/Elab/Tactic/LibrarySearch.lean

@@ -24,28 +24,70 @@ Implementation of the `exact?` tactic.
 def exact? (ref : Syntax) (required : Option (Array (TSyntax `term))) (requireClose : Bool) :
     TacticM Unit := do
   let mvar ← getMainGoal
+  let initialState ← saveState
   let (_, goal) ← (← getMainGoal).intros
   goal.withContext do
     let required := (← (required.getD #[]).mapM getFVarId).toList.map .fvar
     let tactic := fun exfalso =>
-          solveByElim required (exfalso := exfalso) (maxDepth := 6)
+      solveByElim required (exfalso := exfalso) (maxDepth := 6)
     let allowFailure := fun g => do
       let g ← g.withContext (instantiateMVars (.mvar g))
       return required.all fun e => e.occurs g
-    match ← librarySearch goal tactic allowFailure with
+    match (← librarySearch goal tactic allowFailure) with
     -- Found goal that closed problem
     | none =>
-      addExactSuggestion ref (← instantiateMVars (mkMVar mvar)).headBeta
+      addSuggestionIfValid ref mvar initialState
     -- Found suggestions
     | some suggestions =>
-      if requireClose then throwError
-        "`exact?` could not close the goal. Try `apply?` to see partial suggestions."
+      if requireClose then
+        let hint := if suggestions.isEmpty then "" else " Try `apply?` to see partial suggestions."
+        throwError "`exact?` could not close the goal.{hint}"
       reportOutOfHeartbeats `apply? ref
       for (_, suggestionMCtx) in suggestions do
         withMCtx suggestionMCtx do
-          addExactSuggestion ref (← instantiateMVars (mkMVar mvar)).headBeta (addSubgoalsMsg := true)
+          addSuggestionIfValid ref mvar initialState (addSubgoalsMsg := true) (errorOnInvalid := false)
       if suggestions.isEmpty then logError "apply? didn't find any relevant lemmas"
       admitGoal goal
+where
+  /--
+  Executes `tac` in `savedState` (then restores the current state). Used to ensure that a suggested
+  tactic is valid.
+
+  Remark: we don't merely elaborate the proof term's syntax because it may successfully round-trip
+  (d)elaboration but still produce an invalid tactic (see the example in #5407).
+  -/
+  evalTacticWithState (savedState : Tactic.SavedState) (tac : TSyntax `tactic) : TacticM Unit := do
+    let currState ← saveState
+    savedState.restore
+    try
+      Term.withoutErrToSorry <| withoutRecover <| evalTactic tac
+    finally
+      currState.restore
+
+  /--
+  Suggests using the value of `goal` as a proof term if the corresponding tactic is valid at
+  `origGoal`, or else informs the user that a proof exists but is not syntactically valid.
+  -/
+  addSuggestionIfValid (ref : Syntax) (goal : MVarId) (initialState : Tactic.SavedState)
+                       (addSubgoalsMsg := false) (errorOnInvalid := true) : TacticM Unit := do
+    let proofExpr := (← instantiateMVars (mkMVar goal)).headBeta
+    let proofMVars ← getMVars proofExpr
+    let hasMVars := !proofMVars.isEmpty
+    let suggestion ← mkExactSuggestionSyntax proofExpr (useRefine := hasMVars) (exposeNames := false)
+    let mut exposeNames := false
+    try evalTacticWithState initialState suggestion
+    catch _ =>
+      exposeNames := true
+      let suggestion' ← mkExactSuggestionSyntax proofExpr (useRefine := hasMVars) (exposeNames := true)
+      try evalTacticWithState initialState suggestion'
+      catch _ =>
+        let suggestionStr ← SuggestionText.prettyExtra suggestion
+        -- Pretty-print the version without `expose_names` so variable names match the Infoview
+        let msg := m!"found a {if hasMVars then "partial " else ""}proof, \
+                      but the corresponding tactic failed:{indentD suggestionStr}"
+        if errorOnInvalid then throwError msg else logInfo msg
+        return
+    addExactSuggestion ref proofExpr (addSubgoalsMsg := addSubgoalsMsg) (exposeNames := exposeNames)
 
 @[builtin_tactic Lean.Parser.Tactic.exact?]
 def evalExact : Tactic := fun stx => do
@@ -69,7 +111,7 @@ def elabExact?Term : TermElab := fun stx expectedType? => do
     introdGoal.withContext do
       if let some suggestions ← librarySearch introdGoal then
         if suggestions.isEmpty then logError "`exact?%` didn't find any relevant lemmas"
-        else logError "`exact?%` could not close the goal. Try `by apply` to see partial suggestions."
+        else logError "`exact?%` could not close the goal. Try `by apply?` to see partial suggestions."
         mkLabeledSorry expectedType (synthetic := true) (unique := true)
       else
         addTermSuggestion stx (← instantiateMVars goal).headBeta

src/Lean/Elab/Tactic/Try.lean

@@ -48,14 +48,6 @@ private def isExprAccessible (e : Expr) : MetaM Bool := do
   let (_, s) ← e.collectFVars |>.run {}
   s.fvarIds.allM isAccessible
 
-/-- Creates a temporary local context where all names are exposed, and executes `k`-/
-private def withExposedNames (k : MetaM α) : MetaM α := do
-  withNewMCtxDepth do
-    -- Create a helper goal to apply
-    let mvarId := (← mkFreshExprMVar (mkConst ``True)).mvarId!
-    let mvarId ← mvarId.exposeNames
-    mvarId.withContext do k
-
 /-- Executes `tac` in the saved state. This function is used to validate a tactic before suggesting it. -/
 def checkTactic (savedState : SavedState) (tac : TSyntax `tactic) : TacticM Unit := do
   let currState ← saveState

src/Lean/Meta/Tactic/ExposeNames.lean

@@ -7,15 +7,13 @@ prelude
 import Lean.Meta.Tactic.Util
 
 namespace Lean.Meta
-/--
-Creates a new goal whose local context has been "exposed" so that every local declaration has a clear, accessible name.
-If no local declarations require renaming, the original goal is returned unchanged.
--/
-def _root_.Lean.MVarId.exposeNames (mvarId : MVarId) : MetaM MVarId := mvarId.withContext do
-  mvarId.checkNotAssigned `expose_names
+
+/-- Returns a copy of the local context in which all declarations have clear, accessible names. -/
+private def getLCtxWithExposedNames : MetaM LocalContext := do
   let mut map : Std.HashMap Name FVarId := {}
   let mut toRename := #[]
-  for localDecl in (← getLCtx) do
+  let mut lctx ← getLCtx
+  for localDecl in lctx do
     let userName := localDecl.userName
     if userName.hasMacroScopes then
       toRename := toRename.push localDecl.fvarId
@@ -25,9 +23,8 @@ def _root_.Lean.MVarId.exposeNames (mvarId : MVarId) : MetaM MVarId := mvarId.wi
         toRename := toRename.push fvarId
       map := map.insert userName localDecl.fvarId
   if toRename.isEmpty then
-    return mvarId
+    return lctx
   let mut next : Std.HashMap Name Nat := {}
-  let mut lctx ← getLCtx
   -- Remark: Shadowed variables may be inserted later.
   toRename := toRename.qsort fun fvarId₁ fvarId₂ =>
     (lctx.get! fvarId₁).index < (lctx.get! fvarId₂).index
@@ -49,8 +46,21 @@ def _root_.Lean.MVarId.exposeNames (mvarId : MVarId) : MetaM MVarId := mvarId.wi
     next := next.insert baseName i
     map := map.insert userName fvarId
     lctx := lctx.modifyLocalDecl fvarId (·.setUserName userName)
+  return lctx
+
+/--
+Creates a new goal whose local context has been "exposed" so that every local declaration has a clear, accessible name.
+If no local declarations require renaming, the original goal is returned unchanged.
+-/
+def _root_.Lean.MVarId.exposeNames (mvarId : MVarId) : MetaM MVarId := mvarId.withContext do
+  mvarId.checkNotAssigned `expose_names
+  let lctx ← getLCtxWithExposedNames
   let mvarNew ← mkFreshExprMVarAt lctx (← getLocalInstances) (← mvarId.getType) .syntheticOpaque (← mvarId.getTag)
   mvarId.assign mvarNew
   return mvarNew.mvarId!
 
+/-- Creates a temporary local context where all names are exposed, and executes `k` -/
+def withExposedNames (k : MetaM α) : MetaM α := do
+  withNewMCtxDepth <| withLCtx (← getLCtxWithExposedNames) (← getLocalInstances) k
+
 end Lean.Meta

src/Lean/Meta/Tactic/TryThis.lean

@@ -8,6 +8,7 @@ import Lean.Server.CodeActions
 import Lean.Widget.UserWidget
 import Lean.Data.Json.Elab
 import Lean.Data.Lsp.Utf16
+import Lean.Meta.Tactic.ExposeNames
 
 /-!
 # "Try this" support
@@ -430,13 +431,23 @@ def addSuggestions (ref : Syntax) (suggestions : Array Suggestion)
   logInfoAt ref m!"{header}{msgs}"
   addSuggestionCore ref suggestions header (isInline := false) origSpan? style? codeActionPrefix?
 
-private def addExactSuggestionCore (addSubgoalsMsg : Bool) (e : Expr) : MetaM Suggestion :=
+/--
+Returns the syntax for an `exact` or `refine` (as indicated by `useRefine`) tactic corresponding to
+`e`. If `exposeNames` is `true`, prepends the tactic with `expose_names.`
+-/
+def mkExactSuggestionSyntax (e : Expr) (useRefine : Bool) (exposeNames : Bool) : MetaM (TSyntax `tactic) :=
+  withOptions (pp.mvars.set · false) do
+  let exprStx ← (if exposeNames then withExposedNames else id) <| delabToRefinableSyntax e
+  let tac ← if useRefine then `(tactic| refine $exprStx) else `(tactic| exact $exprStx)
+  let tacSeq ← if exposeNames then `(tactic| (expose_names; $tac)) else pure tac
+  return tacSeq
+
+private def addExactSuggestionCore (addSubgoalsMsg : Bool) (exposeNames : Bool) (e : Expr) :
+    MetaM Suggestion :=
   withOptions (pp.mvars.set · false) do
-  let stx ← delabToRefinableSyntax e
   let mvars ← getMVars e
-  let suggestion ← if mvars.isEmpty then `(tactic| exact $stx) else `(tactic| refine $stx)
-  let pp ← ppExpr e
-  let messageData? := if mvars.isEmpty then m!"exact {pp}" else m!"refine {pp}"
+  let mut suggestion ← mkExactSuggestionSyntax e (useRefine := !mvars.isEmpty) exposeNames
+  let messageData? ← SuggestionText.prettyExtra suggestion
   let postInfo? ← if !addSubgoalsMsg || mvars.isEmpty then pure none else
     let mut str := "\nRemaining subgoals:"
     for g in mvars do
@@ -457,11 +468,12 @@ The parameters are:
   `Remaining subgoals:`
 * `codeActionPrefix?`: an optional string to be used as the prefix of the replacement text if the
   suggestion does not have a custom `toCodeActionTitle?`. If not provided, `"Try this: "` is used.
+* `exposeNames`: if true (default false), will insert `expose_names` prior to the generated tactic
 -/
 def addExactSuggestion (ref : Syntax) (e : Expr)
     (origSpan? : Option Syntax := none) (addSubgoalsMsg := false)
-    (codeActionPrefix? : Option String := none): MetaM Unit := do
-  addSuggestion ref (← addExactSuggestionCore addSubgoalsMsg e)
+    (codeActionPrefix? : Option String := none) (exposeNames := false) : MetaM Unit := do
+  addSuggestion ref (← addExactSuggestionCore addSubgoalsMsg exposeNames e)
     (origSpan? := origSpan?) (codeActionPrefix? := codeActionPrefix?)
 
 /-- Add `exact e` or `refine e` suggestions.
@@ -479,8 +491,8 @@ The parameters are:
 -/
 def addExactSuggestions (ref : Syntax) (es : Array Expr)
     (origSpan? : Option Syntax := none) (addSubgoalsMsg := false)
-    (codeActionPrefix? : Option String := none) : MetaM Unit := do
-  let suggestions ← es.mapM <| addExactSuggestionCore addSubgoalsMsg
+    (codeActionPrefix? : Option String := none) (exposeNames := false) : MetaM Unit := do
+  let suggestions ← es.mapM <| addExactSuggestionCore addSubgoalsMsg exposeNames
   addSuggestions ref suggestions (origSpan? := origSpan?) (codeActionPrefix? := codeActionPrefix?)
 
 /-- Add a term suggestion.

tests/lean/librarySearch.lean

@@ -49,7 +49,7 @@ example : x < x + 1 := exact?%
 #guard_msgs in
 example {α : Sort u} (x y : α) : Eq x y := exact?%
 
-/-- error: `exact?%` could not close the goal. Try `by apply` to see partial suggestions. -/
+/-- error: `exact?%` could not close the goal. Try `by apply?` to see partial suggestions. -/
 #guard_msgs in
 example (x y : Nat) : x ≤ y := exact?%
 

tests/lean/run/3922.lean

@@ -20,7 +20,8 @@ axiom r.trans {a b c : Nat} : r a b → r b c → r a c
 /--
 info: Try this: refine r.symm ?_
 ---
-info: Try this: refine r.trans ?_ ?_
+info: found a partial proof, but the corresponding tactic failed:
+  refine r.trans ?_ ?_
 ---
 warning: declaration uses 'sorry'
 -/

tests/lean/run/5407.lean

@@ -0,0 +1,73 @@
+/-!
+# Library search should not return invalid tactics
+
+https://github.com/leanprover/lean4/issues/5407
+
+The library-search tactics `exact?` and `apply?` should not suggest proof terms that do not
+compile. If such proof terms are generated, these tactics should instead provide users with
+appropriate feedback.
+-/
+
+/-! Discards unprintable implicit argument to lambda -/
+inductive Odd : Nat → Prop
+  | one : Odd 1
+  | add_two : Odd n → Odd (n + 2)
+
+theorem odd_iff {n : Nat} : Odd n ↔ n % 2 = 1 := by
+  refine ⟨fun h => by induction h <;> omega, ?_⟩
+  match n with
+  | 0 => simp
+  | 1 => exact fun _ => Odd.one
+  | n + 2 => exact fun _ => Odd.add_two (odd_iff.mpr (by omega))
+
+/--
+error: found a proof, but the corresponding tactic failed:
+  exact fun a => (fun {n} => odd_iff.mpr) a
+-/
+#guard_msgs in
+example {n : Nat} : n % 2 = 1 → Odd n :=
+  by exact?
+
+
+/-! Detects shadowed variables -/
+opaque A : Type
+opaque B : Type
+opaque C : Prop
+axiom imp : A → B → C
+axiom a : A
+axiom b : B
+/--
+info: Try this: (expose_names; exact imp h_1 h)
+-/
+#guard_msgs in
+example : C := by
+  have h : A := a
+  have h : B := b
+  exact?
+
+
+/-! Detects lambdas with insufficient explicit binder types -/
+inductive EqExplicit {α} : α → α → Prop
+  | intro : (a b : α) → a = b → EqExplicit a b
+/--
+error: found a proof, but the corresponding tactic failed:
+  exact EqExplicit.intro (fun f => (fun g x => g x) f) id rfl
+-/
+#guard_msgs in
+example : EqExplicit (fun (f : α → β) => (fun g x => g x) f) id := by
+  exact?
+
+/-! `apply?` logs info instead of erroring -/
+opaque D : Prop
+axiom option1 : A → D
+axiom option2 {_ : B} : D
+/--
+info: Try this: refine option1 ?_
+---
+info: found a partial proof, but the corresponding tactic failed:
+  refine option2
+---
+warning: declaration uses 'sorry'
+-/
+#guard_msgs in
+example : D := by apply?