feat: new bv_distrib tactic (#652)

Co-authored-by: Tobias Grosser <[email protected]>
opencompl · Sep 24, 2024 · d63aaad · d63aaad
1 parent d770d3e
commit d63aaad
Show file tree

Hide file tree

Showing 4 changed files with 50 additions and 16 deletions.
diff --git a/SSA/Projects/InstCombine/BvShift.lean b/SSA/Projects/InstCombine/BvShift.lean
@@ -0,0 +1,36 @@
+/-
+Released under Apache 2.0 license as described in the file LICENSE.
+-/
+
+import SSA.Projects.InstCombine.TacticAuto
+import SSA.Projects.InstCombine.ForLean
+
+@[simp]
+theorem shiftRight_and_or_shiftLeft_distrib {x y z : BitVec w} {n : Nat} :
+    (x >>> n &&& y ||| z) <<< n = x &&& y <<< n ||| z <<< n := by
+  bv_auto
+
+@[simp]
+theorem or_shiftRight_and_shiftLeft_distrib {x y z : BitVec w} {n : Nat} :
+    (z ||| x >>> n &&& y) <<< n = z <<< n ||| x &&& y <<< n := by
+  bv_auto
+
+@[simp]
+theorem shiftRight_and_xor_shiftLeft_distrib {x y z : BitVec w} {n : Nat} :
+    (x >>> n &&& y ^^^ z) <<< n = x &&& y <<< n ^^^ z <<< n := by
+  bv_auto
+
+@[simp]
+theorem xor_shiftRight_and_shiftLeft_distrib {x y z : BitVec w} {n : Nat} :
+    (z ^^^ x >>> n &&& y) <<< n = z <<< n ^^^ x &&& y <<< n := by
+  bv_auto
+
+@[simp]
+theorem and_shiftLeft_allOnes {x y : BitVec w} {n : Nat} :
+    x &&& BitVec.allOnes w <<< n &&& y <<< n = x &&& y <<< n := by
+  bv_auto
+
+@[simp]
+theorem or_shiftLeft_allOnes {x y : BitVec w} {n : Nat} :
+    x ||| BitVec.allOnes w <<< n &&& y <<< n = x ||| y <<< n := by
+  bv_auto
diff --git a/SSA/Projects/InstCombine/ForLean.lean b/SSA/Projects/InstCombine/ForLean.lean
@@ -617,20 +617,9 @@ theorem allOnes_shiftLeft_and_shiftLeft {x : BitVec w} (n : Nat) :
   simp [← BitVec.shiftLeft_and_distrib]
 
 @[simp]
-theorem and_shiftLeft_allOnes {x y : BitVec w} (n : Nat):
-  x &&& BitVec.allOnes w <<< n &&& y <<< n = x &&& y <<< n := by
-  simp [BitVec.and_assoc]
-
-@[simp]
-theorem shiftRight_and_or_shiftLeft_distrib {x y z : BitVec w} {n : Nat}:
-    (x >>> n &&& y ||| z) <<< n = x &&& y <<< n ||| z <<< n := by
-  simp [BitVec.shiftLeft_or_distrib, BitVec.shiftLeft_and_distrib]
-
-@[simp]
-theorem shiftRight_xor_and_shiftLeft_distrib {x y z : BitVec w} {n : Nat} :
-    (x ^^^ y >>> n &&& z) <<< n = y &&& z <<< n ^^^ x <<< n := by
-  simp [BitVec.shiftLeft_xor_distrib, BitVec.shiftLeft_and_distrib]
-  rw [BitVec.xor_comm]
+theorem allOnes_shiftLeft_or_shiftLeft {x : BitVec w} (n : Nat) :
+    BitVec.allOnes w <<< n ||| x <<< n = BitVec.allOnes w <<< n := by
+  simp [← BitVec.shiftLeft_or_distrib]
 
 end BitVec
 

diff --git a/SSA/Projects/InstCombine/HackersDelight.lean b/SSA/Projects/InstCombine/HackersDelight.lean
@@ -157,8 +157,7 @@ theorem sle_iff_add_two_pow_ule_add_two_pow :
 
 theorem ult_iff_not_ule :
     (x <ᵤ y) ↔ ¬ (y ≤ᵤ x) := by
-  try alive_auto
-  all_goals sorry
+  bv_auto
 
 theorem eq_iff_adc_not_add :
     x = y ↔ (BitVec.carry w (x) (~~~ y + 1)) false := by

diff --git a/SSA/Projects/InstCombine/TacticAuto.lean b/SSA/Projects/InstCombine/TacticAuto.lean
@@ -108,6 +108,15 @@ macro "bv_eliminate_bool" : tactic =>
     )
    )
 
+macro "bv_distrib" : tactic =>
+  `(tactic|
+    (
+      try simp [BitVec.shiftLeft_or_distrib, BitVec.shiftLeft_xor_distrib,
+        BitVec.shiftLeft_and_distrib, BitVec.and_assoc, BitVec.or_assoc]
+      try ac_rfl
+    )
+   )
+
 macro "bv_auto": tactic =>
   `(tactic|
       (
@@ -147,6 +156,7 @@ macro "bv_auto": tactic =>
               bv_automata
             )
           | bv_decide
+          | bv_distrib
       )
    )