fix(RingNF): use assoc as a pre lemma (leanprover-community#36947)

This PR was originally meant as a performance improvement, but now serves as a bug fix. The `cleanup` function used by `ring_nf` used to be non-confluent due to using both `add_assoc_rev` and `add_neg`, and it would apply them in the wrong order. This PR fixes that problem by putting `add_assoc_rev` in the pre-simp-set, and keeping `add_neg` in the post-simp-set. This affects a few proofs that needed to be fixed.

When applied to big expressions, associativity lemmas are more efficient as pre lemmas than as post lemmas: as post lemmas, the number of needed rewrites is quadratic instead of linear. This PR applies this idea to the `ring_nf` cleanup function.

Author: JovanGerb

Mathlib/Analysis/SpecialFunctions/BinaryEntropy.lean

@@ -411,7 +411,6 @@ lemma qaryEntropy_strictAntiOn (qLe2 : 2 ≤ q) :
         linarith
       · have qpos : 0 < (q : ℝ) := by positivity
         ring_nf
-        simp only [add_lt_iff_neg_right, neg_add_lt_iff_lt_add, add_zero, gt_iff_lt]
         have : (q : ℝ) - 1 < p * q := by
           have h1 := mul_lt_mul_of_pos_right hp.1 qpos
           have h2 : (1 - (q : ℝ)⁻¹) * ↑q = q - 1 := by calc (1 - (q : ℝ)⁻¹) * ↑q

Mathlib/GroupTheory/SpecificGroups/Quaternion.lean

@@ -93,11 +93,9 @@ instance : Group (QuaternionGroup n) where
   mul := mul
   mul_assoc := by
     rintro (i | i) (j | j) (k | k) <;> simp only [(· * ·), mul] <;> ring_nf
-    congr
-    calc
-      -(n : ZMod (2 * n)) = 0 - n := by rw [zero_sub]
-      _ = 2 * n - n := by norm_cast; simp
-      _ = n := by ring
+    have : (2 * n : ZMod (2 * n)) = 0 := by norm_cast; simp
+    simp only [Mul.mul_eq_hMul]
+    grind
   one := one
   one_mul := by
     rintro (i | i)

Mathlib/NumberTheory/LSeries/HurwitzZetaEven.lean

@@ -166,8 +166,7 @@ lemma hasSum_int_evenKernel (a : ℝ) {t : ℝ} (ht : 0 < t) :
   have (n : ℤ) : cexp (-(π * (n + a) ^ 2 * t)) = cexp (-(π * a ^ 2 * t)) *
       jacobiTheta₂_term n (a * I * t) (I * t) := by
     rw [jacobiTheta₂_term, ← Complex.exp_add]
-    ring_nf
-    simp
+    grind [I_sq]
   simpa [this] using (hasSum_jacobiTheta₂_term _ (by simpa)).mul_left _
 
 lemma hasSum_int_cosKernel (a : ℝ) {t : ℝ} (ht : 0 < t) :

Mathlib/Tactic/Ring/RingNF.lean

@@ -114,10 +114,11 @@ def cleanup (cfg : RingNF.Config) (r : Simp.Result) : MetaM Simp.Result := do
   | .raw => pure r
   | .SOP => do
     let thms : SimpTheorems := {}
-    let thms ← [``add_zero, ``add_assoc_rev, ``_root_.mul_one, ``mul_assoc_rev,
-      ``_root_.pow_one, ``mul_neg, ``add_neg].foldlM (·.addConst ·) thms
+    let thms ← [``add_zero, ``_root_.mul_one, ``_root_.pow_one, ``mul_neg, ``add_neg
+      ].foldlM (·.addConst ·) thms
     let thms ← [``nat_rawCast_0, ``nat_rawCast_1, ``nat_rawCast_2, ``int_rawCast_neg,
-       ``nnrat_rawCast, ``rat_rawCast_neg].foldlM (·.addConst · (post := false)) thms
+      ``nnrat_rawCast, ``rat_rawCast_neg, ``add_assoc_rev, ``mul_assoc_rev
+      ].foldlM (·.addConst · (post := false)) thms
     let ctx ← Simp.mkContext { zetaDelta := cfg.zetaDelta }
       (simpTheorems := #[thms])
       (congrTheorems := ← getSimpCongrTheorems)

MathlibTest/ring.lean

@@ -275,3 +275,14 @@ info: 'test_axioms' depends on axioms: [propext]
 -/
 #guard_msgs in
 #print axioms test_axioms
+
+-- Test that the normalization of `ring_nf` does the right thing
+/--
+trace: a b c d : ℝ
+⊢ a - b - c - d = 0
+-/
+#guard_msgs in
+example (a b c d : ℝ) : a - b - c - d = 0 := by
+  ring_nf
+  trace_state
+  exact test_sorry