Ring tactic bug?

Stream: mathlib4

[Arthur Paulino]

I was playing with the latest Mathlib4 version (3a835b7) and the ring tactic output was a bit strange:

import Mathlib.Tactic.Ring

def sum : Nat → Nat
  | 0     => 0
  | n + 1 => n + 1 + sum n

theorem mulDist {a b c : Nat} : a * (b + c) = a * b + a * c := by ring

theorem twoTimesSumEqTimesSucc {n : Nat} : 2 * sum n = n * (n + 1) := by
  induction n with
    | zero => rfl
    | succ n hi =>
      simp only [sum]
      iterate rw [mulDist]
      rw [hi]
      ring -- unknown free variable '_uniq.1942'

Is this a bug or a misuse of the tactic?

[Gabriel Ebner]

That's a bug.

[Arthur Paulino]

Alright, I'm going to try and debug it

[Jannis Limperg]

The error message indicates that some Expr constructed by the tactic contains an FVarId that doesn't exist. Usually this means that the Expr is used in the wrong context. Maybe that helps with the debugging.

[Arthur Paulino]

The problem happens when calling (m {α := ty, univ := u, cs := inst }).run' {} as the return of RingM.run

[Arthur Paulino]

https://github.com/leanprover-community/mathlib4/issues/165

[Arthur Paulino]

And it's closed :open_mouth:

[Kevin Buzzard]

Thank you!