ring_nf failing to fully normalize

Stream: mathlib4

[David Renshaw]

import Mathlib.Tactic.Ring

theorem foo (x : ℤ) (h₀ : x^2 - (x - 1) * x = 5) : x = 5 := by
  ring_nf at h₀
  -- I expect h₀ to be `x = 5` now, but instead it is `x ^ 2 - (-x + x ^ 2) = 5`.
  sorry

[David Renshaw]

A more minimal example:

import Mathlib.Tactic.Ring

theorem foo (x : ℤ) (h₀ : x - x + x = 0) : x = 0 := by
  ring_nf at h₀
  -- I expect h₀ to be `x = 0` now, but instead it is `0 + x = 0`.
  sorry

[David Renshaw]

@Mario Carneiro can you explain the purpose of this guard !va.isAtom line?
https://github.com/leanprover-community/mathlib4/blob/c16c0c414d4ea87bd10716ffd38b93d9d66aa215/Mathlib/Tactic/Ring/RingNF.lean#L97

When I comment it out, the unexpected behavior goes away.

[Mario Carneiro]

It is to prevent ring from doing useless rewrites all over the place

[David Renshaw]

but it's looking at the output of the rewrite, right?

[Mario Carneiro]

yes, it's a bit awkward to detect whether the input was an atom because it hasn't been parsed yet

[David Renshaw]

If something rewrites to an atom, that doesn't sound useless to me.

[Mario Carneiro]

for sure, this is a bug, but the fix is not so easy

[David Renshaw]

is there an existing github issue?

[David Renshaw]

I'll open one if not

[Mario Carneiro]

no

[David Renshaw]

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

[Thomas Murrills]

could we add a skipParse field to either the cache or eval which would optionally hold the data necessary to skip the parsing part of eval? Then functions like rewrite could do it themselves (it could be none by default, so nothing would have to change everywhere)

Or, maybe we could refactor the post-parsing part of eval into eval.core or something (which would still itself call eval, not eval.core) (I’m guessing this would need mutual)

[Thomas Murrills]

if one of these would be acceptable I think I could do it

[Scott Morrison]

I don't understand @Thomas Murrills's suggestion here. If they or @Mario Carneiro have time to outline a proposed fix I can try implementing it.

[Mario Carneiro]

The issue is that eval does both parsing and evaluation simultaneously, so it is difficult to tell whether we took the code path "it's an atom so we did nothing" as distinct from "it was not an atom but it was reduced to one", and it's not easy to see what kind of additions we can make that don't impact performance in the normal case. I think the best option would be to just detect atoms directly, basically copying the code of eval but only using it to determine whether we would have done something other than the evalAtom path

[Heather Macbeth]

How did it work in mathlib3?

[Scott Morrison]

!4#2708 hopefully implements Mario's suggestion, and resolves !4#2171.

[Scott Morrison]

I've made another attempt at this one. :-)