toInt theorems

src/Init/Data/BitVec/Lemmas.lean

@@ -530,6 +530,11 @@ theorem zeroExtend_eq_setWidth {v : Nat} {x : BitVec w} :
   else
     simp [n_le_i, toNat_ofNat]
 
+@[simp] theorem toInt_setWidth (x : BitVec w) :
+    (x.setWidth v).toInt = Int.bmod (x.toNat) (2^v) := by
+  rw [toInt_eq_toNat_bmod, toNat_setWidth]
+  simp [@Int.emod_bmod _ (2 ^ v)]
+
 theorem setWidth'_eq {x : BitVec w} (h : w ≤ v) : x.setWidth' h = x.setWidth v := by
   apply eq_of_toNat_eq
   rw [toNat_setWidth, toNat_setWidth']
@@ -1568,15 +1573,9 @@ theorem toInt_signExtend_of_gt (x : BitVec w) (hv : w < v):
   <;> simp [h, Nat.mod_eq_of_lt (Nat.lt_of_lt_of_le x.isLt H)]
   omega
 
--- #check setWidth'_eq
-
--- theorem toInt_signExtend (x : BitVec w) :
---   (x.signExtend v).toInt = (x.setWidth v).toInt := by
---   by_cases h : v ≤ w
---   · rw [signExtend_eq_setWidth_of_lt _ h]
---   · have H := Nat.pow_le_pow_of_le_right Nat.two_pos (Nat.le_of_lt (Nat.lt_of_not_le h))
---     rw [toNat_setWidth]
---     rw [Nat.mod_eq_of_lt (Nat.lt_of_lt_of_le x.isLt H)]
+theorem toInt_signExtend_of_le (x : BitVec w) (hv : v ≤ w) :
+  (x.signExtend v).toInt = Int.bmod (x.toNat) (2^v) := by
+  simp [signExtend_eq_setWidth_of_lt _ hv]
 
 
 /-! ### append -/