From 34819d87a29d3acdf4baccab162a90427d283c13 Mon Sep 17 00:00:00 2001
From: Yann Herklotz <git@yannherklotz.com>
Date: Fri, 26 Jul 2024 22:53:15 +0200
Subject: [PATCH] fix: wildcard `generalize` only generalizes visible theorems

`generalize ... at *` sometimes will try to modify the recursive hypothesis
corresponding to the current theorem being defined, which may not be the
expected behaviour.  It should only try to `generalize` hypotheses that it can
actually modify and are visible, not implementation details. Otherwise this
means that there are discrepancies between `generalize ... at *` and `generalize
... at H`, even though `H` is the only hypothesis in the context.

This commit uses `getLocalHyps` instead of `getFVarIds` to get the current valid
`FVarIds` in the context.  This uses `isImplementationDetail` to filter out
`FVarIds` that are implementation details in the context and are not visible to
the user and should not be manipulated by `generalize`.

Closes 4845
---
 src/Lean/Elab/Tactic/Generalize.lean |  2 +-
 tests/lean/4845.lean                 | 12 ++++++++++++
 tests/lean/4845.lean.expected.out    |  4 ++++
 3 files changed, 17 insertions(+), 1 deletion(-)
 create mode 100644 tests/lean/4845.lean
 create mode 100644 tests/lean/4845.lean.expected.out

diff --git a/src/Lean/Elab/Tactic/Generalize.lean b/src/Lean/Elab/Tactic/Generalize.lean
index 3860107a687b..c76a4a048e55 100644
--- a/src/Lean/Elab/Tactic/Generalize.lean
+++ b/src/Lean/Elab/Tactic/Generalize.lean
@@ -30,7 +30,7 @@ open Meta
       args := args.push { hName?, expr, xName? := arg[3].getId : GeneralizeArg }
     let hyps ← match expandOptLocation stx[2] with
     | .targets hyps _ => getFVarIds hyps
-    | .wildcard => pure (← getLCtx).getFVarIds
+    | .wildcard => pure ((← getLocalHyps).map (·.fvarId!))
     let mvarId ← getMainGoal
     mvarId.withContext do
       let (_, newVars, mvarId) ← mvarId.generalizeHyp args hyps
diff --git a/tests/lean/4845.lean b/tests/lean/4845.lean
new file mode 100644
index 000000000000..f22af6301e5e
--- /dev/null
+++ b/tests/lean/4845.lean
@@ -0,0 +1,12 @@
+/-!
+  Generalize should not try to abstract the variable from hypotheses that are
+  implementation details. -/
+
+/-!
+  In this case, generalize tries to revert the lemma being defined to generalize
+  the 0 in it. -/
+
+example : 0 = 0 → True := by
+  intro H; generalize _H : 0 = z at *
+  trace_state
+  constructor
diff --git a/tests/lean/4845.lean.expected.out b/tests/lean/4845.lean.expected.out
new file mode 100644
index 000000000000..7a20a98e3073
--- /dev/null
+++ b/tests/lean/4845.lean.expected.out
@@ -0,0 +1,4 @@
+z : Nat
+_H : 0 = z
+H : z = z
+⊢ True