ring not idempotent

Stream: general

[Kevin Buzzard]

import tactic

-- set_option pp.all true
example (n : ℤ) (hn : 25 * n = n) : n = 0 :=
begin
  have h := sub_eq_zero.mpr hn, -- internally an awkward `0`
  -- h : 25 * n - n = 0
  ring at *, -- `h` now has a better `0`
  -- h : 25 * n - n = 0
  ring at *,
  -- h : 24 * n = 0
  linarith
end

[Riccardo Brasca]

Something similar happened recently in one of my PR, here https://github.com/leanprover-community/mathlib/blob/1e2d820fb10b2a008e346e4f689f9be40c85cf32/src/geometry/euclidean/basic.lean#L200-L201

[Riccardo Brasca]

ring,
ring

works, but ring alone doesn't.

[Bryan Gin-ge Chen]

#3326 has a few other examples

[Riccardo Brasca]

(and moreover I don't what happened, I modified normed_group and this stopped working)

[Mario Carneiro]

Anyone have examples of this happening on terminal ring calls?

[Mario Carneiro]

ring at h is actually a completely different tactic under the hood, it's more like simp_to_SOP

[Junyan Xu]

Mario Carneiro said:

Anyone have examples of this happening on terminal ring calls?

https://github.com/alreadydone/formalising-mathematics/commit/6439475f106653b8eafbb1bf477e9c7d30e10e8b#diff-c9570b5dd291456377e1056063c7c8d2876960e4c2ae01f618661f4c2ea73da6R475
All that the first ring does is a dsimp.
(edit: and Bryan's example in #3326)

[Mario Carneiro]

a #mwe

[Mario Carneiro]

Bryan's version is also not terminal, that's not a goal ring can solve

[Mario Carneiro]

Put another way, ring proves theorems in the language of commutative rings. When given non-theorems, it instead does some debug-only heuristic rewriting for the purpose of showing the user why the goal is failing that is not necessarily idempotent and should not be used in robust proofs

[Scott Morrison]

I wonder if we should split it out into a separate tactic, perhaps ring_nf or ring_normal_form. Then ring could still call ring_nf when it fails, but it would _also_ print a Try this: ring_nf message, to make clear that ring itself is failing.

[Mario Carneiro]

I think that's a good idea. It's pretty easy to get confused about the two functions

[Riccardo Brasca]

Here

https://github.com/leanprover-community/mathlib/pull/6888/commits/4afb7e9984d8ab3c1adfa4356ed84df2fd6a2f78

ring_nf is not idempotent. Is using it twice OK or should I prove it by hand (it just a bunch of rw)?

[Ruben Van de Velde]

Potentially related: https://github.com/leanprover-community/mathlib/issues/3326

[Mario Carneiro]

As my comment above indicates, I don't think you should be using ring_nf at all, certainly not if you are just trying to close a goal. That's what ring is for

[Mario Carneiro]

In the commit that adds ring_nf, I didn't make any attempt to eliminate the existing uses in order to keep the refactor manageable, but arguably every new use of ring_nf should be examined to see whether it isn't supposed to be a proof by congr, ring or something