reduce the number of unneeded calls to ac_nf

src/Lean/Meta/Tactic/AC/Sharing.lean

@@ -231,7 +231,20 @@ def canonicalizeEqWithSharing (ty lhs rhs : Expr) : SimpM Simp.Step := do
 def post : Simp.Simproc := fun e => do
   match_expr e with
   | Eq ty lhs rhs => canonicalizeEqWithSharing ty lhs rhs
-  | _ => AC.post e
+  | _ =>
+    let mkApp2 op _ _ := e | return .continue
+    match (← Simp.getContext).parent? with
+    -- Note: the order of the following match-arms is significant, as `canonicalizeEqWithSharing`
+    -- is biased towards the operation of the left-hand-side of the equality, if present.
+    | mkApp3 (.const ``Eq _) _ (mkApp2 op' _ _) _
+    | mkApp3 (.const ``Eq _) _ _ (mkApp2 op' _ _) =>
+      if (← isDefEq op op') then
+        -- In this case, the current expression will already be canonicalized by
+        -- `canonicalizeEqWithSharing`, hence, we don't call regular ac_nf on it
+        return .continue
+      else
+        AC.post e
+    | _ => AC.post e
 
 def rewriteUnnormalizedWithSharing (mvarId : MVarId) : MetaM MVarId := do
   let simpCtx ← Simp.mkContext

tests/lean/run/ac_nf.lean

@@ -36,9 +36,20 @@ theorem mul_eq_mul_eq_left (x y z : BitVec 64) (h : x = y) :
 theorem short_circuit_triple_mul (x x_1 x_2 : BitVec 32) (h : ¬x_2 &&& 4096#32 == 0#32) :
     (x_1 ||| 4096#32) * x * (x_1 ||| 4096#32) = (x_1 ||| x_2 &&& 4096#32) * x * (x_1 ||| 4096#32) := by
   ac_nf'
-  guard_target =ₛ x * (x_1 ||| 4096#32) * (x_1 ||| 4096#32) = x * (x_1 ||| 4096#32) * (x_1 ||| x_2 &&& 4096#32)
+  guard_target =ₛ
+    ((x_1 ||| 4096#32) * x) * (x_1 ||| 4096#32)
+    = ((x_1 ||| 4096#32) * x) * (x_1 ||| x_2 &&& 4096#32)
   sorry
 
+theorem add_mul_mixed (x y z : BitVec 64) :
+    z * (x + y) = (y + x) * z := by
+  ac_nf'; rfl
+
+theorem add_mul_mixed' (x y z : BitVec 64)
+    (h : (x + y) * z = x + y) :
+    z * (x + y) = (y + x) := by
+  ac_nf'; exact h
+
 /-! ### Scaling Test -/
 
 /-- `repeat_add $n with $t` expands to `$t + $t + ... + $t`, with `n` repetitions