chore: toFin ushiftRight

leanprover · Nov 27, 2024 · 6cfa705 · 6cfa705
1 parent 5b7c654
commit 6cfa705
Showing 1 changed file with 10 additions and 0 deletions.
diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean
@@ -1361,6 +1361,16 @@ theorem toInt_ushiftRight_eq_ite {x : BitVec w} {n : Nat} :
   · rw [toInt_ushiftRight_of_lt (by omega), toInt_eq_toNat_cond]
     simp [hn]
 
+@[simp]
+theorem toFin_uShiftRight {x : BitVec w} {n : Nat} :
+    (x >>> n).toFin = x.toFin / (Fin.ofNat' (2^w) (2^n)) := by
+    apply Fin.eq_of_val_eq
+    by_cases hn : n < w
+    · simp [Nat.shiftRight_eq_div_pow, Nat.mod_eq_of_lt (Nat.pow_lt_pow_of_lt Nat.one_lt_two hn)]
+    · simp only [Nat.not_lt] at hn
+      rw [ushiftRight_eq_zero (by omega)]
+      simp [Nat.dvd_iff_mod_eq_zero.mp (Nat.pow_dvd_pow 2 hn)]
+
 @[simp]
 theorem getMsbD_ushiftRight {x : BitVec w} {i n : Nat} :
     (x >>> n).getMsbD i = (decide (i < w) && (!decide (i < n) && x.getMsbD (i - n))) := by