From 23bd9dfb0906c70dc8453bb08b3f82ca6dfe5434 Mon Sep 17 00:00:00 2001
From: Kyle Miller <kmill31415@gmail.com>
Date: Tue, 4 Feb 2025 06:40:11 -0800
Subject: [PATCH] fix: make `rewrite`/`rw` tactic abort on elaboration errors
 (#6891)

This PR modifies `rewrite`/`rw` to abort rewriting if the elaborated
lemma has any immediate elaboration errors (detected by presence of
synthetic sorries). Rewriting still proceeds if there are elaboration
issues arising from pending synthetic metavariables, like instance
synthesis failures. The purpose of the change is to avoid obscure
"tactic 'rewrite' failed, equality or iff proof expected ?m.5" errors
when for example a lemma does not exist.

This helps error reporting for the natural number game.
https://leanprover.zulipchat.com/#narrow/channel/113489-new-members/topic/Why.20doesn't.20add_left_comm.20work.20here.3F/near/497060022
---
 src/Lean/Elab/Tactic/Rewrite.lean   |  4 ++++
 tests/lean/run/rwWithElabError.lean | 22 ++++++++++++++++++++++
 2 files changed, 26 insertions(+)
 create mode 100644 tests/lean/run/rwWithElabError.lean

diff --git a/src/Lean/Elab/Tactic/Rewrite.lean b/src/Lean/Elab/Tactic/Rewrite.lean
index 55122c71c5..c2da427e69 100644
--- a/src/Lean/Elab/Tactic/Rewrite.lean
+++ b/src/Lean/Elab/Tactic/Rewrite.lean
@@ -15,6 +15,8 @@ open Meta
 def rewriteTarget (stx : Syntax) (symm : Bool) (config : Rewrite.Config := {}) : TacticM Unit := do
   Term.withSynthesize <| withMainContext do
     let e ← elabTerm stx none true
+    if e.hasSyntheticSorry then
+      throwAbortTactic
     let r ← (← getMainGoal).rewrite (← getMainTarget) e symm (config := config)
     let mvarId' ← (← getMainGoal).replaceTargetEq r.eNew r.eqProof
     replaceMainGoal (mvarId' :: r.mvarIds)
@@ -25,6 +27,8 @@ def rewriteLocalDecl (stx : Syntax) (symm : Bool) (fvarId : FVarId) (config : Re
   -- See issues #2711 and #2727.
   let rwResult ← Term.withSynthesize <| withMainContext do
     let e ← elabTerm stx none true
+    if e.hasSyntheticSorry then
+      throwAbortTactic
     let localDecl ← fvarId.getDecl
     (← getMainGoal).rewrite localDecl.type e symm (config := config)
   let replaceResult ← (← getMainGoal).replaceLocalDecl fvarId rwResult.eNew rwResult.eqProof
diff --git a/tests/lean/run/rwWithElabError.lean b/tests/lean/run/rwWithElabError.lean
new file mode 100644
index 0000000000..6013eea931
--- /dev/null
+++ b/tests/lean/run/rwWithElabError.lean
@@ -0,0 +1,22 @@
+/-!
+# Test for error reporting when `rw`/`rewrite` has an elaboration error
+-/
+
+/-!
+Elaboration failures abort tactic evaluation.
+Before, the second error was
+```
+error: tactic 'rewrite' failed, equality or iff proof expected
+  ?m.5
+⊢ True
+```
+-/
+/--
+error: unknown identifier 'not_a_theorem'
+---
+error: unsolved goals
+⊢ True
+-/
+#guard_msgs in
+example : True := by
+  rewrite [not_a_theorem]