fix: wildcard generalize only generalizes visible theorems (leanpro…

…ver#4846)

`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 leanprover#4845

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

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

tests/lean/4845.lean.expected.out

@@ -0,0 +1,4 @@
+z : Nat
+_H : 0 = z
+H : z = z
+⊢ True