Bug in `ring1`?

Stream: mathlib4

[Heather Macbeth]

By the way, what is going on here? ring failed: not an equality

import Mathlib.Tactic.Ring

def f : Nat → Nat := sorry

example (a : Nat) : 1 * f a * 1 = f (a + 0) := by
  have ha : a + 0 = a := by ring
  rw [ha] -- goal is `1 * f a * 1 = f a`
  ring1 -- ring failed: not an equality

[Notification Bot]

A message was moved here from #mathlib4 > Bug in ring_nf? by Heather Macbeth.

[Heather Macbeth]

Adding a line

change _ = _

fixes it, so it seeems that the problem genuinely is the tactic's failure to identify the equality structure of the goal.

[Thomas Murrills]

Hmm, seems like ring relies on .eq? immediately after getting the type of the goal, which ultimately relies on boolean equality of names (i.e. there's no isDefEq check or whnf or the like)

[Thomas Murrills]

But that's weird. The goal does seem to be an Eq application.

[Thomas Murrills]

Ah! It's the mdata.

[Thomas Murrills]

Specifically, .mdata noImplicitLambda:1, as it shows up in pp.raw

[Thomas Murrills]

Replacing lines 1068-1069 in Ring.Basic with

  let some (α, e₁, e₂) := Expr.consumeMData (← instantiateMVars (← g.getType)) |>.eq?
    | throwError "ring failed: not an equality"

fixes it

[Thomas Murrills]

(But I’m not sure if we’d prefer just a whnf or something? (as well? Does whnf strip mdata?) Called away right now, so can’t explore further!)

[Mario Carneiro]

with whnfR instead of consumeMData that's exactly the same bugfix as I have applied to a small handful of other tactics

[Mario Carneiro]

it's a very common pitfall

[Thomas Murrills]

PR'd (whnfR version): !4#2677

[Heather Macbeth]

Mario Carneiro said:

with whnfR instead of consumeMData that's exactly the same bugfix as I have applied to a small handful of other tactics

One such bugfix by Mario from Feb 8 is still awaiting review, if any tactic experts get time: !4#2173

[Mario Carneiro]

Since as they say you won't recognize your code after coming back to it for a while, I've given it a proper independent review :) and hit the merge button