Generalize seems to try to generalize inside the hypothesis being defined

[ymherklotz]

Prerequisites

Please put an X between the brackets as you perform the following steps:

• Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• Test your test case against the latest nightly release, for example on
  https://live.lean-lang.org/#project=lean-nightly
  (You can also use the settings there to switch to “Lean nightly”)

Description

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. See the following examples:

/-! Fails because it tries to generalize the internal example hypothesis.  However, it should succeed and behave like the second example shown here. -/
example (H: 0 = 0): True := by
  generalize _H : 0 = z at *
  constructor

/-! Produces the expected behaviour. -/
example (H: 0 = 0): True := by
  generalize _H : 0 = z at H
  constructor

/-! This works as well, because it won't generalize under the binder for the internal hypothesis. -/
example (y : Nat) (H: y = 0): True := by
  generalize _H : y = z at *
  constructor

I have also made a tentative PR to try and fix to this.

Context

I tried to prove a few lemmas that required inverting hypotheses, however, these needed some of the arguments to be abstracted using generalize first so that the inversion with cases succeeds. By default I just tried generalize ... at *, however, this failed. Instead I used generalize ... at H which had the expected behaviour.

Steps to Reproduce

Link to example in playground

1. Open the link above and observe that the first generalize fails whereas the two others succeed.

Expected behavior: generalize ... at * and generalize ... at H1 H2 ... HN should behave the same if H1 H2 ... HN are the only visible hypothesis in the context.

Actual behavior: generalize ... at * can fail sometimes where generalize ... at H1 H2 ... HN would succeed, because the wildcard version will try to generalize the internal hypothesis generated by the theorem being proven.

Versions

4.11.0-nightly-2024-07-26

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.