rename_bvar is broken

Stream: mathlib4

[Patrick Massot]

Still frantically trying to prepare for teaching using Lean 4, I see the rename_bvar teaching tactic is broken in mathlib4:

import Mathlib.Tactic

example (a b c : ℤ) (h1 : a ∣ b) (h2 : b ∣ c) : a ∣ c := by
  rcases h1 with ⟨k, hk⟩
  show ∃ k, c = a * k
  rename_bvar k → m
  sorry

[Patrick Massot]

Here it does nothing, presumably because there is already some k in the context (but that’s the whole point of the tactic: renaming to avoid apparent notation clash).

[Patrick Massot]

As usual any help is much appreciated while I hunt down the next bug.

[Michael Rothgang]

When this bug gets fixed: it would be great to add this test; the rename_bvar tactic is drastically undertested. (#18139 only added some very basic test.)

[Patrick Massot]

This is the curse of teaching tactics: they are not tested in Mathlib. Usually they are tested in teaching libs before going to Mathlib. But here it was tested in Lean 3 teaching lib, PRed to mathlib3 and ported to Lean 4 without being tested.

[Kyle Miller]

#20743

This case was triggered by metavariables not being handled.

There's also a fix in case the issue was metadata, but I didn't add a test for this.

[Patrick Massot]

Thanks!

[Kyle Miller]

instantiateMVarDeclMVars is a function that could be helpful to fix tactics like this in general (it's a hammer that instantiates all metavariables that appear in the local context and target of a particular goal). Added it to https://github.com/leanprover-community/mathlib4/wiki/Metaprogramming-gotchas