chore: pass on implementation

Author: bollu

src/Init/Data/BitVec/Lemmas.lean

@@ -531,9 +531,8 @@ theorem zeroExtend_eq_setWidth {v : Nat} {x : BitVec w} :
     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)]
+    (x.setWidth v).toInt = Int.bmod x.toNat (2^v) := by
+  simp [toInt_eq_toNat_bmod, toNat_setWidth, Int.emod_bmod]
 
 theorem setWidth'_eq {x : BitVec w} (h : w ≤ v) : x.setWidth' h = x.setWidth v := by
   apply eq_of_toNat_eq
@@ -1537,30 +1536,43 @@ theorem signExtend_eq_setWidth_of_lt (x : BitVec w) {v : Nat} (hv : v ≤ w):
 theorem signExtend_eq (x : BitVec w) : x.signExtend w = x := by
   rw [signExtend_eq_setWidth_of_lt _ (Nat.le_refl _), setWidth_eq]
 
-theorem toNat_signExtend_of_gt (x : BitVec w) {v : Nat} (hv : v >= w):
-  (x.signExtend v).toNat = x.toNat + (2^v - 2^w) * (if x.msb then 1 else 0) := by
+/-- Sign extending to a larger bitwidth depends on the msb.
+If the msb is false, then the result equals the original value.
+If the msb is true, then we add a value of `(2^v - 2^w)`, which arises from the sign extension. -/
+theorem toNat_signExtend_of_le (x : BitVec w) {v : Nat} (hv : w ≤ v) :
+  (x.signExtend v).toNat = x.toNat + if x.msb then 2^v - 2^w else 0 := by
   apply Nat.eq_of_testBit_eq
   intro i
   have ⟨k, hk⟩ := Nat.exists_eq_add_of_le hv; rw [hk]
-  rw [testBit_toNat, getLsbD_signExtend, Nat.pow_add, ← Nat.mul_sub_one,
-      Nat.add_comm (x.toNat), Nat.mul_assoc, Nat.testBit_mul_pow_two_add _ (x.isLt)]
-  by_cases h : i < w
-  · simp [h, Nat.lt_add_right k h, testBit_toNat]
-  · by_cases h2 : x.msb
-    <;> by_cases h1 : i < w + k
-    <;> simp [h2, h, h1, Nat.sub_lt_left_of_lt_add (Nat.le_of_not_lt h)]
-    exact Nat.le_sub_of_add_le (Nat.add_comm _ _ ▸ (Nat.le_of_not_lt h1))
+  rw [testBit_toNat, getLsbD_signExtend, Nat.pow_add, ← Nat.mul_sub_one, Nat.add_comm (x.toNat)]
+  by_cases hx : x.msb
+  · simp [hx, Nat.testBit_mul_pow_two_add _ x.isLt, testBit_toNat]
+    -- Case analysis on i being in the intervals [0..w), [w..w + k), [w+k..∞)
+    have hi : i < w ∨ (w ≤ i ∧ i < w + k) ∨ w + k ≤ i := by omega
+    rcases hi with hi | hi | hi
+    · simp [hi]; omega
+    · simp [hi]; omega
+    · simp [hi, show ¬ (i < w + k) by omega, show ¬ (i < w) by omega]
+      omega
+  · simp [hx, Nat.testBit_mul_pow_two_add _ x.isLt, testBit_toNat]
+    have hi : i < w ∨ (w ≤ i ∧ i < w + k) ∨ w + k ≤ i := by omega
+    rcases hi with hi | hi | hi
+    · simp [hi]; omega
+    · simp [hi]
+    · simp [hi, show ¬ (i < w + k) by omega, show ¬ (i < w) by omega, getLsbD_ge x i (by omega)]
 
+/-- Sign extending to a larger bitwidth depends on the msb.
+If the msb is false, then the result equals the original value.
+If the msb is true, then we add a value of `(2^v - 2^w)`, which arises from the sign extension. -/
 theorem toNat_signExtend (x : BitVec w) {v : Nat} :
-  (x.signExtend v).toNat = (x.setWidth v).toNat + (2 ^ v - 2 ^ w) * (if x.msb then 1 else 0) := by
+  (x.signExtend v).toNat = (x.setWidth v).toNat + if x.msb then 2 ^ v - 2 ^ w else 0 := by
   by_cases h : v ≤ w
-  · rw [signExtend_eq_setWidth_of_lt _ h, toNat_setWidth]
-    simp [Nat.sub_eq_zero_of_le (Nat.pow_le_pow_of_le_right Nat.two_pos 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_signExtend_of_gt _ (Nat.le_of_lt (Nat.lt_of_not_le h)), toNat_setWidth]
-    rw [Nat.mod_eq_of_lt (Nat.lt_of_lt_of_le x.isLt H)]
+  · have : 2^v ≤ 2^w := Nat.pow_le_pow_of_le_right Nat.two_pos h
+    simp [signExtend_eq_setWidth_of_lt x h, toNat_setWidth, Nat.sub_eq_zero_of_le this]
+  · have : 2^w ≤ 2^v := Nat.pow_le_pow_of_le_right Nat.two_pos (by omega)
+    rw [toNat_signExtend_of_le x (by omega), toNat_setWidth, Nat.mod_eq_of_lt (by omega)]
 
-theorem toInt_signExtend_of_gt (x : BitVec w) (hv : w < v):
+theorem toInt_signExtend_of_lt (x : BitVec w) (hv : w < v):
   (x.signExtend v).toInt = x.toInt := by
   simp only [toInt_eq_msb_cond, toNat_signExtend]
   have : (x.signExtend v).msb = x.msb := by
@@ -1577,7 +1589,6 @@ 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 -/
 
 theorem append_def (x : BitVec v) (y : BitVec w) :