From 38ed4346c2981ddb8deb871d1f03368356a948d3 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leomoura@amazon.com>
Date: Fri, 11 Apr 2025 19:39:51 -0700
Subject: [PATCH] chore: improve `grind.clear_aux_decls` error message (#7931)

cc @kim-em
---
 src/Lean/Meta/Tactic/Grind/Util.lean          |  3 +-
 tests/lean/run/grind_clear_error.lean         | 17 ++++++++
 .../grind_ite.lean}                           | 39 ++++++++-----------
 3 files changed, 35 insertions(+), 24 deletions(-)
 create mode 100644 tests/lean/run/grind_clear_error.lean
 rename tests/lean/{grind/clear_aux_decls.lean => run/grind_ite.lean} (90%)

diff --git a/src/Lean/Meta/Tactic/Grind/Util.lean b/src/Lean/Meta/Tactic/Grind/Util.lean
index e25f295902..d243016eff 100644
--- a/src/Lean/Meta/Tactic/Grind/Util.lean
+++ b/src/Lean/Meta/Tactic/Grind/Util.lean
@@ -97,7 +97,8 @@ def _root_.Lean.MVarId.clearAuxDecls (mvarId : MVarId) : MetaM MVarId := mvarId.
     try
       mvarId ← mvarId.clear fvarId
     catch _ =>
-      throwTacticEx `grind.clear_aux_decls mvarId "failed to clear local auxiliary declaration"
+      let userName := (← fvarId.getDecl).userName
+      throwTacticEx `grind mvarId m!"the goal mentions the declaration `{userName}`, which is being defined. To avoid circular reasoning, try rewriting the goal to eliminate `{userName}` before using `grind`."
   return mvarId
 
 /--
diff --git a/tests/lean/run/grind_clear_error.lean b/tests/lean/run/grind_clear_error.lean
new file mode 100644
index 0000000000..8e447aaffd
--- /dev/null
+++ b/tests/lean/run/grind_clear_error.lean
@@ -0,0 +1,17 @@
+reset_grind_attrs%
+set_option grind.warning false
+
+attribute [grind] List.not_mem_nil
+
+/--
+error: tactic 'grind' failed, the goal mentions the declaration `incList`, which is being defined. To avoid circular reasoning, try rewriting the goal to eliminate `incList` before using `grind`.
+as✝ : List Nat
+a : Nat
+as : List Nat
+⊢ ∀ (a : Nat), a ∈ (incList as).val → a > 0
+-/
+#guard_msgs (error) in
+def incList (as : List Nat) : { as : List Nat // ∀ a, a ∈ as → a > 0 } :=
+  match as with
+  | [] => ⟨[], by grind⟩
+  | a::as => ⟨(incList as).1, by grind⟩
diff --git a/tests/lean/grind/clear_aux_decls.lean b/tests/lean/run/grind_ite.lean
similarity index 90%
rename from tests/lean/grind/clear_aux_decls.lean
rename to tests/lean/run/grind_ite.lean
index 9c4a7f9047..789974675b 100644
--- a/tests/lean/grind/clear_aux_decls.lean
+++ b/tests/lean/run/grind_ite.lean
@@ -187,9 +187,6 @@ def IfNormalization : Type := { Z : IfExpr → IfExpr // ∀ e, (Z e).normalized
 See `Statement.lean` for background.
 -/
 
-macro "◾" : tactic => `(tactic| grind)
-macro "◾" : term => `(term| by grind)
-
 set_option grind.warning false
 
 namespace IfExpr
@@ -228,6 +225,9 @@ We don't want a `simp` lemma for `(ite i t e).eval` in general, only once we kno
   | var _ => 1
   | .ite i t e => 2 * normSize i + max (normSize t) (normSize e) + 1
 
+notation "g⟨" a "⟩" => ⟨a, by grind⟩
+macro "c⟨" a:term "⟩" : term => `(have aux := $a; ⟨aux.1, by grind⟩)
+
 /-- Normalizes the expression at the same time as assigning all variables in
 `e` to the literal booleans given by `l` -/
 def normalize (l : AList (fun _ : Nat => Bool)) :
@@ -235,40 +235,33 @@ def normalize (l : AList (fun _ : Nat => Bool)) :
         (∀ f, e'.eval f = e.eval (fun w => (l.lookup w).elim (f w) id))
         ∧ e'.normalized
         ∧ ∀ (v : Nat), v ∈ vars e' → l.lookup v = none }
-  | lit b => ⟨lit b, ◾⟩
+  | lit b => g⟨lit b⟩
   | var v =>
     match h : l.lookup v with
-    | none => ⟨var v, ◾⟩
-    | some b => ⟨lit b, ◾⟩
-  | .ite (lit true)   t e =>
-    -- Fails with `tactic 'grind.clear_aux_decls' failed`:
-    ⟨(normalize l t).1, ◾⟩
-    -- Workaround:
-    -- have t' := normalize l t; ⟨t'.1, ◾⟩
-  | .ite (lit false)  t e => have e' := normalize l e; ⟨e'.1, ◾⟩
-  | .ite (.ite a b c) t e => have i' := normalize l (.ite a (.ite b t e) (.ite c t e)); ⟨i'.1, ◾⟩
+    | none => g⟨var v⟩
+    | some b => g⟨lit b⟩
+  | .ite (lit true)   t e => c⟨normalize l t⟩
+  | .ite (lit false)  t e => c⟨normalize l e⟩
+  | .ite (.ite a b c) t e => c⟨normalize l (.ite a (.ite b t e) (.ite c t e))⟩
   | .ite (var v)      t e =>
     match h : l.lookup v with
     | none =>
       have ⟨t', _⟩ := normalize (l.insert v true) t
       have ⟨e', _⟩ := normalize (l.insert v false) e
       ⟨if t' = e' then t' else .ite (var v) t' e', by
+        -- TODO: automate this proof
         refine ⟨fun f => ?_, ?_, fun w b => ?_⟩
         · -- eval = eval
           simp only [apply_ite, eval_ite_var]
           cases hfv : f v
-          · simp_all
-            ◾
-          · ◾
+          · simp_all; grind
+          · grind
         · -- normalized
           split
-          · ◾
-          · simp only [normalized, disjoint]
-            ◾
-        · -- lookup = none
-          ◾⟩
-    | some b =>
-      have i' := normalize l (.ite (lit b) t e); ⟨i'.1, ◾⟩
+          · grind
+          · simp only [normalized, disjoint]; grind
+        · grind⟩
+    | some b => c⟨normalize l (.ite (lit b) t e)⟩
   termination_by e => e.normSize
 
 /-