feat: add ac_nf and test [ac_nf|ac_rfl] for BitVec (#5524)

ac_nf is a counterpart to ac_rfl, which normalizes bitvector expressions
with respect to associativity and commutativity.

While there, also add test coverage for ac_rfl and ac_nf for BitVec,
complementing the existing test coverage.

src/Init/Tactics.lean

@@ -399,6 +399,19 @@ example (a b c d : Nat) : a + b + c + d = d + (b + c) + a := by ac_rfl
 -/
 syntax (name := acRfl) "ac_rfl" : tactic
 
+/--
+`ac_nf` normalizes equalities up to application of an associative and commutative operator.
+```
+instance : Associative (α := Nat) (.+.) := ⟨Nat.add_assoc⟩
+instance : Commutative (α := Nat) (.+.) := ⟨Nat.add_comm⟩
+
+example (a b c d : Nat) : a + b + c + d = d + (b + c) + a := by
+ ac_nf
+ -- goal: a + (b + (c + d)) = a + (b + (c + d))
+```
+-/
+syntax (name := acNf) "ac_nf" : tactic
+
 /--
 The `sorry` tactic closes the goal using `sorryAx`. This is intended for stubbing out incomplete
 parts of a proof while still having a syntactically correct proof skeleton. Lean will give

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

@@ -140,7 +140,7 @@ where
     | .op l r => mkApp2 preContext.op (convertTarget vars l) (convertTarget vars r)
     | .var x => vars[x]!
 
-def rewriteUnnormalized (mvarId : MVarId) : MetaM Unit := do
+def rewriteUnnormalized (mvarId : MVarId) : MetaM MVarId := do
   let simpCtx :=
     {
       simpTheorems  := {}
@@ -149,8 +149,7 @@ def rewriteUnnormalized (mvarId : MVarId) : MetaM Unit := do
     }
   let tgt ← instantiateMVars (← mvarId.getType)
   let (res, _) ← Simp.main tgt simpCtx (methods := { post })
-  let newGoal ← applySimpResultToTarget mvarId tgt res
-  newGoal.refl
+  applySimpResultToTarget mvarId tgt res
 where
   post (e : Expr) : SimpM Simp.Step := do
     let ctx ← Simp.getContext
@@ -171,9 +170,21 @@ where
       | none => return Simp.Step.done { expr := e }
     | e, _ => return Simp.Step.done { expr := e }
 
+def rewriteUnnormalizedRefl (goal : MVarId) : MetaM Unit := do
+  let newGoal ← rewriteUnnormalized goal
+  newGoal.refl
+
+def rewriteUnnormalizedNormalForm (goal : MVarId) : TacticM Unit := do
+  let newGoal ← rewriteUnnormalized goal
+  replaceMainGoal [newGoal]
+
 @[builtin_tactic acRfl] def acRflTactic : Lean.Elab.Tactic.Tactic := fun _ => do
   let goal ← getMainGoal
-  goal.withContext <| rewriteUnnormalized goal
+  goal.withContext <| rewriteUnnormalizedRefl goal
+
+@[builtin_tactic acNf] def acNfTactic : Lean.Elab.Tactic.Tactic := fun _ => do
+  let goal ← getMainGoal
+  goal.withContext <| rewriteUnnormalizedNormalForm goal
 
 builtin_initialize
   registerTraceClass `Meta.AC

tests/lean/run/ac_rfl.lean

@@ -37,3 +37,105 @@ example (p q : Prop) : (p ∨ p ∨ q ∧ True) = (q ∨ p) := by
 example : ∀ x : Nat, x = x := by intro x; ac_rfl
 
 example : [1, 2] ++ ([] ++ [2+4, 8] ++ [4]) = [1, 2] ++ [4+2, 8] ++ [4] := by ac_rfl
+
+/- BitVec arithmetic | commutativity -/
+
+example (a b c d : BitVec w) :
+    a * b * c * d = d * c * b * a := by
+  ac_nf
+  rfl
+
+example (a b c d : BitVec w) :
+    a * b * c * d = d * c * b * a := by
+  ac_rfl
+
+example (a b c d : BitVec w) :
+    a + b + c + d = d + c + b + a := by
+  ac_nf
+  rfl
+
+example (a b c d : BitVec w) :
+    a + b + c + d = d + c + b + a := by
+  ac_rfl
+
+/- BitVec arithmetic | associativity -/
+
+example (a b c d : BitVec w) :
+    a * (b * (c * d)) = ((a * b) * c) * d := by
+  ac_nf
+  rfl
+
+example (a b c d : BitVec w) :
+    a * (b * (c * d)) = ((a * b) * c) * d := by
+  ac_rfl
+
+example (a b c d : BitVec w) :
+    a + (b + (c + d)) = ((a + b) + c) + d := by
+  ac_nf
+  rfl
+
+example (a b c d : BitVec w) :
+    a + (b + (c + d)) = ((a + b) + c) + d := by
+  ac_rfl
+
+/- BitVec bitwise operations | commutativity -/
+
+example (a b c d : BitVec w) :
+    a ^^^ b ^^^ c ^^^ d = d ^^^ c ^^^ b ^^^ a := by
+  ac_nf
+  rfl
+
+example (a b c d : BitVec w) :
+    a ^^^ b ^^^ c ^^^ d = d ^^^ c ^^^ b ^^^ a := by
+  ac_rfl
+
+example (a b c d : BitVec w) :
+    a &&& b &&& c &&& d = d &&& c &&& b &&& a := by
+  ac_nf
+  rfl
+
+example (a b c d : BitVec w) :
+    a &&& b &&& c &&& d = d &&& c &&& b &&& a := by
+  ac_rfl
+
+example (a b c d : BitVec w) :
+    a ||| b ||| c ||| d = d ||| c ||| b ||| a := by
+  ac_nf
+  rfl
+
+example (a b c d : BitVec w) :
+    a ||| b ||| c ||| d = d ||| c ||| b ||| a := by
+  ac_rfl
+
+/- BitVec bitwise operations | associativity -/
+
+example (a b c d : BitVec w) :
+    a &&& (b &&& (c &&& d)) = ((a &&& b) &&& c) &&& d := by
+  ac_nf
+  rfl
+
+example (a b c d : BitVec w) :
+    a &&& (b &&& (c &&& d)) = ((a &&& b) &&& c) &&& d := by
+  ac_rfl
+
+example (a b c d : BitVec w) :
+    a ||| (b ||| (c ||| d)) = ((a ||| b) ||| c) ||| d := by
+  ac_nf
+  rfl
+
+example (a b c d : BitVec w) :
+    a ||| (b ||| (c ||| d)) = ((a ||| b) ||| c) ||| d := by
+  ac_rfl
+
+example (a b c d : BitVec w) :
+    a ^^^ (b ^^^ (c ^^^ d)) = ((a ^^^ b) ^^^ c) ^^^ d := by
+  ac_nf
+  rfl
+
+example (a b c d : BitVec w) :
+    a ^^^ (b ^^^ (c ^^^ d)) = ((a ^^^ b) ^^^ c) ^^^ d := by
+  ac_rfl
+
+example (a b c d : Nat) : a + b + c + d = d + (b + c) + a := by
+  ac_nf
+  rfl