feat: add BitVec.(getMsbD, msb)_(extractLsb', extractLsb), getMsbD_extractLsb'_eq_getLsbD

src/Init/Data/BitVec/Lemmas.lean

@@ -781,6 +781,23 @@ protected theorem extractLsb_ofNat (x n : Nat) (hi lo : Nat) :
     (extractLsb' start len x).getLsbD i = (i < len && x.getLsbD (start+i)) := by
   simp [getLsbD, Nat.lt_succ]
 
+@[simp] theorem getMsbD_extractLsb' {start len : Nat} {x : BitVec w} {i : Nat} :
+    (extractLsb' start len x).getMsbD i
+    = (decide (i < len) &&
+    (decide (start + (len - 1 - i) < w) && x.getMsbD (w - 1 - (start + (len - 1 - i))))) := by
+  rcases len with rfl | len
+  · simp
+  · have h : (len - i < len + 1) := by omega
+    rw [getMsbD_eq_getLsbD, getLsbD_extractLsb', getLsbD_eq_getMsbD]
+    simp [h]
+
+@[simp] theorem msb_extractLsb' {start len : Nat} {x : BitVec w} :
+    (extractLsb' start len x).msb
+    = (decide (0 < len) && x.getLsbD (start + len - 1)) := by
+  cases len
+  · simp [BitVec.extractLsb', BitVec.msb]
+  · simp [BitVec.msb, BitVec.getMsbD_eq_getLsbD, BitVec.getLsbD_extractLsb', ← Nat.add_assoc]
+
 @[simp] theorem getElem_extract {hi lo : Nat} {x : BitVec n} {i : Nat} (h : i < hi - lo + 1) :
     (extractLsb hi lo x)[i] = getLsbD x (lo+i) := by
   simp [getElem_eq_testBit_toNat, getLsbD, h]
@@ -789,6 +806,24 @@ protected theorem extractLsb_ofNat (x n : Nat) (hi lo : Nat) :
     getLsbD (extractLsb hi lo x) i = (i ≤ (hi-lo) && getLsbD x (lo+i)) := by
   simp [getLsbD, Nat.lt_succ]
 
+
+@[simp] theorem getMsbD_extractLsb {hi lo : Nat} {x : BitVec w} {i : Nat} :
+    (extractLsb hi lo x).getMsbD i
+    = if lo ≤ hi then decide (i ≤ hi - lo) && (decide (hi - i < w) && x.getMsbD (w - 1 - (hi - i)))
+    else decide (i = 0) && (decide (lo < w) && x.getMsbD (w - 1 - lo)) := by
+  by_cases hlo : lo ≤ hi
+  · simp only [hlo, ↓reduceIte]
+    by_cases hil : i ≤ hi - lo
+    · simp [hil, BitVec.extractLsb, BitVec.getMsbD_extractLsb', Nat.add_sub_cancel, Nat.lt_add_one_iff (m := i) (n := (hi - lo)), show lo + (hi - lo - i) = hi - i by omega]
+    · simp [hil, BitVec.extractLsb]; omega
+  · simp [hlo, BitVec.extractLsb, show hi - lo = 0 by omega, show lo + (hi - lo - i) = lo by omega]
+
+@[simp] theorem msb_extractLsb {hi lo : Nat} {x : BitVec w} :
+    (extractLsb hi lo x).msb
+    = if lo ≤ hi then (decide (hi < w) && x.getMsbD (w - 1 - hi))
+    else (decide (lo < w) && x.getMsbD (w - 1 - lo)) := by
+  simp [BitVec.msb, BitVec.getMsbD_extractLsb, Nat.le_sub_iff_add_le' (k := lo) (n := 0) (m := hi)]
+
 theorem extractLsb'_eq_extractLsb {w : Nat} (x : BitVec w) (start len : Nat) (h : len > 0) :
     x.extractLsb' start len = (x.extractLsb (len - 1 + start) start).cast (by omega) := by
   apply eq_of_toNat_eq