feat: support BitVec.abs in bv_decide

leanprover · Oct 26, 2024 · 4a1c236 · 4a1c236
1 parent 106c4e1
commit 4a1c236
Show file tree

Hide file tree

Showing 4 changed files with 6 additions and 0 deletions.
diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean
@@ -2115,6 +2115,8 @@ theorem not_neg (x : BitVec w) : ~~~(-x) = x + -1#w := by
 
 /-! ### abs -/
 
+theorem abs_eq {x : BitVec w} : x.abs = if x.msb then -x else x := by rfl
+
 @[simp, bv_toNat]
 theorem toNat_abs {x : BitVec w} : x.abs.toNat = if x.msb then 2^w - x.toNat else x.toNat := by
   simp only [BitVec.abs, neg_eq]

diff --git a/src/Std/Tactic/BVDecide/Normalize/BitVec.lean b/src/Std/Tactic/BVDecide/Normalize/BitVec.lean
@@ -85,6 +85,7 @@ theorem BitVec.smod_umod (x y : BitVec w) :
   cases x.msb <;> cases y.msb <;> simp
 
 attribute [bv_normalize] Bool.cond_eq_if
+attribute [bv_normalize] BitVec.abs_eq
 
 end Reduce
 

diff --git a/tests/lean/run/bv_arith.lean b/tests/lean/run/bv_arith.lean
@@ -58,3 +58,5 @@ theorem arith_unit_13 (x y : BitVec 8) (hx : x.msb = false) (hy : y.msb = false)
 theorem arith_unit_14 (x y : BitVec 8) (hx : x.msb = true) (hy : y.msb = true) : (-((-x).umod (-y))) = x.smod y := by
   bv_decide
 
+theorem arith_unit_15 (x : BitVec 32) : BitVec.sle x (BitVec.abs x) := by
+  bv_decide
diff --git a/tests/lean/run/bv_decide_rewriter.lean b/tests/lean/run/bv_decide_rewriter.lean
@@ -80,6 +80,7 @@ example {x : BitVec 16} : 2 + (x + 10) = 12 + x := by bv_normalize
 example {x : BitVec 16} : 2 + (10 + x) = 12 + x := by bv_normalize
 example {x : BitVec 16} {b : Bool} : (if b then x else x) = x := by bv_normalize
 example {b : Bool} {x : Bool} : (bif b then x else x) = x := by bv_normalize
+example {x : BitVec 16} : x.abs = if x.msb then -x else x := by bv_normalize
 
 section