feat: add BitVec.getElem_[add|add_add_bool|mul|rotateLeft|rotateRight…

src/Init/Data/BitVec/Bitblast.lean

@@ -164,6 +164,17 @@ theorem getLsbD_add {i : Nat} (i_lt : i < w) (x y : BitVec w) :
       (getLsbD x i ^^ (getLsbD y i ^^ carry i x y false)) := by
   simpa using getLsbD_add_add_bool i_lt x y false
 
+theorem getElem_add_add_bool {i : Nat} (i_lt : i < w) (x y : BitVec w) (c : Bool) :
+    (x + y + setWidth w (ofBool c))[i] =
+      (x[i] ^^ (y[i] ^^ carry i x y c)) := by
+  simp only [← getLsbD_eq_getElem]
+  rw [getLsbD_add_add_bool]
+  omega
+
+theorem getElem_add {i : Nat} (i_lt : i < w) (x y : BitVec w) :
+    (x + y)[i] = (x[i] ^^ (y[i] ^^ carry i x y false)) := by
+  simpa using getElem_add_add_bool i_lt x y false
+
 theorem adc_spec (x y : BitVec w) (c : Bool) :
     adc x y c = (carry w x y c, x + y + setWidth w (ofBool c)) := by
   simp only [adc]
@@ -368,6 +379,10 @@ theorem getLsbD_mul (x y : BitVec w) (i : Nat) :
   · simp
   · omega
 
+theorem getElem_mul (x y : BitVec w) (i : Nat) (h : i < w) :
+    (x * y)[i] = (mulRec x y w)[i] := by
+  simp [mulRec_eq_mul_signExtend_setWidth]
+
 /-! ## shiftLeft recurrence for bitblasting -/
 
 /--

src/Init/Data/BitVec/Lemmas.lean

@@ -525,6 +525,7 @@ theorem getElem_setWidth' (x : BitVec w) (i : Nat) (h : w ≤ v) (hi : i < v) :
     (setWidth' h x)[i] = x.getLsbD i := by
   rw [getElem_eq_testBit_toNat, toNat_setWidth', getLsbD]
 
+@[simp]
 theorem getElem_setWidth (m : Nat) (x : BitVec n) (i : Nat) (h : i < m) :
     (setWidth m x)[i] = x.getLsbD i := by
   rw [setWidth]
@@ -2260,6 +2261,14 @@ theorem getLsbD_rotateLeft {x : BitVec w} {r i : Nat}  :
   · simp
   · rw [← rotateLeft_mod_eq_rotateLeft, getLsbD_rotateLeft_of_le (Nat.mod_lt _ (by omega))]
 
+@[simp]
+theorem getElem_rotateLeft {x : BitVec w} {r i : Nat} (h : i < w) :
+    (x.rotateLeft r)[i] =
+      cond (i < r % w)
+      (x.getLsbD (w - (r % w) + i))
+      (x[i - (r % w)]'(by omega)) := by
+  simp [← BitVec.getLsbD_eq_getElem, h]
+
 /-! ## Rotate Right -/
 
 /--
@@ -2341,6 +2350,15 @@ theorem getLsbD_rotateRight {x : BitVec w} {r i : Nat} :
   · simp
   · rw [← rotateRight_mod_eq_rotateRight, getLsbD_rotateRight_of_le (Nat.mod_lt _ (by omega))]
 
+@[simp]
+theorem getElem_rotateRight {x : BitVec w} {r i : Nat} (h : i < w) :
+    (x.rotateRight r)[i] =
+      cond (i < w - (r % w))
+      (x.getLsbD ((r % w) + i))
+      (x[(i - (w - (r % w)))]) := by
+  simp only [← BitVec.getLsbD_eq_getElem]
+  simp [getLsbD_rotateRight, h]
+
 /- ## twoPow -/
 
 @[simp, bv_toNat]
@@ -2369,6 +2387,12 @@ theorem getLsbD_twoPow (i j : Nat) : (twoPow w i).getLsbD j = ((i < w) && (i = j
           simp at hi
         simp_all
 
+@[simp]
+theorem getElem_twoPow {i j : Nat} (h : j < w) : (twoPow w i)[j] = decide (i = j) := by
+  rw [←getLsbD_eq_getElem, getLsbD_twoPow]
+  simp
+  omega
+
 theorem and_twoPow (x : BitVec w) (i : Nat) :
     x &&& (twoPow w i) = if x.getLsbD i then twoPow w i else 0#w := by
   ext j
@@ -2400,6 +2424,10 @@ theorem twoPow_zero {w : Nat} : twoPow w 0 = 1#w := by
 theorem getLsbD_one {w i : Nat} : (1#w).getLsbD i = (decide (0 < w) && decide (0 = i)) := by
   rw [← twoPow_zero, getLsbD_twoPow]
 
+@[simp]
+theorem getElem_one {w i : Nat} (h : i < w) : (1#w)[i] = decide (0 = i) := by
+  rw [← twoPow_zero, getElem_twoPow]
+
 theorem shiftLeft_eq_mul_twoPow (x : BitVec w) (n : Nat) :
     x <<< n = x * (BitVec.twoPow w n) := by
   ext i
@@ -2504,6 +2532,14 @@ theorem getLsbD_replicate {n w : Nat} (x : BitVec w) :
       simp only [show ¬i < w * n by omega, decide_False, cond_false, hi, Bool.false_and]
       apply BitVec.getLsbD_ge (x := x) (i := i - w * n) (ge := by omega)
 
+@[simp]
+theorem getElem_replicate {n w : Nat} (x : BitVec w) (h : i < w * n) :
+    (x.replicate n)[i] = x.getLsbD (i % w) := by
+  rw [← getLsbD_eq_getElem, getLsbD_replicate]
+  simp only [Bool.and_iff_right_iff_imp, decide_eq_true_eq]
+  intros
+  omega
+
 /-! ### intMin -/
 
 /-- The bitvector of width `w` that has the smallest value when interpreted as an integer. -/