toFin thm

leanprover · Nov 8, 2024 · 76b3e74 · 76b3e74
1 parent ca7a608
commit 76b3e74
Showing 1 changed file with 14 additions and 3 deletions.
diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean
@@ -1240,14 +1240,16 @@ theorem toNat_ushiftRight_lt (x : BitVec w) (n : Nat) (hn : n ≤ w) :
     · apply hn
   · apply Nat.pow_pos (by decide)
 
-theorem toNat_ushiftRight_eq_zero (x : BitVec w) (n : Nat) (hn : w < n) :
+theorem toNat_ushiftRight_eq_zero (x : BitVec w) (n : Nat) (hn : w ≤ n) :
     (x >>> n).toNat = 0 := by
   rw [toNat_ushiftRight, Nat.shiftRight_eq_div_pow, Nat.div_eq_of_lt]
-  exact Nat.lt_trans x.isLt (Nat.pow_lt_pow_of_lt Nat.one_lt_two hn)
+  exact Nat.lt_of_lt_of_le x.isLt (Nat.pow_le_pow_of_le Nat.one_lt_two hn)
 
+@[simp]
 theorem toInt_ushiftRight_zero (x : BitVec w) :
     (x >>> 0).toInt = x.toInt := by simp
 
+@[simp]
 theorem toInt_ushiftRight_pos (x : BitVec w) (n : Nat) (hn : 0 < n) :
     (x >>> n).toInt = x.toNat >>> n := by
   rw [toInt_eq_toNat_cond]
@@ -1257,7 +1259,16 @@ theorem toInt_ushiftRight_pos (x : BitVec w) (n : Nat) (hn : 0 < n) :
     simp only [Nat.lt_of_lt_of_le h1 (Nat.pow_le_pow_of_le (Nat.one_lt_two) (show _ ≤ w by omega))]
     simp
   · rw [← toNat_ushiftRight]
-    simp [toNat_ushiftRight_eq_zero x n (Nat.gt_of_not_le hn), Nat.two_pow_pos w]
+    simp [toNat_ushiftRight_eq_zero x n (by omega), Nat.two_pow_pos w]
+
+@[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
+      simp [toNat_ushiftRight_eq_zero x n hn, Nat.dvd_iff_mod_eq_zero.mp (Nat.pow_dvd_pow 2 hn)]
 
 @[simp]
 theorem getMsbD_ushiftRight {x : BitVec w} {i n : Nat} :