feat: add BitVec.(getElem_umod_of_lt, getElem_umod, getLsbD_umod, getMsbD_umod)

src/Init/Data/BitVec/Bitblast.lean

@@ -1230,4 +1230,36 @@ 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 := (BitVec.not_le (x := d) (y := 0#w)).mp
+    simp only [le_zero_iff] at this
+    rw [← BitVec.umod_eq_divRec (by simp [hd, this])]
+    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 hi : i < w
+  · simp only [BitVec.getLsbD_eq_getElem hi, getElem_umod]
+  · simp [show w ≤ i by omega]
+
+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 hi : i < w
+  · rw [BitVec.getMsbD_eq_getLsbD, getLsbD_umod]
+    simp [BitVec.getMsbD_eq_getLsbD, hi]
+  · simp [show w ≤ i by omega]
+
 end BitVec