feat: BitVec.getMsbD in bv_decide (#5987)

Closes #5983.
leanprover · Nov 7, 2024 · 59ee47a · 59ee47a
1 parent ebc02fc
commit 59ee47a
Show file tree

Hide file tree

Showing 2 changed files with 14 additions and 6 deletions.
diff --git a/src/Std/Tactic/BVDecide/Normalize/BitVec.lean b/src/Std/Tactic/BVDecide/Normalize/BitVec.lean
@@ -122,6 +122,14 @@ attribute [bv_normalize] Bool.cond_eq_if
 attribute [bv_normalize] BitVec.abs_eq
 attribute [bv_normalize] BitVec.twoPow_eq
 
+@[bv_normalize]
+theorem BitVec.getElem_eq_getLsbD (a : BitVec w) (i : Nat) (h : i < w) :
+    a[i]'h = a.getLsbD i := by
+  simp [BitVec.getLsbD_eq_getElem?_getD, BitVec.getElem?_eq, h]
+
+-- The side condition about gets resolved if i and w are constant.
+attribute [bv_normalize] BitVec.getMsbD_eq_getLsbD
+
 end Reduce
 
 section Constant
@@ -137,6 +145,10 @@ attribute [bv_normalize] BitVec.mul_one
 attribute [bv_normalize] BitVec.one_mul
 attribute [bv_normalize] BitVec.not_not
 
+attribute [bv_normalize] decide_true
+attribute [bv_normalize] decide_false
+attribute [bv_normalize] decide_not
+
 end Constant
 
 attribute [bv_normalize] BitVec.zero_and
@@ -280,12 +292,6 @@ theorem BitVec.max_ult' (a : BitVec w) : (BitVec.ult (-1#w) a) = false := by
   simp [this]
 
 attribute [bv_normalize] BitVec.replicate_zero_eq
-
-@[bv_normalize]
-theorem BitVec.getElem_eq_getLsbD (a : BitVec w) (i : Nat) (h : i < w) :
-    a[i] = a.getLsbD i := by
-  simp [BitVec.getLsbD_eq_getElem?_getD, BitVec.getElem?_eq, h]
-
 attribute [bv_normalize] BitVec.add_eq_xor
 attribute [bv_normalize] BitVec.mul_eq_and
 

diff --git a/tests/lean/run/bv_bitwise.lean b/tests/lean/run/bv_bitwise.lean
@@ -38,3 +38,5 @@ theorem bitwise_unit_9 (x y : BitVec 32) :
     BitVec.ofBool (x.getLsbD 0 ^^ y.getLsbD 0) = BitVec.ofBool ((x ^^^ y).getLsbD 0) := by
   bv_decide
 
+theorem bitwise_unit_10 (x : BitVec 2): (x.getMsbD 0) = x.msb := by
+  bv_decide