From 6961c85c79a710bda70e3744de693b74ec1ecf0a Mon Sep 17 00:00:00 2001 From: Siddharth Bhat Date: Mon, 11 Nov 2024 10:52:37 +0000 Subject: [PATCH] chore: pass on implementation --- src/Init/Data/BitVec/Lemmas.lean | 53 +++++++++++++++++++------------- 1 file changed, 32 insertions(+), 21 deletions(-) diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean index 1361d2453d55..51d591f591f7 100644 --- a/src/Init/Data/BitVec/Lemmas.lean +++ b/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) :