Add additional symmetries and change names as per review

leanprover · Jan 21, 2025 · cffe379 · cffe379
1 parent 1ccb080
commit cffe379
Show file tree

Hide file tree

Showing 2 changed files with 16 additions and 4 deletions.
diff --git a/src/Std/Tactic/BVDecide/Normalize/BitVec.lean b/src/Std/Tactic/BVDecide/Normalize/BitVec.lean
@@ -258,12 +258,20 @@ attribute [bv_normalize] BitVec.mul_zero
 attribute [bv_normalize] BitVec.zero_mul
 
 @[bv_normalize]
-theorem BitVec.neg_mul' (x y : BitVec w) : (~~~x + 1#w) * y = ~~~(x * y) + 1#w := by
-  rw [← BitVec.neg_eq_not_add, ← BitVec.neg_eq_not_add, BitVec.neg_mul]
+theorem BitVec.neg_mul (x y : BitVec w) : (~~~x + 1#w) * y = ~~~(x * y) + 1#w := by
+  rw [← BitVec.neg_eq_not_add, ← BitVec.neg_eq_not_add, _root_.BitVec.neg_mul]
 
 @[bv_normalize]
-theorem BitVec.mul_neg' (x y : BitVec w) : x * (~~~y + 1#w) = ~~~(x * y) + 1#w := by
-  rw [← BitVec.neg_eq_not_add, ← BitVec.neg_eq_not_add, BitVec.mul_neg]
+theorem BitVec.neg_mul' (x y : BitVec w) : (1#w + ~~~x) * y = ~~~(x * y) + 1#w := by
+  rw [BitVec.add_comm, BitVec.neg_mul]
+
+@[bv_normalize]
+theorem BitVec.mul_neg (x y : BitVec w) : x * (~~~y + 1#w) = ~~~(x * y) + 1#w := by
+  rw [← BitVec.neg_eq_not_add, ← BitVec.neg_eq_not_add, _root_.BitVec.mul_neg]
+
+@[bv_normalize]
+theorem BitVec.mul_neg' (x y : BitVec w) : x * (1#w + ~~~y) = ~~~(x * y) + 1#w := by
+  rw [BitVec.add_comm, BitVec.mul_neg]
 
 attribute [bv_normalize] BitVec.shiftLeft_zero
 attribute [bv_normalize] BitVec.zero_shiftLeft

diff --git a/tests/lean/run/bv_decide_rewriter.lean b/tests/lean/run/bv_decide_rewriter.lean
@@ -93,8 +93,12 @@ example (x y : BitVec 16) : (-x) * y = -(x * y) := by bv_normalize
 example (x y : BitVec 16) : x * (-y) = -(x * y) := by bv_normalize
 example (x y : BitVec 16) : -x * -y = x * y := by bv_normalize
 example (x y : BitVec 16) : (~~~x + 1) * y = ~~~(x * y) + 1 := by bv_normalize
+example (x y : BitVec 16) : (1 + ~~~x) * y = ~~~(x * y) + 1 := by bv_normalize
 example (x y : BitVec 16) : x * (~~~y + 1) = ~~~(x * y) + 1 := by bv_normalize
+example (x y : BitVec 16) : x * (1 + ~~~y) = ~~~(x * y) + 1 := by bv_normalize
 example (x y : BitVec 16) : (~~~x + 1) * (~~~y + 1) = x * y := by bv_normalize
+example (x y : BitVec 16) : (1 + ~~~x) * (~~~y + 1) = x * y := by bv_normalize
+example (x y : BitVec 16) : (1 + ~~~x) * (1 + ~~~y) = x * y := by bv_normalize
 
 section