From e7e57d40c4c5ee692a48a60a023327cc17c9bf83 Mon Sep 17 00:00:00 2001 From: Tobias Grosser Date: Tue, 11 Mar 2025 09:51:37 +0000 Subject: [PATCH] feat: add BitVec.[toNat|toFin|toInt]_[sshiftRight|sshiftRight'] (#7104) This PR adds `BitVec.[toNat|toFin|toInt]_[sshiftRight|sshiftRight']` plus variants with `of_msb_*`. While at it, we also add `toInt_zero_length` and `toInt_of_zero_length`. In support of our main theorem we add `toInt_shiftRight_lt` and `le_toInt_shiftRight`, which make the main theorem automatically derivable via omega. We also add four shift lemmas for `Int`: `le_shiftRight_of_nonpos`, `shiftRight_le_of_nonneg`, `le_shiftRight_of_nonneg`, `shiftRight_le_of_nonpos`, as well as `emod_eq_add_self_emod`, `ediv_nonpos_of_nonpos_of_neg `, and`bmod_eq_emod_of_lt `. For `Nat` we add `shiftRight_le`. Beyond the lemmas directly needed in the proof, we added a couple more to ensure the API is complete. We also fix the casing of `toFin_ushiftRight` and rename `lt_toInt` to `two_mul_lt_toInt` to avoid `'`-ed lemmas. --- src/Init/Data/BitVec/Bitblast.lean | 6 +- src/Init/Data/BitVec/Lemmas.lean | 153 +++++++++++++++++++++++--- src/Init/Data/Int/Bitwise/Lemmas.lean | 43 ++++++++ src/Init/Data/Int/DivMod/Lemmas.lean | 9 ++ src/Init/Data/Nat/Bitwise/Basic.lean | 4 + src/Init/Data/SInt/Lemmas.lean | 40 +++---- 6 files changed, 218 insertions(+), 37 deletions(-) diff --git a/src/Init/Data/BitVec/Bitblast.lean b/src/Init/Data/BitVec/Bitblast.lean index a3fc2de367..f670c9c888 100644 --- a/src/Init/Data/BitVec/Bitblast.lean +++ b/src/Init/Data/BitVec/Bitblast.lean @@ -504,7 +504,7 @@ theorem msb_neg {w : Nat} {x : BitVec w} : toInt_signExtend_of_le (by omega)] apply ne_of_apply_ne BitVec.toInt rw [toInt_signExtend_of_le (by omega), toInt_intMin_of_pos (by omega)] - have := b.le_toInt + have := b.le_two_mul_toInt have : -2 ^ w < -2 ^ v := by apply Int.neg_lt_neg norm_cast @@ -1288,8 +1288,8 @@ theorem saddOverflow_eq {w : Nat} (x y : BitVec w) : simp only [saddOverflow] rcases w with _|w · revert x y; decide - · have := le_toInt (x := x); have := toInt_lt (x := x) - have := le_toInt (x := y); have := toInt_lt (x := y) + · have := le_two_mul_toInt (x := x); have := two_mul_toInt_lt (x := x) + have := le_two_mul_toInt (x := y); have := two_mul_toInt_lt (x := y) simp only [← decide_or, msb_eq_toInt, decide_beq_decide, toInt_add, ← decide_not, ← decide_and, decide_eq_decide] rw_mod_cast [Int.bmod_neg_iff (by omega) (by omega)] diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean index 7773daecef..f2d084031f 100644 --- a/src/Init/Data/BitVec/Lemmas.lean +++ b/src/Init/Data/BitVec/Lemmas.lean @@ -15,6 +15,7 @@ import Init.Data.Nat.Div.Lemmas import Init.Data.Int.Bitwise.Lemmas import Init.Data.Int.LemmasAux import Init.Data.Int.Pow +import Init.Data.Int.LemmasAux set_option linter.missingDocs true @@ -240,12 +241,16 @@ theorem eq_of_getMsbD_eq {x y : BitVec w} theorem of_length_zero {x : BitVec 0} : x = 0#0 := by ext; simp [← getLsbD_eq_getElem] theorem toNat_zero_length (x : BitVec 0) : x.toNat = 0 := by simp [of_length_zero] +theorem toInt_zero_length (x : BitVec 0) : x.toInt = 0 := by simp [of_length_zero] + theorem getLsbD_zero_length (x : BitVec 0) : x.getLsbD i = false := by simp theorem getMsbD_zero_length (x : BitVec 0) : x.getMsbD i = false := by simp theorem msb_zero_length (x : BitVec 0) : x.msb = false := by simp [BitVec.msb, of_length_zero] theorem toNat_of_zero_length (h : w = 0) (x : BitVec w) : x.toNat = 0 := by subst h; simp [toNat_zero_length] +theorem toInt_of_zero_length (h : w = 0) (x : BitVec w) : x.toInt = 0 := by + subst h; simp [toInt_zero_length] theorem getLsbD_of_zero_length (h : w = 0) (x : BitVec w) : x.getLsbD i = false := by subst h; simp [getLsbD_zero_length] theorem getMsbD_of_zero_length (h : w = 0) (x : BitVec w) : x.getMsbD i = false := by @@ -559,6 +564,16 @@ theorem toInt_eq_toNat_bmod (x : BitVec n) : x.toInt = Int.bmod x.toNat (2^n) := rw [Int.bmod_neg] <;> simp only [←Int.ofNat_emod, toNat_mod_cancel] omega +theorem toInt_neg_of_msb_true {x : BitVec w} (h : x.msb = true) : x.toInt < 0 := by + simp only [BitVec.toInt] + have : 2 * x.toNat ≥ 2 ^ w := msb_eq_true_iff_two_mul_ge.mp h + omega + +theorem toInt_nonneg_of_msb_false {x : BitVec w} (h : x.msb = false) : 0 ≤ x.toInt := by + simp only [BitVec.toInt] + have : 2 * x.toNat < 2 ^ w := msb_eq_false_iff_two_mul_lt.mp h + omega + /-- Prove equality of bitvectors in terms of nat operations. -/ theorem eq_of_toInt_eq {x y : BitVec n} : x.toInt = y.toInt → x = y := by intro eq @@ -630,7 +645,7 @@ theorem toInt_zero {w : Nat} : (0#w).toInt = 0 := by `x.toInt` is less than `2^(w-1)`. We phrase the fact in terms of `2^w` to prevent a case split on `w=0` when the lemma is used. -/ -theorem toInt_lt {w : Nat} {x : BitVec w} : 2 * x.toInt < 2 ^ w := by +theorem two_mul_toInt_lt {w : Nat} {x : BitVec w} : 2 * x.toInt < 2 ^ w := by simp only [BitVec.toInt] rcases w with _|w' · omega @@ -638,26 +653,25 @@ theorem toInt_lt {w : Nat} {x : BitVec w} : 2 * x.toInt < 2 ^ w := by simp only [Nat.zero_lt_succ, Nat.mul_lt_mul_left, Int.natCast_mul, Int.Nat.cast_ofNat_Int] norm_cast; omega -theorem toInt_lt' {w : Nat} {x : BitVec w} : x.toInt < 2 ^ (w - 1) := by +theorem two_mul_toInt_le {w : Nat} {x : BitVec w} : 2 * x.toInt ≤ 2 ^ w - 1 := + Int.le_sub_one_of_lt two_mul_toInt_lt + +theorem toInt_lt {w : Nat} {x : BitVec w} : x.toInt < 2 ^ (w - 1) := by by_cases h : w = 0 · subst h - simp [BitVec.eq_nil x] - · have := toInt_lt (w := w) (x := x) - generalize x.toInt = x at * - rw [(show w = w - 1 + 1 by omega), Int.pow_succ] at this + simp [eq_nil x] + · have := @two_mul_toInt_lt w x + rw_mod_cast [← Nat.two_pow_pred_add_two_pow_pred (by omega), Int.mul_comm, Int.natCast_add] at this omega -theorem toInt_le {w : Nat} {x : BitVec w} : 2 * x.toInt ≤ 2 ^ w - 1 := +theorem toInt_le {w : Nat} {x : BitVec w} : x.toInt ≤ 2 ^ (w - 1) - 1 := Int.le_sub_one_of_lt toInt_lt -theorem toInt_le' {w : Nat} {x : BitVec w} : x.toInt ≤ 2 ^ (w - 1) - 1 := by - exact Int.le_sub_one_of_lt (toInt_lt') - /-- `x.toInt` is greater than or equal to `-2^(w-1)`. We phrase the fact in terms of `2^w` to prevent a case split on `w=0` when the lemma is used. -/ -theorem le_toInt {w : Nat} {x : BitVec w} : -2 ^ w ≤ 2 * x.toInt := by +theorem le_two_mul_toInt {w : Nat} {x : BitVec w} : -2 ^ w ≤ 2 * x.toInt := by simp only [BitVec.toInt] rcases w with _|w' · omega @@ -665,11 +679,12 @@ theorem le_toInt {w : Nat} {x : BitVec w} : -2 ^ w ≤ 2 * x.toInt := by simp only [Nat.zero_lt_succ, Nat.mul_lt_mul_left, Int.natCast_mul, Int.Nat.cast_ofNat_Int] norm_cast; omega -theorem le_toInt' {w : Nat} (x : BitVec w) : -2 ^ (w - 1) ≤ x.toInt := by + +theorem le_toInt {w : Nat} (x : BitVec w) : -2 ^ (w - 1) ≤ x.toInt := by by_cases h : w = 0 · subst h simp [BitVec.eq_nil x] - · have := le_toInt (w := w) (x := x) + · have := le_two_mul_toInt (w := w) (x := x) generalize x.toInt = x at * rw [(show w = w - 1 + 1 by omega), Int.pow_succ] at this omega @@ -1806,7 +1821,7 @@ theorem toInt_ushiftRight {x : BitVec w} {n : Nat} : simp [hn] @[simp] -theorem toFin_uShiftRight {x : BitVec w} {n : Nat} : +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 @@ -2012,11 +2027,118 @@ theorem getMsbD_sshiftRight {x : BitVec w} {i n : Nat} : by_cases h₄ : n + (w - 1 - i) < w <;> (simp only [h₄, ↓reduceIte]; congr; omega) · simp [h] +theorem toInt_shiftRight_lt {x : BitVec w} {n : Nat} : + x.toInt >>> n < 2 ^ (w - 1) := by + have := @Int.shiftRight_le_of_nonneg x.toInt n + have := @Int.shiftRight_le_of_nonpos x.toInt n + have := @BitVec.toInt_lt w x + have := @Nat.one_le_two_pow (w-1) + norm_cast at * + omega + +theorem le_toInt_shiftRight {x : BitVec w} {n : Nat} : + -(2 ^ (w - 1)) ≤ x.toInt >>> n := by + have := @Int.le_shiftRight_of_nonpos x.toInt n + have := @Int.le_shiftRight_of_nonneg x.toInt n + have := @BitVec.le_toInt w x + have := @Nat.one_le_two_pow (w-1) + norm_cast at * + omega + +theorem toNat_sshiftRight_of_msb_true {x : BitVec w} {n : Nat} (h : x.msb = true) : + (x.sshiftRight n).toNat = 2 ^ w - 1 - (2 ^ w - 1 - x.toNat) >>> n := by + simp [sshiftRight_eq_of_msb_true, h] + +theorem toNat_sshiftRight_of_msb_false {x : BitVec w} {n : Nat} (h : x.msb = false) : + (x.sshiftRight n).toNat = x.toNat >>> n := by + simp [sshiftRight_eq_of_msb_false, h] + +theorem toNat_sshiftRight {x : BitVec w} {n : Nat} : + (x.sshiftRight n).toNat = + if x.msb + then 2 ^ w - 1 - (2 ^ w - 1 - x.toNat) >>> n + else x.toNat >>> n := by + by_cases h : x.msb + · simp [toNat_sshiftRight_of_msb_true, h] + · rw [Bool.not_eq_true] at h + simp [toNat_sshiftRight_of_msb_false, h] + +theorem toFin_sshiftRight_of_msb_true {x : BitVec w} {n : Nat} (h : x.msb = true) : + (x.sshiftRight n).toFin = Fin.ofNat' (2^w) (2 ^ w - 1 - (2 ^ w - 1 - x.toNat) >>> n) := by + apply Fin.eq_of_val_eq + simp only [val_toFin, toNat_sshiftRight, h, ↓reduceIte, Fin.val_ofNat'] + rw [Nat.mod_eq_of_lt] + have := x.isLt + have ineq : ∀ y, 2 ^ w - 1 - y < 2 ^ w := by omega + exact ineq ((2 ^ w - 1 - x.toNat) >>> n) + +theorem toFin_sshiftRight_of_msb_false {x : BitVec w} {n : Nat} (h : x.msb = false) : + (x.sshiftRight n).toFin = Fin.ofNat' (2^w) (x.toNat >>> n) := by + apply Fin.eq_of_val_eq + simp only [val_toFin, toNat_sshiftRight, h, Bool.false_eq_true, ↓reduceIte, Fin.val_ofNat'] + have := Nat.shiftRight_le x.toNat n + rw [Nat.mod_eq_of_lt (by omega)] + +theorem toFin_sshiftRight {x : BitVec w} {n : Nat} : + (x.sshiftRight n).toFin = + if x.msb + then Fin.ofNat' (2^w) (2 ^ w - 1 - (2 ^ w - 1 - x.toNat) >>> n) + else Fin.ofNat' (2^w) (x.toNat >>> n) := by + by_cases h : x.msb + · simp [toFin_sshiftRight_of_msb_true, h] + · simp [toFin_sshiftRight_of_msb_false, h] + +@[simp] +theorem toInt_sshiftRight {x : BitVec w} {n : Nat} : + (x.sshiftRight n).toInt = x.toInt >>> n := by + by_cases h : w = 0 + · subst h + simp [BitVec.eq_nil x] + · rw [sshiftRight, toInt_ofInt, ←Nat.two_pow_pred_add_two_pow_pred (by omega)] + have := @toInt_shiftRight_lt w x n + have := @le_toInt_shiftRight w x n + norm_cast at * + exact Int.bmod_eq_self_of_le (by omega) (by omega) + /-! ### sshiftRight reductions from BitVec to Nat -/ @[simp] theorem sshiftRight_eq' (x : BitVec w) : x.sshiftRight' y = x.sshiftRight y.toNat := rfl +theorem toNat_sshiftRight'_of_msb_true {x y : BitVec w} (h : x.msb = true) : + (x.sshiftRight' y).toNat = 2 ^ w - 1 - (2 ^ w - 1 - x.toNat) >>> y.toNat := by + rw [sshiftRight_eq', toNat_sshiftRight_of_msb_true h] + +theorem toNat_sshiftRight'_of_msb_false {x y : BitVec w} (h : x.msb = false) : + (x.sshiftRight' y).toNat = x.toNat >>> y.toNat := by + rw [sshiftRight_eq', toNat_sshiftRight_of_msb_false h] + +theorem toNat_sshiftRight' {x y : BitVec w} : + (x.sshiftRight' y).toNat = + if x.msb + then 2 ^ w - 1 - (2 ^ w - 1 - x.toNat) >>> y.toNat + else x.toNat >>> y.toNat := by + rw [sshiftRight_eq', toNat_sshiftRight] + +theorem toFin_sshiftRight'_of_msb_true {x y : BitVec w} (h : x.msb = true) : + (x.sshiftRight' y).toFin = Fin.ofNat' (2^w) (2 ^ w - 1 - (2 ^ w - 1 - x.toNat) >>> y.toNat) := by + rw [sshiftRight_eq', toFin_sshiftRight_of_msb_true h] + +theorem toFin_sshiftRight'_of_msb_false {x y : BitVec w} (h : x.msb = false) : + (x.sshiftRight' y).toFin = Fin.ofNat' (2^w) (x.toNat >>> y.toNat) := by + rw [sshiftRight_eq', toFin_sshiftRight_of_msb_false h] + +theorem toFin_sshiftRight' {x y : BitVec w} : + (x.sshiftRight' y).toFin = + if x.msb + then Fin.ofNat' (2^w) (2 ^ w - 1 - (2 ^ w - 1 - x.toNat) >>> y.toNat) + else Fin.ofNat' (2^w) (x.toNat >>> y.toNat) := by + rw [sshiftRight_eq', toFin_sshiftRight] + +theorem toInt_sshiftRight' {x y : BitVec w} : + (x.sshiftRight' y).toInt = x.toInt >>> y.toNat := by + rw [sshiftRight_eq', toInt_sshiftRight] + -- This should not be a `@[simp]` lemma as the left hand side is not in simp normal form. theorem getLsbD_sshiftRight' {x y : BitVec w} {i : Nat} : getLsbD (x.sshiftRight' y) i = @@ -4446,6 +4568,9 @@ instance instDecidableExistsBitVec : set_option linter.missingDocs false +@[deprecated toFin_uShiftRight (since := "2025-02-18")] +abbrev toFin_uShiftRight := @toFin_ushiftRight + @[deprecated signExtend_eq_setWidth_of_msb_false (since := "2024-12-08")] abbrev signExtend_eq_not_setWidth_not_of_msb_false := @signExtend_eq_setWidth_of_msb_false diff --git a/src/Init/Data/Int/Bitwise/Lemmas.lean b/src/Init/Data/Int/Bitwise/Lemmas.lean index 14d8b3dcd2..41d2cc1f0f 100644 --- a/src/Init/Data/Int/Bitwise/Lemmas.lean +++ b/src/Init/Data/Int/Bitwise/Lemmas.lean @@ -39,4 +39,47 @@ theorem zero_shiftRight (n : Nat) : (0 : Int) >>> n = 0 := by theorem shiftRight_zero (n : Int) : n >>> 0 = n := by simp [Int.shiftRight_eq_div_pow] +theorem le_shiftRight_of_nonpos {n : Int} {s : Nat} (h : n ≤ 0) : n ≤ n >>> s := by + simp only [Int.shiftRight_eq, Int.shiftRight, Int.ofNat_eq_coe] + split + case _ _ _ m => + simp only [ofNat_eq_coe] at h + by_cases hm : m = 0 + · simp [hm] + · omega + case _ _ _ m => + by_cases hm : m = 0 + · simp [hm] + · have := Nat.shiftRight_le m s + omega + +theorem shiftRight_le_of_nonneg {n : Int} {s : Nat} (h : 0 ≤ n) : n >>> s ≤ n := by + simp only [Int.shiftRight_eq, Int.shiftRight, Int.ofNat_eq_coe] + split + case _ _ _ m => + simp only [Int.ofNat_eq_coe] at h + by_cases hm : m = 0 + · simp [hm] + · have := Nat.shiftRight_le m s + simp + omega + case _ _ _ m => + omega + +theorem le_shiftRight_of_nonneg {n : Int} {s : Nat} (h : 0 ≤ n) : 0 ≤ (n >>> s) := by + rw [Int.shiftRight_eq_div_pow] + by_cases h' : s = 0 + · simp [h', h] + · have := @Nat.pow_pos 2 s (by omega) + have := @Int.ediv_nonneg n (2^s) h (by norm_cast at *; omega) + norm_cast at * + +theorem shiftRight_le_of_nonpos {n : Int} {s : Nat} (h : n ≤ 0) : (n >>> s) ≤ 0 := by + rw [Int.shiftRight_eq_div_pow] + by_cases h' : s = 0 + · simp [h', h] + · have : 1 < 2 ^ s := Nat.one_lt_two_pow (by omega) + have rl : n / 2 ^ s ≤ 0 := Int.ediv_nonpos_of_nonpos_of_neg (by omega) (by norm_cast at *; omega) + norm_cast at * + end Int diff --git a/src/Init/Data/Int/DivMod/Lemmas.lean b/src/Init/Data/Int/DivMod/Lemmas.lean index 308e27cce7..0ff1722cbd 100644 --- a/src/Init/Data/Int/DivMod/Lemmas.lean +++ b/src/Init/Data/Int/DivMod/Lemmas.lean @@ -608,6 +608,9 @@ theorem ofNat_mod_ofNat (m n : Nat) : (m % n : Int) = ↑(m % n) := rfl theorem neg_emod_eq_sub_emod {a b : Int} : -a % b = (b - a) % b := by rw [← add_emod_self_left]; rfl +theorem emod_eq_add_self_emod {a b : Int} : a % b = (a + b) % b := + Int.add_emod_self.symm + @[simp] theorem emod_neg (a b : Int) : a % -b = a % b := by rw [emod_def, emod_def, Int.ediv_neg, Int.neg_mul_neg] @@ -909,6 +912,9 @@ theorem le_of_mul_le_mul_right {a b c : Int} (w : b * a ≤ c * a) (h : 0 < a) : protected theorem ediv_le_of_le_mul {a b c : Int} (H : 0 < c) (H' : a ≤ b * c) : a / c ≤ b := le_of_mul_le_mul_right (Int.le_trans (Int.ediv_mul_le _ (Int.ne_of_gt H)) H') H +protected theorem ediv_nonpos_of_nonpos_of_neg {n s : Int} (h : n ≤ 0) (h2 : 0 < s) : n / s ≤ 0 := + Int.ediv_le_of_le_mul h2 (by simp [h]) + protected theorem mul_lt_of_lt_ediv {a b c : Int} (H : 0 < c) (H3 : a < b / c) : a * c < b := Int.lt_of_not_ge <| mt (Int.ediv_le_of_le_mul H) (Int.not_le_of_gt H3) @@ -2263,6 +2269,9 @@ theorem bmod_lt {x : Int} {m : Nat} (h : 0 < m) : bmod x m < (m + 1) / 2 := by exact Int.sub_neg_of_lt this · exact Int.le.intro_sub _ rfl +theorem bmod_eq_emod_of_lt {x : Int} {m : Nat} (hx : x % m < (m + 1) / 2) : bmod x m = x % m := by + simp [bmod, hx] + theorem bmod_le {x : Int} {m : Nat} (h : 0 < m) : bmod x m ≤ (m - 1) / 2 := by refine lt_add_one_iff.mp ?_ calc diff --git a/src/Init/Data/Nat/Bitwise/Basic.lean b/src/Init/Data/Nat/Bitwise/Basic.lean index dde8c26247..6de9522410 100644 --- a/src/Init/Data/Nat/Bitwise/Basic.lean +++ b/src/Init/Data/Nat/Bitwise/Basic.lean @@ -74,6 +74,10 @@ theorem shiftRight_eq_div_pow (m : Nat) : ∀ n, m >>> n = m / 2 ^ n theorem shiftRight_eq_zero (m n : Nat) (hn : m < 2^n) : m >>> n = 0 := by simp [Nat.shiftRight_eq_div_pow, Nat.div_eq_of_lt hn] +theorem shiftRight_le (m n : Nat) : m >>> n ≤ m := by + simp only [shiftRight_eq_div_pow] + apply Nat.div_le_self + /-! ### testBit We define an operation for testing individual bits in the binary representation diff --git a/src/Init/Data/SInt/Lemmas.lean b/src/Init/Data/SInt/Lemmas.lean index abcf39f073..ae9cb28fe7 100644 --- a/src/Init/Data/SInt/Lemmas.lean +++ b/src/Init/Data/SInt/Lemmas.lean @@ -268,14 +268,14 @@ theorem Int64.toInt_maxValue : Int64.maxValue.toInt = 2 ^ 63 - 1 := rfl @[simp] theorem ISize.toBitVec_toInt32 (x : ISize) : x.toInt32.toBitVec = x.toBitVec.signExtend 32 := rfl @[simp] theorem ISize.toBitVec_toInt64 (x : ISize) : x.toInt64.toBitVec = x.toBitVec.signExtend 64 := rfl -theorem Int8.toInt_lt (x : Int8) : x.toInt < 2 ^ 7 := Int.lt_of_mul_lt_mul_left BitVec.toInt_lt (by decide) -theorem Int8.le_toInt (x : Int8) : -2 ^ 7 ≤ x.toInt := Int.le_of_mul_le_mul_left BitVec.le_toInt (by decide) -theorem Int16.toInt_lt (x : Int16) : x.toInt < 2 ^ 15 := Int.lt_of_mul_lt_mul_left BitVec.toInt_lt (by decide) -theorem Int16.le_toInt (x : Int16) : -2 ^ 15 ≤ x.toInt := Int.le_of_mul_le_mul_left BitVec.le_toInt (by decide) -theorem Int32.toInt_lt (x : Int32) : x.toInt < 2 ^ 31 := Int.lt_of_mul_lt_mul_left BitVec.toInt_lt (by decide) -theorem Int32.le_toInt (x : Int32) : -2 ^ 31 ≤ x.toInt := Int.le_of_mul_le_mul_left BitVec.le_toInt (by decide) -theorem Int64.toInt_lt (x : Int64) : x.toInt < 2 ^ 63 := Int.lt_of_mul_lt_mul_left BitVec.toInt_lt (by decide) -theorem Int64.le_toInt (x : Int64) : -2 ^ 63 ≤ x.toInt := Int.le_of_mul_le_mul_left BitVec.le_toInt (by decide) +theorem Int8.toInt_lt (x : Int8) : x.toInt < 2 ^ 7 := Int.lt_of_mul_lt_mul_left BitVec.two_mul_toInt_lt (by decide) +theorem Int8.le_toInt (x : Int8) : -2 ^ 7 ≤ x.toInt := Int.le_of_mul_le_mul_left BitVec.le_two_mul_toInt (by decide) +theorem Int16.toInt_lt (x : Int16) : x.toInt < 2 ^ 15 := Int.lt_of_mul_lt_mul_left BitVec.two_mul_toInt_lt (by decide) +theorem Int16.le_toInt (x : Int16) : -2 ^ 15 ≤ x.toInt := Int.le_of_mul_le_mul_left BitVec.le_two_mul_toInt (by decide) +theorem Int32.toInt_lt (x : Int32) : x.toInt < 2 ^ 31 := Int.lt_of_mul_lt_mul_left BitVec.two_mul_toInt_lt (by decide) +theorem Int32.le_toInt (x : Int32) : -2 ^ 31 ≤ x.toInt := Int.le_of_mul_le_mul_left BitVec.le_two_mul_toInt (by decide) +theorem Int64.toInt_lt (x : Int64) : x.toInt < 2 ^ 63 := Int.lt_of_mul_lt_mul_left BitVec.two_mul_toInt_lt (by decide) +theorem Int64.le_toInt (x : Int64) : -2 ^ 63 ≤ x.toInt := Int.le_of_mul_le_mul_left BitVec.le_two_mul_toInt (by decide) theorem ISize.toInt_lt_two_pow_numBits (x : ISize) : x.toInt < 2 ^ (System.Platform.numBits - 1) := by have := x.toBitVec.toInt_lt; cases System.Platform.numBits_eq <;> simp_all <;> omega theorem ISize.two_pow_numBits_le_toInt (x : ISize) : -2 ^ (System.Platform.numBits - 1) ≤ x.toInt := by @@ -1408,20 +1408,20 @@ theorem ISize.toInt64_ofIntLE {n : Int} (h₁ h₂) : ISize.toInt64_ofNat' (by rw [toInt_maxValue]; cases System.Platform.numBits_eq <;> simp_all <;> omega) @[simp] theorem Int8.ofIntLE_bitVecToInt (n : BitVec 8) : - Int8.ofIntLE n.toInt (n.le_toInt') (n.toInt_le') = Int8.ofBitVec n := + Int8.ofIntLE n.toInt n.le_toInt n.toInt_le = Int8.ofBitVec n := Int8.toBitVec.inj (by simp) @[simp] theorem Int16.ofIntLE_bitVecToInt (n : BitVec 16) : - Int16.ofIntLE n.toInt (n.le_toInt') (n.toInt_le') = Int16.ofBitVec n := + Int16.ofIntLE n.toInt n.le_toInt n.toInt_le = Int16.ofBitVec n := Int16.toBitVec.inj (by simp) @[simp] theorem Int32.ofIntLE_bitVecToInt (n : BitVec 32) : - Int32.ofIntLE n.toInt (n.le_toInt') (n.toInt_le') = Int32.ofBitVec n := + Int32.ofIntLE n.toInt n.le_toInt n.toInt_le = Int32.ofBitVec n := Int32.toBitVec.inj (by simp) @[simp] theorem Int64.ofIntLE_bitVecToInt (n : BitVec 64) : - Int64.ofIntLE n.toInt (n.le_toInt') (n.toInt_le') = Int64.ofBitVec n := + Int64.ofIntLE n.toInt n.le_toInt n.toInt_le = Int64.ofBitVec n := Int64.toBitVec.inj (by simp) @[simp] theorem ISize.ofIntLE_bitVecToInt (n : BitVec System.Platform.numBits) : - ISize.ofIntLE n.toInt (toInt_minValue ▸ n.le_toInt') - (toInt_maxValue ▸ n.toInt_le') = ISize.ofBitVec n := + ISize.ofIntLE n.toInt (toInt_minValue ▸ n.le_toInt) + (toInt_maxValue ▸ n.toInt_le) = ISize.ofBitVec n := ISize.toBitVec.inj (by simp) theorem Int8.ofBitVec_ofNatLT (n : Nat) (hn) : Int8.ofBitVec (BitVec.ofNatLT n hn) = Int8.ofNat n := @@ -1470,13 +1470,13 @@ theorem ISize.ofBitVec_ofNatLT (n : Nat) (hn) : ISize.ofBitVec (BitVec.ofNatLT n ISize.toBitVec.inj (by simp) @[simp] theorem Int8.ofIntTruncate_bitVecToInt (n : BitVec 8) : Int8.ofIntTruncate n.toInt = Int8.ofBitVec n := - Int8.toBitVec.inj (by simp [toBitVec_ofIntTruncate (n.le_toInt') (n.toInt_le')]) + Int8.toBitVec.inj (by simp [toBitVec_ofIntTruncate (n.le_toInt) (n.toInt_le)]) @[simp] theorem Int16.ofIntTruncate_bitVecToInt (n : BitVec 16) : Int16.ofIntTruncate n.toInt = Int16.ofBitVec n := - Int16.toBitVec.inj (by simp [toBitVec_ofIntTruncate (n.le_toInt') (n.toInt_le')]) + Int16.toBitVec.inj (by simp [toBitVec_ofIntTruncate (n.le_toInt) (n.toInt_le)]) @[simp] theorem Int32.ofIntTruncate_bitVecToInt (n : BitVec 32) : Int32.ofIntTruncate n.toInt = Int32.ofBitVec n := - Int32.toBitVec.inj (by simp [toBitVec_ofIntTruncate (n.le_toInt') (n.toInt_le')]) + Int32.toBitVec.inj (by simp [toBitVec_ofIntTruncate (n.le_toInt) (n.toInt_le)]) @[simp] theorem Int64.ofIntTruncate_bitVecToInt (n : BitVec 64) : Int64.ofIntTruncate n.toInt = Int64.ofBitVec n := - Int64.toBitVec.inj (by simp [toBitVec_ofIntTruncate (n.le_toInt') (n.toInt_le')]) + Int64.toBitVec.inj (by simp [toBitVec_ofIntTruncate (n.le_toInt) (n.toInt_le)]) @[simp] theorem ISize.ofIntTruncate_bitVecToInt (n : BitVec System.Platform.numBits) : ISize.ofIntTruncate n.toInt = ISize.ofBitVec n := - ISize.toBitVec.inj (by simp [toBitVec_ofIntTruncate (toInt_minValue ▸ n.le_toInt') - (toInt_maxValue ▸ n.toInt_le') ]) + ISize.toBitVec.inj (by simp [toBitVec_ofIntTruncate (toInt_minValue ▸ n.le_toInt) + (toInt_maxValue ▸ n.toInt_le) ])