feat: have ring_nf fail if no progress (leanprover-community#24529)

Makes `ring_nf` fail if no progress is made, and adds a new option `failIfUnchanged` (default value := `true`) to the config.

Motivated by stanford-centaur/PyPantograph#97. The unusedTactic linter is not sufficient here because it fails in the presence of certain errors (for example, `unsolved goals`).

Author: plp127

Mathlib/NumberTheory/Padics/PadicNumbers.lean

@@ -647,7 +647,7 @@ theorem exi_rat_seq_conv_cauchy : IsCauSeq (padicNorm p) (limSeq f) := fun ε h
   intro j hj
   suffices
     padicNormE (limSeq f j - f (max N N2) + (f (max N N2) - limSeq f (max N N2)) : ℚ_[p]) < ε by
-    ring_nf at this ⊢
+    ring_nf at this
     rw [← padicNormE.eq_padic_norm']
     exact mod_cast this
   apply lt_of_le_of_lt

Mathlib/Tactic/Group.lean

@@ -64,7 +64,7 @@ syntax (name := aux_group₂) "aux_group₂" (location)? : tactic
 
 macro_rules
 | `(tactic| aux_group₂ $[at $location]?) =>
-  `(tactic| ring_nf $[at $location]?)
+  `(tactic| ring_nf -failIfUnchanged $[at $location]?)
 
 /-- Tactic for normalizing expressions in multiplicative groups, without assuming
 commutativity, using only the group axioms without any information about which group

Mathlib/Tactic/Ring/RingNF.lean

@@ -64,6 +64,8 @@ structure Config where
   zetaDelta := false
   /-- if true, atoms inside ring expressions will be reduced recursively -/
   recursive := true
+  /-- if true, then fail if no progess is made -/
+  failIfUnchanged := true
   /-- The normalization style. -/
   mode := RingMode.SOP
   deriving Inhabited, BEq, Repr
@@ -177,7 +179,10 @@ def ringNFTarget (s : IO.Ref AtomM.State) (cfg : Config) : TacticM Unit := withM
     goal.assign (← mkOfEqTrue (← r.getProof))
     replaceMainGoal []
   else
-    replaceMainGoal [← applySimpResultToTarget goal tgt r]
+    let newGoal ← applySimpResultToTarget goal tgt r
+    if cfg.failIfUnchanged && goal == newGoal then
+      throwError "ring_nf made no progress"
+    replaceMainGoal [newGoal]
 
 /-- Use `ring_nf` to rewrite hypothesis `h`. -/
 def ringNFLocalDecl (s : IO.Ref AtomM.State) (cfg : Config) (fvarId : FVarId) :
@@ -187,7 +192,10 @@ def ringNFLocalDecl (s : IO.Ref AtomM.State) (cfg : Config) (fvarId : FVarId) :
   let myres ← M.run s cfg <| rewrite tgt
   match ← applySimpResultToLocalDecl goal fvarId myres false with
   | none => replaceMainGoal []
-  | some (_, newGoal) => replaceMainGoal [newGoal]
+  | some (_, newGoal) =>
+    if cfg.failIfUnchanged && goal == newGoal then
+      throwError "ring_nf made no progress"
+    replaceMainGoal [newGoal]
 
 /--
 Simplification tactic for expressions in the language of commutative (semi)rings,

MathlibTest/ring.lean

@@ -210,17 +210,21 @@ end
 set_option linter.unusedTactic false in
 example (x : ℝ) (f : ℝ → ℝ) : True := by
   let y := x
+  /-
+  Two of these fail, and two of these succeed in rewriting the instance, so it's not a good idea
+  to use `fail_if_success` since the instances could change without warning.
+  -/
   have : x = y := by
-    ring_nf
+    ring_nf -failIfUnchanged
     ring_nf!
   have : x - y = 0 := by
-    ring_nf
+    ring_nf -failIfUnchanged
     ring_nf!
   have : f x = f y := by
-    ring_nf
+    ring_nf -failIfUnchanged
     ring_nf!
   have : f x - f y = 0 := by
-    ring_nf
+    ring_nf -failIfUnchanged
     ring_nf!
   trivial