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.
This commit is contained in:
Tobias Grosser
GitHub
parent
7c0b72e2c5
commit
e7e57d40c4
6 changed files with 218 additions and 37 deletions
|
|
@ -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)]
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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) ])
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue