feat: add `BitVec.(getElem_umod_of_lt, getElem_umod, getLsbD_umod, ge…

…tMsbD_umod)` and support `BitVec.le_zero_eq_zero`

This PR adds theorems `BitVec.(getElem_umod_of_lt, getElem_umod, getLsbD_umod, getMsbD_umod)` and support theorem `BitVec.le_zero_eq_zero`. For the defiition of these theorems we rely on `divRec`, excluding the case where `d=0#w`, which is treated separately because there is no infrastructure to reason about this case within `divRec`. In particular, our implementation follows the mathlib standard [where division by 0 yields 0](https://github.com/leanprover/lean4/blob/c7c1e091c9f07ae6f8e8ff7246eb7650e2740dcb/src/Init/Data/BitVec/Basic.lean#L217), while in [SMTLIB this yields `allOnes`](https://github.com/leanprover/lean4/blob/c7c1e091c9f07ae6f8e8ff7246eb7650e2740dcb/src/Init/Data/BitVec/Basic.lean#L237).

Co-authored by @bollu.

src/Init/Data/BitVec/Bitblast.lean

@@ -1230,4 +1230,38 @@ theorem shiftRight_eq_ushiftRightRec (x : BitVec w₁) (y : BitVec w₂) :
   · simp [of_length_zero]
   · simp [ushiftRightRec_eq]
 
+/- ### umod -/
+
+theorem getElem_umod_of_lt {n d : BitVec w} (hi : i < w) (hd : 0#w < d) :
+    (umod n d)[i] = (divRec w {n, d} (DivModState.init w)).r[i] := by
+  rw [← BitVec.umod_eq_divRec] <;> simp [hd]
+
+theorem getElem_umod {n d : BitVec w} (hi : i < w) :
+    (umod n d)[i] = if d = 0#w then n[i] else (divRec w {n, d} (DivModState.init w)).r[i] := by
+  by_cases hd : d = 0#w
+  · simp [hd]
+  · have hd' := BitVec.zero_lt_of_neq_zero hd
+    rw [getElem_umod_of_lt hi hd']
+    simp [hd]
+
+theorem getLsbD_umod {n d : BitVec w}:
+    (umod n d).getLsbD i =
+      if d = 0#w then n.getLsbD i
+      else (divRec w {n, d} (DivModState.init w)).r.getLsbD i := by
+  by_cases hd : d = 0#w
+  · simp [hd]
+  · have hd' := BitVec.zero_lt_of_neq_zero hd
+    rw [← BitVec.umod_eq_divRec hd']
+    simp [hd]
+
+theorem getMsbD_umod {n d : BitVec w}:
+    (umod n d).getMsbD i =
+      if d = 0#w then n.getMsbD i
+      else (divRec w {n, d} (DivModState.init w)).r.getMsbD i := by
+  by_cases hd : d = 0#w
+  · simp [hd]
+  · have hd' := BitVec.zero_lt_of_neq_zero hd
+    rw [← BitVec.umod_eq_divRec hd']
+    simp [hd]
+
 end BitVec