rcases subgoals leaking out of have

Stream: lean4

[Patrick Massot]

I just noticed something very weird:

example : True := by
  have : ∃ k, 5 = 2 + k := by
    -- Using apply with a hole create a new goal right here
    -- apply Nat.exists_eq_add_of_le (?_ : 2 ≤ 5)
    -- Using rcases teleports the new goal outside of the have block
    rcases Nat.exists_eq_add_of_le (?_ : 2 ≤ 5) with ⟨k, hk⟩
    exact ⟨k, hk⟩
  trivial -- This trivial solves 2 ≤ 5
  trivial -- this one takes care of True

[Patrick Massot]

This happens with lean4.8.0-rc2. And it is a mwe, no import is required.

[Kyle Miller]

I might guess that it's that rcases is forgetting to capture the metavariables and create new goals, but have then captures the metavariables in the resulting proof term (for example, have : True := ?_ creates a new goal).

This has a similar effect, but with swapped goals for some reason:

example : True := by
  have : ∃ k, 5 = 2 + k :=
    let h := Nat.exists_eq_add_of_le (?_ : 2 ≤ 5)
    by
      rcases h with ⟨k, hk⟩
      exact ⟨k, hk⟩
  trivial -- this one takes care of True
  trivial -- This trivial solves 2 ≤ 5

[Patrick Massot]

I’ve hit this issue again so I opened https://github.com/leanprover/lean4/issues/4331