chore: integrate with bv_decide

leanprover · Oct 28, 2024 · e74a90d · e74a90d
1 parent 4ab1b28
commit e74a90d
Show file tree

Hide file tree

Showing 2 changed files with 46 additions and 0 deletions.
diff --git a/src/Std/Tactic/BVDecide/Normalize/BitVec.lean b/src/Std/Tactic/BVDecide/Normalize/BitVec.lean
@@ -84,6 +84,40 @@ theorem BitVec.smod_umod (x y : BitVec w) :
   rw [BitVec.smod_eq]
   cases x.msb <;> cases y.msb <;> simp
 
+attribute [bv_normalize] BitVec.smtUDiv_eq
+
+@[bv_normalize]
+theorem BitVec.smtSDiv_smtUDiv (x y : BitVec w) :
+    x.smtSDiv y = 
+      if x.msb then
+        if y.msb then
+          (-x).smtUDiv (-y)
+        else
+          -((-x).smtUDiv y)
+      else
+        if y.msb then
+          -(x.smtUDiv (-y))
+        else
+          x.smtUDiv y := by
+  rw [BitVec.smtSDiv_eq]
+  cases x.msb <;> cases y.msb <;> simp
+
+@[bv_normalize]
+theorem BitVec.srem_umod (x y : BitVec w) :
+    x.srem y = 
+      if x.msb then
+        if y.msb then
+          -((-x) % (-y))
+        else
+          -((-x) % y)
+      else
+        if y.msb then
+          x % (-y)
+        else
+          x % y := by
+  rw [BitVec.srem_eq]
+  cases x.msb <;> cases y.msb <;> simp
+
 attribute [bv_normalize] Bool.cond_eq_if
 attribute [bv_normalize] BitVec.abs_eq
 

diff --git a/tests/lean/run/bv_arith.lean b/tests/lean/run/bv_arith.lean
@@ -60,3 +60,15 @@ theorem arith_unit_14 (x y : BitVec 8) (hx : x.msb = true) (hy : y.msb = true) :
 
 theorem arith_unit_15 (x : BitVec 32) : BitVec.sle x (BitVec.abs x) := by
   bv_decide
+
+theorem arith_unit_16 (x y : BitVec 8)  (hy : y ≠ 0) : x.smtUDiv y = x / y := by
+  bv_decide
+
+theorem arith_unit_17 (x y : BitVec 8)  (hy : y = 0) : x.smtUDiv y = -1#8 := by
+  bv_decide
+
+theorem arith_unit_18 (x y : BitVec 8)  (hx : x.msb = true) (h : y.msb = true) : x.smtSDiv y = (-x).smtUDiv (-y) := by
+  bv_decide
+
+theorem arith_unit_19 (x y : BitVec 8)  (hx : x.msb = true) (h : y.msb = true) : x.srem y = -((-x) % (-y)) := by
+  bv_decide