refactor: remove match for Eq

Earlier passes in bv_normalize should have already rewritten all `Eq`s to Beq

src/Lean/Elab/Tactic/BVDecide/Frontend/Normalize/AC.lean

@@ -316,12 +316,8 @@ def canonicalizeWithSharing (P : Expr) (lhs rhs : Expr) : SimpM Simp.Step := do
       proof? := some proof
     }
 
-def post' : Simp.Simproc := fun e => do
+def post : Simp.Simproc := fun e => do
   match_expr e with
-  | Eq ty lhs rhs =>
-      let u ← getLevel ty
-      let P := mkApp (.const ``Eq [u]) ty
-      canonicalizeWithSharing P lhs rhs
   | BEq.beq ty inst lhs rhs =>
       let uLvl ← getDecLevel ty
       let P := mkApp2 (.const ``BEq.beq [uLvl]) ty inst

tests/lean/run/bv_decide_rewriter_ac_nf.lean

@@ -20,45 +20,44 @@ documentation. Any changes to the behaviour of this test should be reflected in
 that docstring also. -/
 /-- warning: declaration uses 'sorry' -/
 #guard_msgs in
-theorem mul_mul_eq_mul_mul (x₁ x₂ y₁ y₂ z : BitVec 4) (h₁ : x₁ = x₂) (h₂ : y₁ = y₂) :
-    x₁ * (y₁ * z) = x₂ * (y₂ * z) := by
+theorem mul_mul_beq_mul_mul (x₁ x₂ y₁ y₂ z : BitVec 4) (h₁ : x₁ = x₂) (h₂ : y₁ = y₂) :
+    x₁ * (y₁ * z) == x₂ * (y₂ * z) := by
   bv_ac_nf
-  guard_target =ₛ z * (x₁ * y₁) = z * (x₂ * y₂)
+  guard_target =ₛ (z * (x₁ * y₁) == z * (x₂ * y₂)) = true
   sorry
 
 /-- warning: declaration uses 'sorry' -/
 #guard_msgs in
-theorem ex_1 (x y z k₁ k₂ l₁ l₂ m₁ m₂ v : BitVec w)
-    (h₁ : k₁ = k₂) (h₂ : l₁ = l₂) (h₃ : m₁ = m₂) :
-    m₁ * x * (y * l₁ * k₁) * z = v * (k₂ * l₂ * x * y) * z * m₂ := by
+theorem ex_1 (x y z k₁ k₂ l₁ l₂ m₁ m₂ v : BitVec w) :
+    m₁ * x * (y * l₁ * k₁) * z == v * (k₂ * l₂ * x * y) * z * m₂ := by
   bv_ac_nf
-  guard_target =ₛ x * y * z * (m₁ * l₁ * k₁) = x * y * z * (v * k₂ * l₂ * m₂)
+  guard_target =ₛ (x * y * z * (m₁ * l₁ * k₁) == x * y * z * (v * k₂ * l₂ * m₂)) = true
   sorry
 
 /-- warning: declaration uses 'sorry' -/
 #guard_msgs in
 theorem ex_2 (x y : BitVec w) (h₁ : y = x) :
-    x * x * x * x = y * x * x * y := by
+    x * x * x * x == y * x * x * y := by
   bv_ac_nf
-  guard_target =ₛ x * x * (x * x) = x * x * (y * y)
+  guard_target =ₛ (x * x * (x * x) == x * x * (y * y)) = true
   sorry
 
 -- This theorem is short-circuited and scales to standard bitwidths.
 /-- warning: declaration uses 'sorry' -/
 #guard_msgs in
-theorem mul_eq_mul_eq_right (x y z : BitVec 64) (h : x = y) :
-    x * z = y * z := by
+theorem mul_beq_mul_eq_right (x y z : BitVec 64) (h : x = y) :
+    x * z == y * z := by
   bv_ac_nf
-  guard_target =ₛ z * x = z * y
+  guard_target =ₛ (z * x == z * y) = true
   sorry
 
 -- This theorem is short-circuited and scales to standard bitwidths.
 /-- warning: declaration uses 'sorry' -/
 #guard_msgs in
-theorem mul_eq_mul_eq_left (x y z : BitVec 64) (h : x = y) :
-    z * x = z * y := by
+theorem mul_beq_mul_eq_left (x y z : BitVec 64) (h : x = y) :
+    z * x == z * y := by
   bv_ac_nf
-  guard_target =ₛ z * x = z * y
+  guard_target =ₛ (z * x == z * y) = true
   sorry
 
 /-- warning: declaration uses 'sorry' -/