From 9deff2751fdcb4d52d248e1696ba236daa2eaa9f Mon Sep 17 00:00:00 2001
From: Joachim Breitner <mail@joachim-breitner.de>
Date: Tue, 16 Sep 2025 12:35:46 +0200
Subject: [PATCH] refactor: use reduceBEq in Init (#10398)

This PR uses the `reduceBEq` simproc in Init, but mostly only for
testing, because afer #10351 this code will be derived.
---
 src/Init/Data/Int/Linear.lean        |  6 +++---
 src/Init/Grind/AC.lean               |  4 ++--
 src/Init/Grind/Ordered/Linarith.lean |  6 +++---
 src/Init/Grind/Ring/CommSolver.lean  | 32 ++++++++++++----------------
 src/Init/Grind/ToInt.lean            |  4 ++--
 5 files changed, 24 insertions(+), 28 deletions(-)

diff --git a/src/Init/Data/Int/Linear.lean b/src/Init/Data/Int/Linear.lean
index 088d381cef..fe444723a7 100644
--- a/src/Init/Data/Int/Linear.lean
+++ b/src/Init/Data/Int/Linear.lean
@@ -528,13 +528,13 @@ attribute [local simp] Expr.denote_norm
 
 instance : LawfulBEq Poly where
   eq_of_beq {a} := by
-    induction a <;> intro b <;> cases b <;> simp_all! [BEq.beq]
-    next ih =>
+    induction a <;> intro b <;> cases b <;> simp_all [reduceBEq]
+    next ih _ _ _ =>
       intro _ _ h
       exact ih h
   rfl := by
     intro a
-    induction a <;> simp! [BEq.beq]
+    induction a <;> simp [reduceBEq]
     assumption
 
 attribute [local simp] Poly.denote'_eq_denote
diff --git a/src/Init/Grind/AC.lean b/src/Init/Grind/AC.lean
index 1f2c43539c..722ce6bd9e 100644
--- a/src/Init/Grind/AC.lean
+++ b/src/Init/Grind/AC.lean
@@ -57,9 +57,9 @@ attribute [local simp] Seq.beq'_eq
 
 instance : LawfulBEq Seq where
   eq_of_beq {a} := by
-    induction a <;> intro b <;> cases b <;> simp! [BEq.beq]
+    induction a <;> intro b <;> cases b <;> simp [reduceBEq]
     next x₁ s₁ ih x₂ s₂ => intro h₁ h₂; simp [h₁, ih h₂]
-  rfl := by intro a; induction a <;> simp! [BEq.beq]; assumption
+  rfl := by intro a; induction a <;> simp [reduceBEq]; assumption
 
 noncomputable def Seq.denote {α} (ctx : Context α) (s : Seq) : α :=
   Seq.rec (fun x => x.denote ctx) (fun x _ ih => ctx.op (x.denote ctx) ih) s
diff --git a/src/Init/Grind/Ordered/Linarith.lean b/src/Init/Grind/Ordered/Linarith.lean
index 47828bf173..352121af38 100644
--- a/src/Init/Grind/Ordered/Linarith.lean
+++ b/src/Init/Grind/Ordered/Linarith.lean
@@ -236,13 +236,13 @@ attribute [local simp] Expr.denote_norm
 
 instance : LawfulBEq Poly where
   eq_of_beq {a} := by
-    induction a <;> intro b <;> cases b <;> simp_all! [BEq.beq]
-    next ih =>
+    induction a <;> intro b <;> cases b <;> simp_all [reduceBEq]
+    next ih _ _ _ =>
       intro _ _ h
       exact ih h
   rfl := by
     intro a
-    induction a <;> simp! [BEq.beq]
+    induction a <;> simp [reduceBEq]
     assumption
 
 attribute [local simp] Poly.denote'_eq_denote
diff --git a/src/Init/Grind/Ring/CommSolver.lean b/src/Init/Grind/Ring/CommSolver.lean
index 77c4c9eeb5..a420bf8457 100644
--- a/src/Init/Grind/Ring/CommSolver.lean
+++ b/src/Init/Grind/Ring/CommSolver.lean
@@ -71,8 +71,8 @@ structure Power where
   deriving BEq, Repr, Inhabited, Hashable
 
 instance : LawfulBEq Power where
-  eq_of_beq {a} := by cases a <;> intro b <;> cases b <;> simp_all! [BEq.beq]
-  rfl := by intro a; cases a <;> simp! [BEq.beq]
+  eq_of_beq {a} := by cases a <;> intro b <;> cases b <;> simp_all [reduceBEq]
+  rfl := by intro a; cases a <;> simp [reduceBEq]
 
 protected noncomputable def Power.beq' (pw₁ pw₂ : Power) : Bool :=
   Power.rec (fun x₁ k₁ => Power.rec (fun x₂ k₂ => Nat.beq x₁ x₂ && Nat.beq k₁ k₂) pw₂) pw₁
@@ -96,15 +96,15 @@ inductive Mon where
   deriving BEq, Repr, Inhabited, Hashable
 
 instance : LawfulBEq Mon where
-  eq_of_beq {a} := by
-    induction a <;> intro b <;> cases b <;> simp_all! [BEq.beq]
-    next p₁ m₁ p₂ m₂ ih =>
-      cases p₁ <;> cases p₂ <;> simp <;> intros <;> simp [*]
-      next h => exact ih h
   rfl := by
     intro a
-    induction a <;> simp! [BEq.beq]
+    induction a <;> simp [reduceBEq]
     assumption
+  eq_of_beq {a} := by
+    induction a <;> intro b <;> cases b <;> simp_all [reduceBEq]
+    next ih _ _ =>
+      intro _ h
+      exact ih h
 
 protected noncomputable def Mon.beq' (m₁ : Mon) : Mon → Bool :=
   Mon.rec
@@ -345,18 +345,14 @@ protected noncomputable def Poly.beq' (p₁ : Poly) : Poly → Bool :=
   simp [← ih p₂, ← Bool.and'_eq_and]; rfl
 
 instance : LawfulBEq Poly where
-  eq_of_beq {a} := by
-    induction a <;> intro b <;> cases b <;> simp_all! [BEq.beq]
-    intro h₁ h₂ h₃
-    rename_i m₁ p₁ _ m₂ p₂ ih
-    replace h₂ : m₁ == m₂ := h₂
-    simp [ih h₃, eq_of_beq h₂]
   rfl := by
     intro a
-    induction a <;> simp! [BEq.beq]
-    rename_i k m p ih
-    change m == m ∧ p == p
-    simp [ih]
+    induction a <;> simp [reduceBEq]
+    assumption
+  eq_of_beq {a} := by
+    induction a <;> intro b <;> cases b <;> simp_all [reduceBEq]
+    intros
+    apply_rules
 
 def Poly.denote [Ring α] (ctx : Context α) (p : Poly) : α :=
   match p with
diff --git a/src/Init/Grind/ToInt.lean b/src/Init/Grind/ToInt.lean
index 07775d131a..7f43b17acc 100644
--- a/src/Init/Grind/ToInt.lean
+++ b/src/Init/Grind/ToInt.lean
@@ -40,8 +40,8 @@ inductive IntInterval : Type where
   deriving BEq, DecidableEq, Inhabited
 
 instance : LawfulBEq IntInterval where
-   rfl := by intro a; cases a <;> simp_all! [BEq.beq]
-   eq_of_beq := by intro a b; cases a <;> cases b <;> simp_all! [BEq.beq]
+   rfl := by intro a; cases a <;> simp [reduceBEq]
+   eq_of_beq := by intro a b; cases a <;> cases b <;> simp_all [reduceBEq]
 
 namespace IntInterval