feat: finite type conversions (Nat/Int/Fin/BitVec -> IntX -> *) (#7368)
This PR adds lemmas for iterated conversions between finite types, starting with something of type `Nat`/`Int`/`Fin`/`BitVec` and going through `IntX`.
This commit is contained in:
Markus Himmel
GitHub
parent
84c7e5db1f
commit
7bfa8f6296
7 changed files with 731 additions and 28 deletions
|
|
@ -483,6 +483,36 @@ theorem msb_neg {w : Nat} {x : BitVec w} :
|
|||
case zero => exact hmsb
|
||||
case succ => exact getMsbD_x _ hi (by omega)
|
||||
|
||||
/-- This is false if `v < w` and `b = intMin`. See also `signExtend_neg_of_ne_intMin`. -/
|
||||
@[simp] theorem signExtend_neg_of_le {v w : Nat} (h : w ≤ v) (b : BitVec v) :
|
||||
(-b).signExtend w = -b.signExtend w := by
|
||||
apply BitVec.eq_of_getElem_eq
|
||||
intro i hi
|
||||
simp only [getElem_signExtend, getElem_neg]
|
||||
rw [dif_pos (by omega), dif_pos (by omega)]
|
||||
simp only [getLsbD_signExtend, Bool.and_eq_true, decide_eq_true_eq, Bool.ite_eq_true_distrib,
|
||||
Bool.bne_right_inj, decide_eq_decide]
|
||||
exact ⟨fun ⟨j, hj₁, hj₂⟩ => ⟨j, ⟨hj₁, ⟨by omega, by rwa [if_pos (by omega)]⟩⟩⟩,
|
||||
fun ⟨j, hj₁, hj₂, hj₃⟩ => ⟨j, hj₁, by rwa [if_pos (by omega)] at hj₃⟩⟩
|
||||
|
||||
/-- This is false if `v < w` and `b = intMin`. See also `signExtend_neg_of_le`. -/
|
||||
@[simp] theorem signExtend_neg_of_ne_intMin {v w : Nat} (b : BitVec v) (hb : b ≠ intMin v) :
|
||||
(-b).signExtend w = -b.signExtend w := by
|
||||
refine (by omega : w ≤ v ∨ v < w).elim (fun h => signExtend_neg_of_le h b) (fun h => ?_)
|
||||
apply BitVec.eq_of_toInt_eq
|
||||
rw [toInt_signExtend_of_le (by omega), toInt_neg_of_ne_intMin hb, toInt_neg_of_ne_intMin,
|
||||
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 : -2 ^ w < -2 ^ v := by
|
||||
apply Int.neg_lt_neg
|
||||
norm_cast
|
||||
rwa [Nat.pow_lt_pow_iff_right (by omega)]
|
||||
have : 2 * b.toInt ≠ -2 ^ w := by omega
|
||||
rw [(show w = w - 1 + 1 by omega), Int.pow_succ] at this
|
||||
omega
|
||||
|
||||
/-! ### abs -/
|
||||
|
||||
theorem msb_abs {w : Nat} {x : BitVec w} :
|
||||
|
|
|
|||
|
|
@ -2064,14 +2064,18 @@ theorem msb_signExtend {x : BitVec w} :
|
|||
· simp [h, BitVec.msb, getMsbD_signExtend, show ¬ (v - w = 0) by omega]
|
||||
|
||||
/-- Sign extending to a width smaller than the starting width is a truncation. -/
|
||||
theorem signExtend_eq_setWidth_of_lt (x : BitVec w) {v : Nat} (hv : v ≤ w):
|
||||
theorem signExtend_eq_setWidth_of_le (x : BitVec w) {v : Nat} (hv : v ≤ w) :
|
||||
x.signExtend v = x.setWidth v := by
|
||||
ext i h
|
||||
simp [getElem_signExtend, show i < w by omega]
|
||||
|
||||
@[deprecated signExtend_eq_setWidth_of_le (since := "2025-03-07")]
|
||||
theorem signExtend_eq_setWidth_of_lt (x : BitVec w) {v : Nat} (hv : v ≤ w) :
|
||||
x.signExtend v = x.setWidth v := signExtend_eq_setWidth_of_le x hv
|
||||
|
||||
/-- Sign extending to the same bitwidth is a no op. -/
|
||||
@[simp] theorem signExtend_eq (x : BitVec w) : x.signExtend w = x := by
|
||||
rw [signExtend_eq_setWidth_of_lt _ (Nat.le_refl _), setWidth_eq]
|
||||
rw [signExtend_eq_setWidth_of_le _ (Nat.le_refl _), setWidth_eq]
|
||||
|
||||
/-- Sign extending to a larger bitwidth depends on the msb.
|
||||
If the msb is false, then the result equals the original value.
|
||||
|
|
@ -2108,7 +2112,7 @@ theorem toNat_signExtend (x : BitVec w) {v : Nat} :
|
|||
(x.signExtend v).toNat = (x.setWidth v).toNat + if x.msb then 2^v - 2^w else 0 := by
|
||||
by_cases h : v ≤ w
|
||||
· have : 2^v ≤ 2^w := Nat.pow_le_pow_right Nat.two_pos h
|
||||
simp [signExtend_eq_setWidth_of_lt x h, toNat_setWidth, Nat.sub_eq_zero_of_le this]
|
||||
simp [signExtend_eq_setWidth_of_le x h, toNat_setWidth, Nat.sub_eq_zero_of_le this]
|
||||
· have : 2^w ≤ 2^v := Nat.pow_le_pow_right Nat.two_pos (by omega)
|
||||
rw [toNat_signExtend_of_le x (by omega), toNat_setWidth, Nat.mod_eq_of_lt (by omega)]
|
||||
|
||||
|
|
@ -2144,7 +2148,7 @@ and we compute a modulo by `2^v`.
|
|||
-/
|
||||
theorem toInt_signExtend_eq_toNat_bmod_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]
|
||||
simp [signExtend_eq_setWidth_of_le _ hv]
|
||||
|
||||
/--
|
||||
Interpreting the sign extension of `(x : BitVec w)` to width `v`
|
||||
|
|
@ -2168,8 +2172,6 @@ theorem toInt_signExtend_eq_toInt_bmod_of_le (x : BitVec w) (h : v ≤ w) :
|
|||
(x.signExtend v).toInt = x.toInt.bmod (2 ^ v) := by
|
||||
rw [BitVec.toInt_signExtend, Nat.min_eq_left h]
|
||||
|
||||
attribute [simp] BitVec.signExtend_eq
|
||||
|
||||
/-! ### append -/
|
||||
|
||||
theorem append_def (x : BitVec v) (y : BitVec w) :
|
||||
|
|
@ -4002,7 +4004,6 @@ theorem toNat_intMin : (intMin w).toNat = 2 ^ (w - 1) % 2 ^ w := by
|
|||
/--
|
||||
The RHS is zero in case `w = 0` which is modeled by wrapping the expression in `... % 2 ^ w`.
|
||||
-/
|
||||
@[simp]
|
||||
theorem toInt_intMin {w : Nat} :
|
||||
(intMin w).toInt = -((2 ^ (w - 1) % 2 ^ w) : Nat) := by
|
||||
by_cases h : w = 0
|
||||
|
|
@ -4014,10 +4015,16 @@ theorem toInt_intMin {w : Nat} :
|
|||
rw [Nat.mul_comm]
|
||||
simp [w_pos]
|
||||
|
||||
theorem toInt_intMin_of_pos {v : Nat} (hv : 0 < v) : (intMin v).toInt = -2 ^ (v - 1) := by
|
||||
rw [toInt_intMin, Nat.mod_eq_of_lt]
|
||||
· simp [Int.natCast_pow]
|
||||
· rw [Nat.pow_lt_pow_iff_right (by omega)]
|
||||
omega
|
||||
|
||||
theorem toInt_intMin_le (x : BitVec w) :
|
||||
(intMin w).toInt ≤ x.toInt := by
|
||||
cases w
|
||||
case zero => simp [@of_length_zero x]
|
||||
case zero => simp [toInt_intMin, @of_length_zero x]
|
||||
case succ w =>
|
||||
simp only [toInt_intMin, Nat.add_one_sub_one, Int.ofNat_emod]
|
||||
have : 0 < 2 ^ w := Nat.two_pow_pos w
|
||||
|
|
@ -4508,7 +4515,7 @@ abbrev signExtend_eq_not_zeroExtend_not_of_msb_false := @signExtend_eq_setWidth
|
|||
abbrev signExtend_eq_not_zeroExtend_not_of_msb_true := @signExtend_eq_not_setWidth_not_of_msb_true
|
||||
|
||||
@[deprecated signExtend_eq_setWidth_of_lt (since := "2024-09-18")]
|
||||
abbrev signExtend_eq_truncate_of_lt := @signExtend_eq_setWidth_of_lt
|
||||
abbrev signExtend_eq_truncate_of_lt := @signExtend_eq_setWidth_of_le
|
||||
|
||||
@[deprecated truncate_append (since := "2024-09-18")]
|
||||
abbrev truncate_append := @setWidth_append
|
||||
|
|
|
|||
|
|
@ -8,6 +8,7 @@ import Init.Data.SInt.Basic
|
|||
import Init.Data.BitVec.Bitblast
|
||||
import Init.Data.Int.LemmasAux
|
||||
import Init.Data.UInt.Lemmas
|
||||
import Init.System.Platform
|
||||
|
||||
open Lean in
|
||||
set_option hygiene false in
|
||||
|
|
@ -71,15 +72,26 @@ theorem ISize.toNat_toBitVec_ofNat_of_lt {n : Nat} (h : n < 2^32) :
|
|||
(ofNat n).toBitVec.toNat = n :=
|
||||
Nat.mod_eq_of_lt (Nat.lt_of_lt_of_le h (by cases USize.size_eq <;> simp_all +decide))
|
||||
|
||||
theorem Int8.toInt_ofInt {n : Int} (hn : -2^7 ≤ n) (hn' : n < 2^7) : toInt (ofInt n) = n := by
|
||||
@[simp] theorem Int8.toInt_ofInt {n : Int} : toInt (ofInt n) = n.bmod Int8.size := by
|
||||
rw [toInt, toBitVec_ofInt, BitVec.toInt_ofInt]
|
||||
@[simp] theorem Int16.toInt_ofInt {n : Int} : toInt (ofInt n) = n.bmod Int16.size := by
|
||||
rw [toInt, toBitVec_ofInt, BitVec.toInt_ofInt]
|
||||
@[simp] theorem Int32.toInt_ofInt {n : Int} : toInt (ofInt n) = n.bmod Int32.size := by
|
||||
rw [toInt, toBitVec_ofInt, BitVec.toInt_ofInt]
|
||||
@[simp] theorem Int64.toInt_ofInt {n : Int} : toInt (ofInt n) = n.bmod Int64.size := by
|
||||
rw [toInt, toBitVec_ofInt, BitVec.toInt_ofInt]
|
||||
theorem ISize.toInt_ofInt {n : Int} : toInt (ofInt n) = n.bmod ISize.size := by
|
||||
rw [toInt, toBitVec_ofInt, BitVec.toInt_ofInt]
|
||||
|
||||
theorem Int8.toInt_ofInt_of_le {n : Int} (hn : -2^7 ≤ n) (hn' : n < 2^7) : toInt (ofInt n) = n := by
|
||||
rw [toInt, toBitVec_ofInt, BitVec.toInt_ofInt_eq_self (by decide) hn hn']
|
||||
theorem Int16.toInt_ofInt {n : Int} (hn : -2^15 ≤ n) (hn' : n < 2^15) : toInt (ofInt n) = n := by
|
||||
theorem Int16.toInt_ofInt_of_le {n : Int} (hn : -2^15 ≤ n) (hn' : n < 2^15) : toInt (ofInt n) = n := by
|
||||
rw [toInt, toBitVec_ofInt, BitVec.toInt_ofInt_eq_self (by decide) hn hn']
|
||||
theorem Int32.toInt_ofInt {n : Int} (hn : -2^31 ≤ n) (hn' : n < 2^31) : toInt (ofInt n) = n := by
|
||||
theorem Int32.toInt_ofInt_of_le {n : Int} (hn : -2^31 ≤ n) (hn' : n < 2^31) : toInt (ofInt n) = n := by
|
||||
rw [toInt, toBitVec_ofInt, BitVec.toInt_ofInt_eq_self (by decide) hn hn']
|
||||
theorem Int64.toInt_ofInt {n : Int} (hn : -2^63 ≤ n) (hn' : n < 2^63) : toInt (ofInt n) = n := by
|
||||
theorem Int64.toInt_ofInt_of_le {n : Int} (hn : -2^63 ≤ n) (hn' : n < 2^63) : toInt (ofInt n) = n := by
|
||||
rw [toInt, toBitVec_ofInt, BitVec.toInt_ofInt_eq_self (by decide) hn hn']
|
||||
theorem ISize.toInt_ofInt {n : Int} (hn : -2^31 ≤ n) (hn' : n < 2^31) : toInt (ofInt n) = n := by
|
||||
theorem ISize.toInt_ofInt_of_le {n : Int} (hn : -2^31 ≤ n) (hn' : n < 2^31) : toInt (ofInt n) = n := by
|
||||
rw [toInt, toBitVec_ofInt, BitVec.toInt_ofInt_eq_self] <;> cases System.Platform.numBits_eq
|
||||
<;> (simp_all; try omega)
|
||||
|
||||
|
|
@ -90,8 +102,14 @@ theorem ISize.toInt_ofInt_of_two_pow_numBits_le {n : Int} (hn : -2 ^ (System.Pla
|
|||
|
||||
theorem ISize.toNatClampNeg_ofInt_eq_zero {n : Int} (hn : -2^31 ≤ n) (hn' : n ≤ 0) :
|
||||
toNatClampNeg (ofInt n) = 0 := by
|
||||
rwa [toNatClampNeg, toInt_ofInt hn (by omega), Int.toNat_eq_zero]
|
||||
rwa [toNatClampNeg, toInt_ofInt_of_le hn (by omega), Int.toNat_eq_zero]
|
||||
|
||||
theorem Int8.neg_ofInt {n : Int} : -ofInt n = ofInt (-n) :=
|
||||
toBitVec.inj (by simp [BitVec.ofInt_neg])
|
||||
theorem Int16.neg_ofInt {n : Int} : -ofInt n = ofInt (-n) :=
|
||||
toBitVec.inj (by simp [BitVec.ofInt_neg])
|
||||
theorem Int32.neg_ofInt {n : Int} : -ofInt n = ofInt (-n) :=
|
||||
toBitVec.inj (by simp [BitVec.ofInt_neg])
|
||||
theorem Int64.neg_ofInt {n : Int} : -ofInt n = ofInt (-n) :=
|
||||
toBitVec.inj (by simp [BitVec.ofInt_neg])
|
||||
theorem ISize.neg_ofInt {n : Int} : -ofInt n = ofInt (-n) :=
|
||||
|
|
@ -103,37 +121,67 @@ theorem Int32.ofInt_eq_ofNat {n : Nat} : ofInt n = ofNat n := toBitVec.inj (by s
|
|||
theorem Int64.ofInt_eq_ofNat {n : Nat} : ofInt n = ofNat n := toBitVec.inj (by simp)
|
||||
theorem ISize.ofInt_eq_ofNat {n : Nat} : ofInt n = ofNat n := toBitVec.inj (by simp)
|
||||
|
||||
@[simp] theorem Int8.toInt_ofNat {n : Nat} : toInt (ofNat n) = (n : Int).bmod Int8.size := by
|
||||
rw [← ofInt_eq_ofNat, toInt_ofInt]
|
||||
@[simp] theorem Int16.toInt_ofNat {n : Nat} : toInt (ofNat n) = (n : Int).bmod Int16.size := by
|
||||
rw [← ofInt_eq_ofNat, toInt_ofInt]
|
||||
@[simp] theorem Int32.toInt_ofNat {n : Nat} : toInt (ofNat n) = (n : Int).bmod Int32.size := by
|
||||
rw [← ofInt_eq_ofNat, toInt_ofInt]
|
||||
@[simp] theorem Int64.toInt_ofNat {n : Nat} : toInt (ofNat n) = (n : Int).bmod Int64.size := by
|
||||
rw [← ofInt_eq_ofNat, toInt_ofInt]
|
||||
@[simp] theorem ISize.toInt_ofNat {n : Nat} : toInt (ofNat n) = (n : Int).bmod ISize.size := by
|
||||
rw [← ofInt_eq_ofNat, toInt_ofInt]
|
||||
|
||||
theorem Int8.neg_ofNat {n : Nat} : -ofNat n = ofInt (-n) := by
|
||||
rw [← neg_ofInt, ofInt_eq_ofNat]
|
||||
theorem Int16.neg_ofNat {n : Nat} : -ofNat n = ofInt (-n) := by
|
||||
rw [← neg_ofInt, ofInt_eq_ofNat]
|
||||
theorem Int32.neg_ofNat {n : Nat} : -ofNat n = ofInt (-n) := by
|
||||
rw [← neg_ofInt, ofInt_eq_ofNat]
|
||||
theorem Int64.neg_ofNat {n : Nat} : -ofNat n = ofInt (-n) := by
|
||||
rw [← neg_ofInt, ofInt_eq_ofNat]
|
||||
theorem ISize.neg_ofNat {n : Nat} : -ofNat n = ofInt (-n) := by
|
||||
rw [← neg_ofInt, ofInt_eq_ofNat]
|
||||
|
||||
theorem Int8.toNatClampNeg_ofNat_of_lt {n : Nat} (h : n < 2 ^ 7) : toNatClampNeg (ofNat n) = n := by
|
||||
rw [toNatClampNeg, ← ofInt_eq_ofNat, toInt_ofInt (by omega) (by omega), Int.toNat_ofNat]
|
||||
rw [toNatClampNeg, ← ofInt_eq_ofNat, toInt_ofInt_of_le (by omega) (by omega), Int.toNat_ofNat]
|
||||
theorem Int16.toNatClampNeg_ofNat_of_lt {n : Nat} (h : n < 2 ^ 15) : toNatClampNeg (ofNat n) = n := by
|
||||
rw [toNatClampNeg, ← ofInt_eq_ofNat, toInt_ofInt_of_le (by omega) (by omega), Int.toNat_ofNat]
|
||||
theorem Int32.toNatClampNeg_ofNat_of_lt {n : Nat} (h : n < 2 ^ 31) : toNatClampNeg (ofNat n) = n := by
|
||||
rw [toNatClampNeg, ← ofInt_eq_ofNat, toInt_ofInt_of_le (by omega) (by omega), Int.toNat_ofNat]
|
||||
theorem Int64.toNatClampNeg_ofNat_of_lt {n : Nat} (h : n < 2 ^ 63) : toNatClampNeg (ofNat n) = n := by
|
||||
rw [toNatClampNeg, ← ofInt_eq_ofNat, toInt_ofInt_of_le (by omega) (by omega), Int.toNat_ofNat]
|
||||
theorem ISize.toNatClampNeg_ofNat_of_lt {n : Nat} (h : n < 2 ^ 31) : toNatClampNeg (ofNat n) = n := by
|
||||
rw [toNatClampNeg, ← ofInt_eq_ofNat, toInt_ofInt (by omega) (by omega), Int.toNat_ofNat]
|
||||
rw [toNatClampNeg, ← ofInt_eq_ofNat, toInt_ofInt_of_le (by omega) (by omega), Int.toNat_ofNat]
|
||||
theorem ISize.toNatClampNeg_ofNat_of_lt_two_pow_numBits {n : Nat} (h : n < 2 ^ (System.Platform.numBits - 1)) :
|
||||
toNatClampNeg (ofNat n) = n := by
|
||||
rw [toNatClampNeg, ← ofInt_eq_ofNat, toInt_ofInt_of_two_pow_numBits_le, Int.toNat_ofNat]
|
||||
· cases System.Platform.numBits_eq <;> simp_all <;> omega
|
||||
· cases System.Platform.numBits_eq <;> simp_all <;> omega
|
||||
|
||||
theorem ISize.toNatClampNeg_neg_ofNat_of_le {n : Nat} (h : n ≤ 2 ^ 31) :
|
||||
toNatClampNeg (-ofNat n) = 0 := by
|
||||
rw [neg_ofNat, toNatClampNeg_ofInt_eq_zero (by omega) (by omega)]
|
||||
|
||||
theorem Int8.toInt_ofNat_of_lt {n : Nat} (h : n < 2 ^ 7) : toInt (ofNat n) = n := by
|
||||
rw [← ofInt_eq_ofNat, toInt_ofInt (by omega) (by omega)]
|
||||
rw [← ofInt_eq_ofNat, toInt_ofInt_of_le (by omega) (by omega)]
|
||||
theorem Int16.toInt_ofNat_of_lt {n : Nat} (h : n < 2 ^ 15) : toInt (ofNat n) = n := by
|
||||
rw [← ofInt_eq_ofNat, toInt_ofInt (by omega) (by omega)]
|
||||
rw [← ofInt_eq_ofNat, toInt_ofInt_of_le (by omega) (by omega)]
|
||||
theorem Int32.toInt_ofNat_of_lt {n : Nat} (h : n < 2 ^ 31) : toInt (ofNat n) = n := by
|
||||
rw [← ofInt_eq_ofNat, toInt_ofInt (by omega) (by omega)]
|
||||
rw [← ofInt_eq_ofNat, toInt_ofInt_of_le (by omega) (by omega)]
|
||||
theorem Int64.toInt_ofNat_of_lt {n : Nat} (h : n < 2 ^ 63) : toInt (ofNat n) = n := by
|
||||
rw [← ofInt_eq_ofNat, toInt_ofInt (by omega) (by omega)]
|
||||
rw [← ofInt_eq_ofNat, toInt_ofInt_of_le (by omega) (by omega)]
|
||||
theorem ISize.toInt_ofNat_of_lt {n : Nat} (h : n < 2 ^ 31) : toInt (ofNat n) = n := by
|
||||
rw [← ofInt_eq_ofNat, toInt_ofInt (by omega) (by omega)]
|
||||
rw [← ofInt_eq_ofNat, toInt_ofInt_of_le (by omega) (by omega)]
|
||||
theorem ISize.toInt_ofNat_of_lt_two_pow_numBits {n : Nat}
|
||||
(h : n < 2 ^ (System.Platform.numBits - 1)) : toInt (ofNat n) = n := by
|
||||
rw [← ofInt_eq_ofNat, toInt_ofInt_of_two_pow_numBits_le] <;>
|
||||
cases System.Platform.numBits_eq <;> simp_all <;> omega
|
||||
|
||||
theorem Int64.toInt_neg_ofNat_of_le {n : Nat} (h : n ≤ 2^63) : toInt (-ofNat n) = -n := by
|
||||
rw [← ofInt_eq_ofNat, neg_ofInt, toInt_ofInt (by omega) (by omega)]
|
||||
rw [← ofInt_eq_ofNat, neg_ofInt, toInt_ofInt_of_le (by omega) (by omega)]
|
||||
theorem ISize.toInt_neg_ofNat_of_le {n : Nat} (h : n ≤ 2 ^ 31) : toInt (-ofNat n) = -n := by
|
||||
rw [← ofInt_eq_ofNat, neg_ofInt, toInt_ofInt (by omega) (by omega)]
|
||||
rw [← ofInt_eq_ofNat, neg_ofInt, toInt_ofInt_of_le (by omega) (by omega)]
|
||||
|
||||
theorem Int8.toInt_zero : toInt 0 = 0 := by simp
|
||||
theorem Int16.toInt_zero : toInt 0 = 0 := by simp
|
||||
|
|
@ -141,13 +189,30 @@ theorem Int32.toInt_zero : toInt 0 = 0 := by simp
|
|||
theorem Int64.toInt_zero : toInt 0 = 0 := by simp
|
||||
theorem ISize.toInt_zero : toInt 0 = 0 := by simp
|
||||
|
||||
theorem Int8.toInt_minValue : Int8.minValue.toInt = -2^7 := rfl
|
||||
theorem Int16.toInt_minValue : Int16.minValue.toInt = -2^15 := rfl
|
||||
theorem Int32.toInt_minValue : Int32.minValue.toInt = -2^31 := rfl
|
||||
theorem Int64.toInt_minValue : Int64.minValue.toInt = -2^63 := rfl
|
||||
@[simp] theorem ISize.toInt_minValue : ISize.minValue.toInt = -2^(System.Platform.numBits - 1) := by
|
||||
rw [minValue, toInt_ofInt_of_two_pow_numBits_le] <;> cases System.Platform.numBits_eq
|
||||
<;> simp_all
|
||||
|
||||
theorem Int8.toInt_maxValue : Int8.maxValue.toInt = 2 ^ 7 - 1 := rfl
|
||||
theorem Int16.toInt_maxValue : Int16.maxValue.toInt = 2 ^ 15 - 1 := rfl
|
||||
theorem Int32.toInt_maxValue : Int32.maxValue.toInt = 2 ^ 31 - 1 := rfl
|
||||
theorem Int64.toInt_maxValue : Int64.maxValue.toInt = 2 ^ 63 - 1 := rfl
|
||||
@[simp] theorem ISize.toInt_maxValue : ISize.maxValue.toInt = 2^(System.Platform.numBits - 1) - 1:= by
|
||||
rw [maxValue, toInt_ofInt_of_two_pow_numBits_le] <;> cases System.Platform.numBits_eq
|
||||
<;> simp_all
|
||||
|
||||
@[simp] theorem Int8.toNatClampNeg_minValue : Int8.minValue.toNatClampNeg = 0 := rfl
|
||||
@[simp] theorem Int16.toNatClampNeg_minValue : Int16.minValue.toNatClampNeg = 0 := rfl
|
||||
@[simp] theorem Int32.toNatClampNeg_minValue : Int32.minValue.toNatClampNeg = 0 := rfl
|
||||
@[simp] theorem Int64.toNatClampNeg_minValue : Int64.minValue.toNatClampNeg = 0 := rfl
|
||||
@[simp] theorem ISize.toNatClampNeg_minValue : ISize.minValue.toNatClampNeg = 0 := by
|
||||
rw [toNatClampNeg, toInt_minValue]
|
||||
cases System.Platform.numBits_eq <;> simp_all
|
||||
|
||||
@[simp] theorem UInt8.toBitVec_toInt8 (x : UInt8) : x.toInt8.toBitVec = x.toBitVec := rfl
|
||||
@[simp] theorem UInt16.toBitVec_toInt16 (x : UInt16) : x.toInt16.toBitVec = x.toBitVec := rfl
|
||||
@[simp] theorem UInt32.toBitVec_toInt32 (x : UInt32) : x.toInt32.toBitVec = x.toBitVec := rfl
|
||||
|
|
@ -551,13 +616,13 @@ theorem ISize.ofIntLE_int64ToInt (x : Int64) {h₁ h₂} : ISize.ofIntLE x.toInt
|
|||
@[simp] theorem ISize.ofInt_int64ToInt (x : Int64) : ISize.ofInt x.toInt = x.toISize := rfl
|
||||
|
||||
@[simp] theorem Int8.toInt_ofIntLE {x : Int} {h₁ h₂} : (ofIntLE x h₁ h₂).toInt = x := by
|
||||
rw [ofIntLE, toInt_ofInt h₁ (Int.lt_of_le_sub_one h₂)]
|
||||
rw [ofIntLE, toInt_ofInt_of_le h₁ (Int.lt_of_le_sub_one h₂)]
|
||||
@[simp] theorem Int16.toInt_ofIntLE {x : Int} {h₁ h₂} : (ofIntLE x h₁ h₂).toInt = x := by
|
||||
rw [ofIntLE, toInt_ofInt h₁ (Int.lt_of_le_sub_one h₂)]
|
||||
rw [ofIntLE, toInt_ofInt_of_le h₁ (Int.lt_of_le_sub_one h₂)]
|
||||
@[simp] theorem Int32.toInt_ofIntLE {x : Int} {h₁ h₂} : (ofIntLE x h₁ h₂).toInt = x := by
|
||||
rw [ofIntLE, toInt_ofInt h₁ (Int.lt_of_le_sub_one h₂)]
|
||||
rw [ofIntLE, toInt_ofInt_of_le h₁ (Int.lt_of_le_sub_one h₂)]
|
||||
@[simp] theorem Int64.toInt_ofIntLE {x : Int} {h₁ h₂} : (ofIntLE x h₁ h₂).toInt = x := by
|
||||
rw [ofIntLE, toInt_ofInt h₁ (Int.lt_of_le_sub_one h₂)]
|
||||
rw [ofIntLE, toInt_ofInt_of_le h₁ (Int.lt_of_le_sub_one h₂)]
|
||||
@[simp] theorem ISize.toInt_ofIntLE {x : Int} {h₁ h₂} : (ofIntLE x h₁ h₂).toInt = x := by
|
||||
rw [ofIntLE, toInt_ofInt_of_two_pow_numBits_le]
|
||||
· simpa using h₁
|
||||
|
|
@ -575,6 +640,12 @@ theorem Int64.ofIntLE_eq_ofIntTruncate {x : Int} {h₁ h₂} : (ofIntLE x h₁ h
|
|||
theorem ISize.ofIntLE_eq_ofIntTruncate {x : Int} {h₁ h₂} : (ofIntLE x h₁ h₂) = ofIntTruncate x := by
|
||||
rw [ofIntTruncate, dif_pos h₁, dif_pos h₂]
|
||||
|
||||
theorem Int8.ofIntLE_eq_ofInt {n : Int} (h₁ h₂) : Int8.ofIntLE n h₁ h₂ = Int8.ofInt n := rfl
|
||||
theorem Int16.ofIntLE_eq_ofInt {n : Int} (h₁ h₂) : Int16.ofIntLE n h₁ h₂ = Int16.ofInt n := rfl
|
||||
theorem Int32.ofIntLE_eq_ofInt {n : Int} (h₁ h₂) : Int32.ofIntLE n h₁ h₂ = Int32.ofInt n := rfl
|
||||
theorem Int64.ofIntLE_eq_ofInt {n : Int} (h₁ h₂) : Int64.ofIntLE n h₁ h₂ = Int64.ofInt n := rfl
|
||||
theorem ISize.ofIntLE_eq_ofInt {n : Int} (h₁ h₂) : ISize.ofIntLE n h₁ h₂ = ISize.ofInt n := rfl
|
||||
|
||||
theorem Int8.toInt_ofIntTruncate {x : Int} (h₁ : Int8.minValue.toInt ≤ x)
|
||||
(h₂ : x ≤ Int8.maxValue.toInt) : (Int8.ofIntTruncate x).toInt = x := by
|
||||
rw [← ofIntLE_eq_ofIntTruncate (h₁ := h₁) (h₂ := h₂), toInt_ofIntLE]
|
||||
|
|
@ -865,3 +936,473 @@ theorem USize.toISize_ofNatLT {n : Nat} (hn) : (USize.ofNatLT n hn).toISize = IS
|
|||
@[simp] theorem UInt32.toInt32_ofBitVec (b) : (UInt32.ofBitVec b).toInt32 = Int32.ofBitVec b := rfl
|
||||
@[simp] theorem UInt64.toInt64_ofBitVec (b) : (UInt64.ofBitVec b).toInt64 = Int64.ofBitVec b := rfl
|
||||
@[simp] theorem USize.toInt8_ofBitVec (b) : (USize.ofBitVec b).toISize = ISize.ofBitVec b := rfl
|
||||
|
||||
@[simp] theorem Int8.toBitVec_ofBitVec (b) : (Int8.ofBitVec b).toBitVec = b := rfl
|
||||
@[simp] theorem Int16.toBitVec_ofBitVec (b) : (Int16.ofBitVec b).toBitVec = b := rfl
|
||||
@[simp] theorem Int32.toBitVec_ofBitVec (b) : (Int32.ofBitVec b).toBitVec = b := rfl
|
||||
@[simp] theorem Int64.toBitVec_ofBitVec (b) : (Int64.ofBitVec b).toBitVec = b := rfl
|
||||
@[simp] theorem ISize.toBitVec_ofBitVec (b) : (ISize.ofBitVec b).toBitVec = b := rfl
|
||||
|
||||
theorem Int8.toBitVec_ofIntTruncate {n : Int} (h₁ : Int8.minValue.toInt ≤ n) (h₂ : n ≤ Int8.maxValue.toInt) :
|
||||
(Int8.ofIntTruncate n).toBitVec = BitVec.ofInt _ n := by
|
||||
rw [← ofIntLE_eq_ofIntTruncate (h₁ := h₁) (h₂ := h₂), toBitVec_ofIntLE]
|
||||
theorem Int16.toBitVec_ofIntTruncate {n : Int} (h₁ : Int16.minValue.toInt ≤ n) (h₂ : n ≤ Int16.maxValue.toInt) :
|
||||
(Int16.ofIntTruncate n).toBitVec = BitVec.ofInt _ n := by
|
||||
rw [← ofIntLE_eq_ofIntTruncate (h₁ := h₁) (h₂ := h₂), toBitVec_ofIntLE]
|
||||
theorem Int32.toBitVec_ofIntTruncate {n : Int} (h₁ : Int32.minValue.toInt ≤ n) (h₂ : n ≤ Int32.maxValue.toInt) :
|
||||
(Int32.ofIntTruncate n).toBitVec = BitVec.ofInt _ n := by
|
||||
rw [← ofIntLE_eq_ofIntTruncate (h₁ := h₁) (h₂ := h₂), toBitVec_ofIntLE]
|
||||
theorem Int64.toBitVec_ofIntTruncate {n : Int} (h₁ : Int64.minValue.toInt ≤ n) (h₂ : n ≤ Int64.maxValue.toInt) :
|
||||
(Int64.ofIntTruncate n).toBitVec = BitVec.ofInt _ n := by
|
||||
rw [← ofIntLE_eq_ofIntTruncate (h₁ := h₁) (h₂ := h₂), toBitVec_ofIntLE]
|
||||
theorem ISize.toBitVec_ofIntTruncate {n : Int} (h₁ : ISize.minValue.toInt ≤ n) (h₂ : n ≤ ISize.maxValue.toInt) :
|
||||
(ISize.ofIntTruncate n).toBitVec = BitVec.ofInt _ n := by
|
||||
rw [← ofIntLE_eq_ofIntTruncate (h₁ := h₁) (h₂ := h₂), toBitVec_ofIntLE]
|
||||
|
||||
@[simp] theorem Int8.toInt_ofBitVec (b) : (Int8.ofBitVec b).toInt = b.toInt := rfl
|
||||
@[simp] theorem Int16.toInt_ofBitVec (b) : (Int16.ofBitVec b).toInt = b.toInt := rfl
|
||||
@[simp] theorem Int32.toInt_ofBitVec (b) : (Int32.ofBitVec b).toInt = b.toInt := rfl
|
||||
@[simp] theorem Int64.toInt_ofBitVec (b) : (Int64.ofBitVec b).toInt = b.toInt := rfl
|
||||
@[simp] theorem ISize.toInt_ofBitVec (b) : (ISize.ofBitVec b).toInt = b.toInt := rfl
|
||||
|
||||
@[simp] theorem Int8.toNatClampNeg_ofIntLE {n : Int} (h₁ h₂) : (Int8.ofIntLE n h₁ h₂).toNatClampNeg = n.toNat := by
|
||||
rw [ofIntLE, toNatClampNeg, toInt_ofInt_of_le h₁ (Int.lt_of_le_sub_one h₂)]
|
||||
@[simp] theorem Int16.toNatClampNeg_ofIntLE {n : Int} (h₁ h₂) : (Int16.ofIntLE n h₁ h₂).toNatClampNeg = n.toNat := by
|
||||
rw [ofIntLE, toNatClampNeg, toInt_ofInt_of_le h₁ (Int.lt_of_le_sub_one h₂)]
|
||||
@[simp] theorem Int32.toNatClampNeg_ofIntLE {n : Int} (h₁ h₂) : (Int32.ofIntLE n h₁ h₂).toNatClampNeg = n.toNat := by
|
||||
rw [ofIntLE, toNatClampNeg, toInt_ofInt_of_le h₁ (Int.lt_of_le_sub_one h₂)]
|
||||
@[simp] theorem Int64.toNatClampNeg_ofIntLE {n : Int} (h₁ h₂) : (Int64.ofIntLE n h₁ h₂).toNatClampNeg = n.toNat := by
|
||||
rw [ofIntLE, toNatClampNeg, toInt_ofInt_of_le h₁ (Int.lt_of_le_sub_one h₂)]
|
||||
@[simp] theorem ISize.toNatClampNeg_ofIntLE {n : Int} (h₁ h₂) : (ISize.ofIntLE n h₁ h₂).toNatClampNeg = n.toNat := by
|
||||
rw [ofIntLE, toNatClampNeg, toInt_ofInt_of_two_pow_numBits_le]
|
||||
· rwa [← ISize.toInt_minValue]
|
||||
· apply Int.lt_of_le_sub_one
|
||||
rwa [← ISize.toInt_maxValue]
|
||||
|
||||
@[simp] theorem Int8.toNatClampNeg_ofBitVec (b) : (Int8.ofBitVec b).toNatClampNeg = b.toInt.toNat := rfl
|
||||
@[simp] theorem Int16.toNatClampNeg_ofBitVec (b) : (Int16.ofBitVec b).toNatClampNeg = b.toInt.toNat := rfl
|
||||
@[simp] theorem Int32.toNatClampNeg_ofBitVec (b) : (Int32.ofBitVec b).toNatClampNeg = b.toInt.toNat := rfl
|
||||
@[simp] theorem Int64.toNatClampNeg_ofBitVec (b) : (Int64.ofBitVec b).toNatClampNeg = b.toInt.toNat := rfl
|
||||
@[simp] theorem ISize.toNatClampNeg_ofBitVec (b) : (ISize.ofBitVec b).toNatClampNeg = b.toInt.toNat := rfl
|
||||
|
||||
theorem Int8.toNatClampNeg_ofInt_of_le {n : Int} (h₁ : -2 ^ 7 ≤ n) (h₂ : n < 2 ^ 7) :
|
||||
(Int8.ofInt n).toNatClampNeg = n.toNat := by rw [toNatClampNeg, toInt_ofInt_of_le h₁ h₂]
|
||||
theorem Int16.toNatClampNeg_ofInt_of_le {n : Int} (h₁ : -2 ^ 15 ≤ n) (h₂ : n < 2 ^ 15) :
|
||||
(Int16.ofInt n).toNatClampNeg = n.toNat := by rw [toNatClampNeg, toInt_ofInt_of_le h₁ h₂]
|
||||
theorem Int32.toNatClampNeg_ofInt_of_le {n : Int} (h₁ : -2 ^ 31 ≤ n) (h₂ : n < 2 ^ 31) :
|
||||
(Int32.ofInt n).toNatClampNeg = n.toNat := by rw [toNatClampNeg, toInt_ofInt_of_le h₁ h₂]
|
||||
theorem Int64.toNatClampNeg_ofInt_of_le {n : Int} (h₁ : -2 ^ 63 ≤ n) (h₂ : n < 2 ^ 63) :
|
||||
(Int64.ofInt n).toNatClampNeg = n.toNat := by rw [toNatClampNeg, toInt_ofInt_of_le h₁ h₂]
|
||||
theorem ISize.toNatClampNeg_ofInt_of_le {n : Int} (h₁ : -2 ^ 31 ≤ n)
|
||||
(h₂ : n < 2 ^ 31) : (ISize.ofInt n).toNatClampNeg = n.toNat := by
|
||||
rw [toNatClampNeg, toInt_ofInt_of_le h₁ h₂]
|
||||
theorem ISize.toNatClampNeg_ofInt_of_two_pow_numBits {n : Int} (h₁ : -2 ^ (System.Platform.numBits - 1) ≤ n)
|
||||
(h₂ : n < 2 ^ (System.Platform.numBits - 1)) : (ISize.ofInt n).toNatClampNeg = n.toNat := by
|
||||
rw [toNatClampNeg, toInt_ofInt_of_two_pow_numBits_le h₁ h₂]
|
||||
|
||||
theorem Int8.toNatClampNeg_ofIntTruncate_of_lt {n : Int} (h₁ : n < 2 ^ 7) :
|
||||
(Int8.ofIntTruncate n).toNatClampNeg = n.toNat := by
|
||||
rw [ofIntTruncate]
|
||||
split
|
||||
· rw [dif_pos (by rw [toInt_maxValue]; omega), toNatClampNeg_ofIntLE]
|
||||
· next h =>
|
||||
rw [toNatClampNeg_minValue, eq_comm, Int.toNat_eq_zero]
|
||||
rw [toInt_minValue] at h
|
||||
omega
|
||||
theorem Int16.toNatClampNeg_ofIntTruncate_of_lt {n : Int} (h₁ : n < 2 ^ 15) :
|
||||
(Int16.ofIntTruncate n).toNatClampNeg = n.toNat := by
|
||||
rw [ofIntTruncate]
|
||||
split
|
||||
· rw [dif_pos (by rw [toInt_maxValue]; omega), toNatClampNeg_ofIntLE]
|
||||
· next h =>
|
||||
rw [toNatClampNeg_minValue, eq_comm, Int.toNat_eq_zero]
|
||||
rw [toInt_minValue] at h
|
||||
omega
|
||||
theorem Int32.toNatClampNeg_ofIntTruncate_of_lt {n : Int} (h₁ : n < 2 ^ 31) :
|
||||
(Int32.ofIntTruncate n).toNatClampNeg = n.toNat := by
|
||||
rw [ofIntTruncate]
|
||||
split
|
||||
· rw [dif_pos (by rw [toInt_maxValue]; omega), toNatClampNeg_ofIntLE]
|
||||
· next h =>
|
||||
rw [toNatClampNeg_minValue, eq_comm, Int.toNat_eq_zero]
|
||||
rw [toInt_minValue] at h
|
||||
omega
|
||||
theorem Int64.toNatClampNeg_ofIntTruncate_of_lt {n : Int} (h₁ : n < 2 ^ 63) :
|
||||
(Int64.ofIntTruncate n).toNatClampNeg = n.toNat := by
|
||||
rw [ofIntTruncate]
|
||||
split
|
||||
· rw [dif_pos (by rw [toInt_maxValue]; omega), toNatClampNeg_ofIntLE]
|
||||
· next h =>
|
||||
rw [toNatClampNeg_minValue, eq_comm, Int.toNat_eq_zero]
|
||||
rw [toInt_minValue] at h
|
||||
omega
|
||||
theorem ISize.toNatClampNeg_ofIntTruncate_of_lt_two_pow_numBits {n : Int} (h₁ : n < 2 ^ (System.Platform.numBits - 1)) :
|
||||
(ISize.ofIntTruncate n).toNatClampNeg = n.toNat := by
|
||||
rw [ofIntTruncate]
|
||||
split
|
||||
· rw [dif_pos (by rw [toInt_maxValue]; omega), toNatClampNeg_ofIntLE]
|
||||
· next h =>
|
||||
rw [toNatClampNeg_minValue, eq_comm, Int.toNat_eq_zero]
|
||||
rw [toInt_minValue] at h
|
||||
omega
|
||||
theorem ISize.toNatClampNeg_ofIntTruncate_of_lt {n : Int} (h₁ : n < 2 ^ 31) :
|
||||
(ISize.ofIntTruncate n).toNatClampNeg = n.toNat := by
|
||||
apply ISize.toNatClampNeg_ofIntTruncate_of_lt_two_pow_numBits (Int.lt_of_lt_of_le h₁ _)
|
||||
cases System.Platform.numBits_eq <;> simp_all
|
||||
|
||||
@[simp] theorem Int8.toUInt8_ofBitVec (b) : (Int8.ofBitVec b).toUInt8 = UInt8.ofBitVec b := rfl
|
||||
@[simp] theorem Int16.toUInt16_ofBitVec (b) : (Int16.ofBitVec b).toUInt16 = UInt16.ofBitVec b := rfl
|
||||
@[simp] theorem Int32.toUInt32_ofBitVec (b) : (Int32.ofBitVec b).toUInt32 = UInt32.ofBitVec b := rfl
|
||||
@[simp] theorem Int64.toUInt64_ofBitVec (b) : (Int64.ofBitVec b).toUInt64 = UInt64.ofBitVec b := rfl
|
||||
@[simp] theorem ISize.toUSize_ofBitVec (b) : (ISize.ofBitVec b).toUSize = USize.ofBitVec b := rfl
|
||||
|
||||
@[simp] theorem Int8.toUInt8_ofNat' {n} : (Int8.ofNat n).toUInt8 = UInt8.ofNat n := rfl
|
||||
@[simp] theorem Int16.toUInt16_ofNat' {n} : (Int16.ofNat n).toUInt16 = UInt16.ofNat n := rfl
|
||||
@[simp] theorem Int32.toUInt32_ofNat' {n} : (Int32.ofNat n).toUInt32 = UInt32.ofNat n := rfl
|
||||
@[simp] theorem Int64.toUInt64_ofNat' {n} : (Int64.ofNat n).toUInt64 = UInt64.ofNat n := rfl
|
||||
@[simp] theorem ISize.toUSize_ofNat' {n} : (ISize.ofNat n).toUSize = USize.ofNat n := rfl
|
||||
|
||||
@[simp] theorem Int8.toUInt8_ofNat {n} : toUInt8 (OfNat.ofNat n) = OfNat.ofNat n := rfl
|
||||
@[simp] theorem Int16.toUInt16_ofNat {n} : toUInt16 (OfNat.ofNat n) = OfNat.ofNat n := rfl
|
||||
@[simp] theorem Int32.toUInt32_ofNat {n} : toUInt32 (OfNat.ofNat n) = OfNat.ofNat n := rfl
|
||||
@[simp] theorem Int64.toUInt64_ofNat {n} : toUInt64 (OfNat.ofNat n) = OfNat.ofNat n := rfl
|
||||
@[simp] theorem ISize.toUISize_ofNat {n} : toUSize (OfNat.ofNat n) = OfNat.ofNat n := rfl
|
||||
|
||||
theorem Int16.toInt8_ofIntLE {n} (h₁ h₂) : (Int16.ofIntLE n h₁ h₂).toInt8 = Int8.ofInt n := Int8.toInt.inj (by simp)
|
||||
theorem Int32.toInt8_ofIntLE {n} (h₁ h₂) : (Int32.ofIntLE n h₁ h₂).toInt8 = Int8.ofInt n := Int8.toInt.inj (by simp)
|
||||
theorem Int64.toInt8_ofIntLE {n} (h₁ h₂) : (Int64.ofIntLE n h₁ h₂).toInt8 = Int8.ofInt n := Int8.toInt.inj (by simp)
|
||||
theorem ISize.toInt8_ofIntLE {n} (h₁ h₂) : (ISize.ofIntLE n h₁ h₂).toInt8 = Int8.ofInt n := Int8.toInt.inj (by simp)
|
||||
|
||||
@[simp] theorem Int16.toInt8_ofBitVec (b) : (Int16.ofBitVec b).toInt8 = Int8.ofBitVec (b.signExtend _) := rfl
|
||||
@[simp] theorem Int32.toInt8_ofBitVec (b) : (Int32.ofBitVec b).toInt8 = Int8.ofBitVec (b.signExtend _) := rfl
|
||||
@[simp] theorem Int64.toInt8_ofBitVec (b) : (Int64.ofBitVec b).toInt8 = Int8.ofBitVec (b.signExtend _) := rfl
|
||||
@[simp] theorem ISize.toInt8_ofBitVec (b) : (ISize.ofBitVec b).toInt8 = Int8.ofBitVec (b.signExtend _) := rfl
|
||||
|
||||
@[simp] theorem Int16.toInt8_ofNat' {n} : (Int16.ofNat n).toInt8 = Int8.ofNat n :=
|
||||
Int8.toBitVec.inj (by simp [BitVec.signExtend_eq_setWidth_of_le])
|
||||
@[simp] theorem Int32.toInt8_ofNat' {n} : (Int32.ofNat n).toInt8 = Int8.ofNat n :=
|
||||
Int8.toBitVec.inj (by simp [BitVec.signExtend_eq_setWidth_of_le])
|
||||
@[simp] theorem Int64.toInt8_ofNat' {n} : (Int64.ofNat n).toInt8 = Int8.ofNat n :=
|
||||
Int8.toBitVec.inj (by simp [BitVec.signExtend_eq_setWidth_of_le])
|
||||
@[simp] theorem ISize.toInt8_ofNat' {n} : (ISize.ofNat n).toInt8 = Int8.ofNat n := by
|
||||
apply Int8.toBitVec.inj
|
||||
simp only [toBitVec_toInt8, toBitVec_ofNat', Int8.toBitVec_ofNat']
|
||||
rw [BitVec.signExtend_eq_setWidth_of_le, BitVec.setWidth_ofNat_of_le]
|
||||
all_goals cases System.Platform.numBits_eq <;> simp_all
|
||||
|
||||
@[simp] theorem Int16.toInt8_ofInt {n} : (Int16.ofInt n).toInt8 = Int8.ofInt n :=
|
||||
Int8.toInt.inj (by simpa using Int.bmod_bmod_of_dvd (by decide))
|
||||
@[simp] theorem Int32.toInt8_ofInt {n} : (Int32.ofInt n).toInt8 = Int8.ofInt n :=
|
||||
Int8.toInt.inj (by simpa using Int.bmod_bmod_of_dvd (by decide))
|
||||
@[simp] theorem Int64.toInt8_ofInt {n} : (Int64.ofInt n).toInt8 = Int8.ofInt n :=
|
||||
Int8.toInt.inj (by simpa using Int.bmod_bmod_of_dvd (by decide))
|
||||
@[simp] theorem ISize.toInt8_ofInt {n} : (ISize.ofInt n).toInt8 = Int8.ofInt n := by
|
||||
apply Int8.toInt.inj
|
||||
simp only [toInt_toInt8, toInt_ofInt, Nat.reducePow, Int8.toInt_ofInt]
|
||||
exact Int.bmod_bmod_of_dvd UInt8.size_dvd_usizeSize
|
||||
|
||||
@[simp] theorem Int16.toInt8_ofNat {n} : toInt8 (no_index (OfNat.ofNat n)) = OfNat.ofNat n := toInt8_ofNat'
|
||||
@[simp] theorem Int32.toInt8_ofNat {n} : toInt8 (no_index (OfNat.ofNat n)) = OfNat.ofNat n := toInt8_ofNat'
|
||||
@[simp] theorem Int64.toInt8_ofNat {n} : toInt8 (no_index (OfNat.ofNat n)) = OfNat.ofNat n := toInt8_ofNat'
|
||||
@[simp] theorem ISize.toInt8_ofNat {n} : toInt8 (no_index (OfNat.ofNat n)) = OfNat.ofNat n := toInt8_ofNat'
|
||||
|
||||
theorem Int16.toInt8_ofIntTruncate {n : Int} (h₁ : -2 ^ 15 ≤ n) (h₂ : n < 2 ^ 15) :
|
||||
(Int16.ofIntTruncate n).toInt8 = Int8.ofInt n := by
|
||||
rw [← ofIntLE_eq_ofIntTruncate (h₁ := h₁) (h₂ := Int.le_of_lt_add_one h₂), toInt8_ofIntLE]
|
||||
theorem Int32.toInt8_ofIntTruncate {n : Int} (h₁ : -2 ^ 31 ≤ n) (h₂ : n < 2 ^ 31) :
|
||||
(Int32.ofIntTruncate n).toInt8 = Int8.ofInt n := by
|
||||
rw [← ofIntLE_eq_ofIntTruncate (h₁ := h₁) (h₂ := Int.le_of_lt_add_one h₂), toInt8_ofIntLE]
|
||||
theorem Int64.toInt8_ofIntTruncate {n : Int} (h₁ : -2 ^ 63 ≤ n) (h₂ : n < 2 ^ 63) :
|
||||
(Int64.ofIntTruncate n).toInt8 = Int8.ofInt n := by
|
||||
rw [← ofIntLE_eq_ofIntTruncate (h₁ := h₁) (h₂ := Int.le_of_lt_add_one h₂), toInt8_ofIntLE]
|
||||
theorem ISize.toInt8_ofIntTruncate {n : Int} (h₁ : -2 ^ (System.Platform.numBits - 1) ≤ n)
|
||||
(h₂ : n < 2 ^ (System.Platform.numBits - 1)) : (ISize.ofIntTruncate n).toInt8 = Int8.ofInt n := by
|
||||
rw [← ofIntLE_eq_ofIntTruncate, toInt8_ofIntLE]
|
||||
· exact toInt_minValue ▸ h₁
|
||||
· rw [toInt_maxValue]
|
||||
omega
|
||||
|
||||
theorem Int32.toInt16_ofIntLE {n} (h₁ h₂) : (Int32.ofIntLE n h₁ h₂).toInt16 = Int16.ofInt n := Int16.toInt.inj (by simp)
|
||||
theorem Int64.toInt16_ofIntLE {n} (h₁ h₂) : (Int64.ofIntLE n h₁ h₂).toInt16 = Int16.ofInt n := Int16.toInt.inj (by simp)
|
||||
theorem ISize.toInt16_ofIntLE {n} (h₁ h₂) : (ISize.ofIntLE n h₁ h₂).toInt16 = Int16.ofInt n := Int16.toInt.inj (by simp)
|
||||
|
||||
@[simp] theorem Int32.toInt16_ofBitVec (b) : (Int32.ofBitVec b).toInt16 = Int16.ofBitVec (b.signExtend _) := rfl
|
||||
@[simp] theorem Int64.toInt16_ofBitVec (b) : (Int64.ofBitVec b).toInt16 = Int16.ofBitVec (b.signExtend _) := rfl
|
||||
@[simp] theorem ISize.toInt16_ofBitVec (b) : (ISize.ofBitVec b).toInt16 = Int16.ofBitVec (b.signExtend _) := rfl
|
||||
|
||||
@[simp] theorem Int32.toInt16_ofNat' {n} : (Int32.ofNat n).toInt16 = Int16.ofNat n :=
|
||||
Int16.toBitVec.inj (by simp [BitVec.signExtend_eq_setWidth_of_le])
|
||||
@[simp] theorem Int64.toInt16_ofNat' {n} : (Int64.ofNat n).toInt16 = Int16.ofNat n :=
|
||||
Int16.toBitVec.inj (by simp [BitVec.signExtend_eq_setWidth_of_le])
|
||||
@[simp] theorem ISize.toInt16_ofNat' {n} : (ISize.ofNat n).toInt16 = Int16.ofNat n := by
|
||||
apply Int16.toBitVec.inj
|
||||
simp only [toBitVec_toInt16, toBitVec_ofNat', Int16.toBitVec_ofNat']
|
||||
rw [BitVec.signExtend_eq_setWidth_of_le, BitVec.setWidth_ofNat_of_le]
|
||||
all_goals cases System.Platform.numBits_eq <;> simp_all
|
||||
|
||||
@[simp] theorem Int32.toInt16_ofInt {n} : (Int32.ofInt n).toInt16 = Int16.ofInt n :=
|
||||
Int16.toInt.inj (by simpa using Int.bmod_bmod_of_dvd (by decide))
|
||||
@[simp] theorem Int64.toInt16_ofInt {n} : (Int64.ofInt n).toInt16 = Int16.ofInt n :=
|
||||
Int16.toInt.inj (by simpa using Int.bmod_bmod_of_dvd (by decide))
|
||||
@[simp] theorem ISize.toInt16_ofInt {n} : (ISize.ofInt n).toInt16 = Int16.ofInt n := by
|
||||
apply Int16.toInt.inj
|
||||
simp only [toInt_toInt16, toInt_ofInt, Nat.reducePow, Int16.toInt_ofInt]
|
||||
exact Int.bmod_bmod_of_dvd UInt16.size_dvd_usizeSize
|
||||
|
||||
@[simp] theorem Int32.toInt16_ofNat {n} : toInt16 (no_index (OfNat.ofNat n)) = OfNat.ofNat n := toInt16_ofNat'
|
||||
@[simp] theorem Int64.toInt16_ofNat {n} : toInt16 (no_index (OfNat.ofNat n)) = OfNat.ofNat n := toInt16_ofNat'
|
||||
@[simp] theorem ISize.toInt16_ofNat {n} : toInt16 (no_index (OfNat.ofNat n)) = OfNat.ofNat n := toInt16_ofNat'
|
||||
|
||||
theorem Int32.toInt16_ofIntTruncate {n : Int} (h₁ : -2 ^ 31 ≤ n) (h₂ : n < 2 ^ 31) :
|
||||
(Int32.ofIntTruncate n).toInt16 = Int16.ofInt n := by
|
||||
rw [← ofIntLE_eq_ofIntTruncate (h₁ := h₁) (h₂ := Int.le_of_lt_add_one h₂), toInt16_ofIntLE]
|
||||
theorem Int64.toInt16_ofIntTruncate {n : Int} (h₁ : -2 ^ 63 ≤ n) (h₂ : n < 2 ^ 63) :
|
||||
(Int64.ofIntTruncate n).toInt16 = Int16.ofInt n := by
|
||||
rw [← ofIntLE_eq_ofIntTruncate (h₁ := h₁) (h₂ := Int.le_of_lt_add_one h₂), toInt16_ofIntLE]
|
||||
theorem ISize.toInt16_ofIntTruncate {n : Int} (h₁ : -2 ^ (System.Platform.numBits - 1) ≤ n)
|
||||
(h₂ : n < 2 ^ (System.Platform.numBits - 1)) : (ISize.ofIntTruncate n).toInt16 = Int16.ofInt n := by
|
||||
rw [← ofIntLE_eq_ofIntTruncate, toInt16_ofIntLE]
|
||||
· exact toInt_minValue ▸ h₁
|
||||
· rw [toInt_maxValue]
|
||||
omega
|
||||
|
||||
theorem Int64.toInt32_ofIntLE {n} (h₁ h₂) : (Int64.ofIntLE n h₁ h₂).toInt32 = Int32.ofInt n := Int32.toInt.inj (by simp)
|
||||
theorem ISize.toInt32_ofIntLE {n} (h₁ h₂) : (ISize.ofIntLE n h₁ h₂).toInt32 = Int32.ofInt n := Int32.toInt.inj (by simp)
|
||||
|
||||
@[simp] theorem Int64.toInt32_ofBitVec (b) : (Int64.ofBitVec b).toInt32 = Int32.ofBitVec (b.signExtend _) := rfl
|
||||
@[simp] theorem ISize.toInt32_ofBitVec (b) : (ISize.ofBitVec b).toInt32 = Int32.ofBitVec (b.signExtend _) := rfl
|
||||
|
||||
@[simp] theorem Int64.toInt32_ofNat' {n} : (Int64.ofNat n).toInt32 = Int32.ofNat n :=
|
||||
Int32.toBitVec.inj (by simp [BitVec.signExtend_eq_setWidth_of_le])
|
||||
@[simp] theorem ISize.toInt32_ofNat' {n} : (ISize.ofNat n).toInt32 = Int32.ofNat n := by
|
||||
apply Int32.toBitVec.inj
|
||||
simp only [toBitVec_toInt32, toBitVec_ofNat', Int32.toBitVec_ofNat']
|
||||
rw [BitVec.signExtend_eq_setWidth_of_le, BitVec.setWidth_ofNat_of_le]
|
||||
all_goals cases System.Platform.numBits_eq <;> simp_all
|
||||
|
||||
@[simp] theorem Int64.toInt32_ofInt {n} : (Int64.ofInt n).toInt32 = Int32.ofInt n :=
|
||||
Int32.toInt.inj (by simpa using Int.bmod_bmod_of_dvd (by decide))
|
||||
@[simp] theorem ISize.toInt32_ofInt {n} : (ISize.ofInt n).toInt32 = Int32.ofInt n := by
|
||||
apply Int32.toInt.inj
|
||||
simp only [toInt_toInt32, toInt_ofInt, Nat.reducePow, Int32.toInt_ofInt]
|
||||
exact Int.bmod_bmod_of_dvd UInt32.size_dvd_usizeSize
|
||||
|
||||
@[simp] theorem Int64.toInt32_ofNat {n} : toInt32 (no_index (OfNat.ofNat n)) = OfNat.ofNat n := toInt32_ofNat'
|
||||
@[simp] theorem ISize.toInt32_ofNat {n} : toInt32 (no_index (OfNat.ofNat n)) = OfNat.ofNat n := toInt32_ofNat'
|
||||
|
||||
theorem Int64.toInt32_ofIntTruncate {n : Int} (h₁ : -2 ^ 63 ≤ n) (h₂ : n < 2 ^ 63) :
|
||||
(Int64.ofIntTruncate n).toInt32 = Int32.ofInt n := by
|
||||
rw [← ofIntLE_eq_ofIntTruncate (h₁ := h₁) (h₂ := Int.le_of_lt_add_one h₂), toInt32_ofIntLE]
|
||||
theorem ISize.toInt32_ofIntTruncate {n : Int} (h₁ : -2 ^ (System.Platform.numBits - 1) ≤ n)
|
||||
(h₂ : n < 2 ^ (System.Platform.numBits - 1)) : (ISize.ofIntTruncate n).toInt32 = Int32.ofInt n := by
|
||||
rw [← ofIntLE_eq_ofIntTruncate, toInt32_ofIntLE]
|
||||
· exact toInt_minValue ▸ h₁
|
||||
· rw [toInt_maxValue]
|
||||
omega
|
||||
|
||||
theorem Int64.toISize_ofIntLE {n} (h₁ h₂) : (Int64.ofIntLE n h₁ h₂).toISize = ISize.ofInt n :=
|
||||
ISize.toInt.inj (by simp [ISize.toInt_ofInt])
|
||||
|
||||
@[simp] theorem Int64.toISize_ofBitVec (b) : (Int64.ofBitVec b).toISize = ISize.ofBitVec (b.signExtend _) := rfl
|
||||
|
||||
@[simp] theorem Int64.toISize_ofNat' {n} : (Int64.ofNat n).toISize = ISize.ofNat n :=
|
||||
ISize.toBitVec.inj (by simp [BitVec.signExtend_eq_setWidth_of_le])
|
||||
|
||||
@[simp] theorem Int64.toISize_ofInt {n} : (Int64.ofInt n).toISize = ISize.ofInt n :=
|
||||
ISize.toInt.inj (by simpa [ISize.toInt_ofInt] using Int.bmod_bmod_of_dvd USize.size_dvd_uInt64Size)
|
||||
|
||||
@[simp] theorem Int64.toISize_ofNat {n} : toISize (no_index (OfNat.ofNat n)) = OfNat.ofNat n := toISize_ofNat'
|
||||
|
||||
theorem Int64.toISize_ofIntTruncate {n : Int} (h₁ : -2 ^ 63 ≤ n) (h₂ : n < 2 ^ 63) :
|
||||
(Int64.ofIntTruncate n).toISize = ISize.ofInt n := by
|
||||
rw [← ofIntLE_eq_ofIntTruncate (h₁ := h₁) (h₂ := Int.le_of_lt_add_one h₂), toISize_ofIntLE]
|
||||
|
||||
@[simp] theorem Int8.toBitVec_minValue : minValue.toBitVec = BitVec.intMin _ := rfl
|
||||
@[simp] theorem Int16.toBitVec_minValue : minValue.toBitVec = BitVec.intMin _ := rfl
|
||||
@[simp] theorem Int32.toBitVec_minValue : minValue.toBitVec = BitVec.intMin _ := rfl
|
||||
@[simp] theorem Int64.toBitVec_minValue : minValue.toBitVec = BitVec.intMin _ := rfl
|
||||
@[simp] theorem ISize.toBitVec_minValue : minValue.toBitVec = BitVec.intMin _ :=
|
||||
BitVec.eq_of_toInt_eq (by rw [toInt_toBitVec, toInt_minValue,
|
||||
BitVec.toInt_intMin_of_pos (by cases System.Platform.numBits_eq <;> simp_all)])
|
||||
|
||||
@[simp] theorem Int16.toInt8_neg (x : Int16) : (-x).toInt8 = -x.toInt8 := Int8.toBitVec.inj (by simp)
|
||||
@[simp] theorem Int32.toInt8_neg (x : Int32) : (-x).toInt8 = -x.toInt8 := Int8.toBitVec.inj (by simp)
|
||||
@[simp] theorem Int64.toInt8_neg (x : Int64) : (-x).toInt8 = -x.toInt8 := Int8.toBitVec.inj (by simp)
|
||||
@[simp] theorem ISize.toInt8_neg (x : ISize) : (-x).toInt8 = -x.toInt8 :=
|
||||
Int8.toBitVec.inj (by rw [toBitVec_toInt8, toBitVec_neg, Int8.toBitVec_neg, toBitVec_toInt8,
|
||||
BitVec.signExtend_neg_of_le (by cases System.Platform.numBits_eq <;> simp_all)])
|
||||
|
||||
@[simp] theorem Int32.toInt16_neg (x : Int32) : (-x).toInt16 = -x.toInt16 := Int16.toBitVec.inj (by simp)
|
||||
@[simp] theorem Int64.toInt16_neg (x : Int64) : (-x).toInt16 = -x.toInt16 := Int16.toBitVec.inj (by simp)
|
||||
@[simp] theorem ISize.toInt16_neg (x : ISize) : (-x).toInt16 = -x.toInt16 :=
|
||||
Int16.toBitVec.inj (by rw [toBitVec_toInt16, toBitVec_neg, Int16.toBitVec_neg, toBitVec_toInt16,
|
||||
BitVec.signExtend_neg_of_le (by cases System.Platform.numBits_eq <;> simp_all)])
|
||||
|
||||
@[simp] theorem Int64.toInt32_neg (x : Int64) : (-x).toInt32 = -x.toInt32 := Int32.toBitVec.inj (by simp)
|
||||
@[simp] theorem ISize.toInt32_neg (x : ISize) : (-x).toInt32 = -x.toInt32 :=
|
||||
Int32.toBitVec.inj (by rw [toBitVec_toInt32, toBitVec_neg, Int32.toBitVec_neg, toBitVec_toInt32,
|
||||
BitVec.signExtend_neg_of_le (by cases System.Platform.numBits_eq <;> simp_all)])
|
||||
|
||||
@[simp] theorem Int64.toISize_neg (x : Int64) : (-x).toISize = -x.toISize := ISize.toBitVec.inj (by simp)
|
||||
|
||||
@[simp] theorem Int8.toInt16_neg_of_ne {x : Int8} (hx : x ≠ -128) : (-x).toInt16 = -x.toInt16 :=
|
||||
Int16.toBitVec.inj (BitVec.signExtend_neg_of_ne_intMin _ (fun h => hx (Int8.toBitVec.inj h)))
|
||||
|
||||
@[simp] theorem Int8.toInt32_neg_of_ne {x : Int8} (hx : x ≠ -128) : (-x).toInt32 = -x.toInt32 :=
|
||||
Int32.toBitVec.inj (BitVec.signExtend_neg_of_ne_intMin _ (fun h => hx (Int8.toBitVec.inj h)))
|
||||
@[simp] theorem Int16.toInt32_neg_of_ne {x : Int16} (hx : x ≠ -32768) : (-x).toInt32 = -x.toInt32 :=
|
||||
Int32.toBitVec.inj (BitVec.signExtend_neg_of_ne_intMin _ (fun h => hx (Int16.toBitVec.inj h)))
|
||||
|
||||
@[simp] theorem Int8.toISize_neg_of_ne {x : Int8} (hx : x ≠ -128) : (-x).toISize = -x.toISize :=
|
||||
ISize.toBitVec.inj (BitVec.signExtend_neg_of_ne_intMin _ (fun h => hx (Int8.toBitVec.inj h)))
|
||||
@[simp] theorem Int16.toISize_neg_of_ne {x : Int16} (hx : x ≠ -32768) : (-x).toISize = -x.toISize :=
|
||||
ISize.toBitVec.inj (BitVec.signExtend_neg_of_ne_intMin _ (fun h => hx (Int16.toBitVec.inj h)))
|
||||
@[simp] theorem Int32.toISize_neg_of_ne {x : Int32} (hx : x ≠ -2147483648) : (-x).toISize = -x.toISize :=
|
||||
ISize.toBitVec.inj (BitVec.signExtend_neg_of_ne_intMin _ (fun h => hx (Int32.toBitVec.inj h)))
|
||||
|
||||
@[simp] theorem Int8.toInt64_neg_of_ne {x : Int8} (hx : x ≠ -128) : (-x).toInt64 = -x.toInt64 :=
|
||||
Int64.toBitVec.inj (BitVec.signExtend_neg_of_ne_intMin _ (fun h => hx (Int8.toBitVec.inj h)))
|
||||
@[simp] theorem Int16.toInt64_neg_of_ne {x : Int16} (hx : x ≠ -32768) : (-x).toInt64 = -x.toInt64 :=
|
||||
Int64.toBitVec.inj (BitVec.signExtend_neg_of_ne_intMin _ (fun h => hx (Int16.toBitVec.inj h)))
|
||||
@[simp] theorem Int32.toInt64_neg_of_ne {x : Int32} (hx : x ≠ -2147483648) : (-x).toInt64 = -x.toInt64 :=
|
||||
Int64.toBitVec.inj (BitVec.signExtend_neg_of_ne_intMin _ (fun h => hx (Int32.toBitVec.inj h)))
|
||||
@[simp] theorem ISize.toInt64_neg_of_ne {x : ISize} (hx : x ≠ minValue) : (-x).toInt64 = -x.toInt64 :=
|
||||
Int64.toBitVec.inj (BitVec.signExtend_neg_of_ne_intMin _
|
||||
(fun h => hx (ISize.toBitVec.inj (h.trans toBitVec_minValue.symm))))
|
||||
|
||||
theorem Int8.toInt16_ofIntLE {n : Int} (h₁ h₂) :
|
||||
(Int8.ofIntLE n h₁ h₂).toInt16 = Int16.ofIntLE n (Int.le_trans (by decide) h₁) (Int.le_trans h₂ (by decide)) :=
|
||||
Int16.toInt.inj (by simp)
|
||||
theorem Int8.toInt32_ofIntLE {n : Int} (h₁ h₂) :
|
||||
(Int8.ofIntLE n h₁ h₂).toInt32 = Int32.ofIntLE n (Int.le_trans (by decide) h₁) (Int.le_trans h₂ (by decide)) :=
|
||||
Int32.toInt.inj (by simp)
|
||||
theorem Int8.toInt64_ofIntLE {n : Int} (h₁ h₂) :
|
||||
(Int8.ofIntLE n h₁ h₂).toInt64 = Int64.ofIntLE n (Int.le_trans (by decide) h₁) (Int.le_trans h₂ (by decide)) :=
|
||||
Int64.toInt.inj (by simp)
|
||||
theorem Int8.toISize_ofIntLE {n : Int} (h₁ h₂) :
|
||||
(Int8.ofIntLE n h₁ h₂).toISize = ISize.ofIntLE n (Int.le_trans minValue.iSizeMinValue_le_toInt h₁)
|
||||
(Int.le_trans h₂ maxValue.toInt_le_iSizeMaxValue) :=
|
||||
ISize.toInt.inj (by simp)
|
||||
|
||||
@[simp] theorem Int8.toInt16_ofBitVec (b) : (Int8.ofBitVec b).toInt16 = Int16.ofBitVec (b.signExtend _) := rfl
|
||||
@[simp] theorem Int8.toInt32_ofBitVec (b) : (Int8.ofBitVec b).toInt32 = Int32.ofBitVec (b.signExtend _) := rfl
|
||||
@[simp] theorem Int8.toInt64_ofBitVec (b) : (Int8.ofBitVec b).toInt64 = Int64.ofBitVec (b.signExtend _) := rfl
|
||||
@[simp] theorem Int8.toISize_ofBitVec (b) : (Int8.ofBitVec b).toISize = ISize.ofBitVec (b.signExtend _) := rfl
|
||||
|
||||
@[simp] theorem Int8.toInt16_ofInt {n : Int} (h₁ : Int8.minValue.toInt ≤ n) (h₂ : n ≤ Int8.maxValue.toInt) :
|
||||
(Int8.ofInt n).toInt16 = Int16.ofInt n := by rw [← Int8.ofIntLE_eq_ofInt h₁ h₂, toInt16_ofIntLE, Int16.ofIntLE_eq_ofInt]
|
||||
@[simp] theorem Int8.toInt32_ofInt {n : Int} (h₁ : Int8.minValue.toInt ≤ n) (h₂ : n ≤ Int8.maxValue.toInt) :
|
||||
(Int8.ofInt n).toInt32 = Int32.ofInt n := by rw [← Int8.ofIntLE_eq_ofInt h₁ h₂, toInt32_ofIntLE, Int32.ofIntLE_eq_ofInt]
|
||||
@[simp] theorem Int8.toInt64_ofInt {n : Int} (h₁ : Int8.minValue.toInt ≤ n) (h₂ : n ≤ Int8.maxValue.toInt) :
|
||||
(Int8.ofInt n).toInt64 = Int64.ofInt n := by rw [← Int8.ofIntLE_eq_ofInt h₁ h₂, toInt64_ofIntLE, Int64.ofIntLE_eq_ofInt]
|
||||
@[simp] theorem Int8.toISize_ofInt {n : Int} (h₁ : Int8.minValue.toInt ≤ n) (h₂ : n ≤ Int8.maxValue.toInt) :
|
||||
(Int8.ofInt n).toISize = ISize.ofInt n := by rw [← Int8.ofIntLE_eq_ofInt h₁ h₂, toISize_ofIntLE, ISize.ofIntLE_eq_ofInt]
|
||||
|
||||
@[simp] theorem Int8.toInt16_ofNat' {n : Nat} (h : n ≤ Int8.maxValue.toInt) :
|
||||
(Int8.ofNat n).toInt16 = Int16.ofNat n := by
|
||||
rw [← ofInt_eq_ofNat, toInt16_ofInt (by simp [toInt_minValue]) h, Int16.ofInt_eq_ofNat]
|
||||
@[simp] theorem Int8.toInt32_ofNat' {n : Nat} (h : n ≤ Int8.maxValue.toInt) :
|
||||
(Int8.ofNat n).toInt32 = Int32.ofNat n := by
|
||||
rw [← ofInt_eq_ofNat, toInt32_ofInt (by simp [toInt_minValue]) h, Int32.ofInt_eq_ofNat]
|
||||
@[simp] theorem Int8.toInt64_ofNat' {n : Nat} (h : n ≤ Int8.maxValue.toInt) :
|
||||
(Int8.ofNat n).toInt64 = Int64.ofNat n := by
|
||||
rw [← ofInt_eq_ofNat, toInt64_ofInt (by simp [toInt_minValue]) h, Int64.ofInt_eq_ofNat]
|
||||
@[simp] theorem Int8.toISize_ofNat' {n : Nat} (h : n ≤ Int8.maxValue.toInt) :
|
||||
(Int8.ofNat n).toISize = ISize.ofNat n := by
|
||||
rw [← ofInt_eq_ofNat, toISize_ofInt (by simp [toInt_minValue]) h, ISize.ofInt_eq_ofNat]
|
||||
|
||||
@[simp] theorem Int8.toInt16_ofNat {n : Nat} (h : n ≤ 127) :
|
||||
toInt16 (no_index (OfNat.ofNat n)) = OfNat.ofNat n := Int8.toInt16_ofNat' (by rw [toInt_maxValue]; omega)
|
||||
@[simp] theorem Int8.toInt32_ofNat {n : Nat} (h : n ≤ 127) :
|
||||
toInt32 (no_index (OfNat.ofNat n)) = OfNat.ofNat n := Int8.toInt32_ofNat' (by rw [toInt_maxValue]; omega)
|
||||
@[simp] theorem Int8.toInt64_ofNat {n : Nat} (h : n ≤ 127) :
|
||||
toInt64 (no_index (OfNat.ofNat n)) = OfNat.ofNat n := Int8.toInt64_ofNat' (by rw [toInt_maxValue]; omega)
|
||||
@[simp] theorem Int8.toISize_ofNat {n : Nat} (h : n ≤ 127) :
|
||||
toISize (no_index (OfNat.ofNat n)) = OfNat.ofNat n := Int8.toISize_ofNat' (by rw [toInt_maxValue]; omega)
|
||||
|
||||
theorem Int16.toInt32_ofIntLE {n : Int} (h₁ h₂) :
|
||||
(Int16.ofIntLE n h₁ h₂).toInt32 = Int32.ofIntLE n (Int.le_trans (by decide) h₁) (Int.le_trans h₂ (by decide)) :=
|
||||
Int32.toInt.inj (by simp)
|
||||
theorem Int16.toInt64_ofIntLE {n : Int} (h₁ h₂) :
|
||||
(Int16.ofIntLE n h₁ h₂).toInt64 = Int64.ofIntLE n (Int.le_trans (by decide) h₁) (Int.le_trans h₂ (by decide)) :=
|
||||
Int64.toInt.inj (by simp)
|
||||
theorem Int16.toISize_ofIntLE {n : Int} (h₁ h₂) :
|
||||
(Int16.ofIntLE n h₁ h₂).toISize = ISize.ofIntLE n (Int.le_trans minValue.iSizeMinValue_le_toInt h₁)
|
||||
(Int.le_trans h₂ maxValue.toInt_le_iSizeMaxValue) :=
|
||||
ISize.toInt.inj (by simp)
|
||||
|
||||
@[simp] theorem Int16.toInt32_ofBitVec (b) : (Int16.ofBitVec b).toInt32 = Int32.ofBitVec (b.signExtend _) := rfl
|
||||
@[simp] theorem Int16.toInt64_ofBitVec (b) : (Int16.ofBitVec b).toInt64 = Int64.ofBitVec (b.signExtend _) := rfl
|
||||
@[simp] theorem Int16.toISize_ofBitVec (b) : (Int16.ofBitVec b).toISize = ISize.ofBitVec (b.signExtend _) := rfl
|
||||
|
||||
@[simp] theorem Int16.toInt32_ofInt {n : Int} (h₁ : Int16.minValue.toInt ≤ n) (h₂ : n ≤ Int16.maxValue.toInt) :
|
||||
(Int16.ofInt n).toInt32 = Int32.ofInt n := by rw [← Int16.ofIntLE_eq_ofInt h₁ h₂, toInt32_ofIntLE, Int32.ofIntLE_eq_ofInt]
|
||||
@[simp] theorem Int16.toInt64_ofInt {n : Int} (h₁ : Int16.minValue.toInt ≤ n) (h₂ : n ≤ Int16.maxValue.toInt) :
|
||||
(Int16.ofInt n).toInt64 = Int64.ofInt n := by rw [← Int16.ofIntLE_eq_ofInt h₁ h₂, toInt64_ofIntLE, Int64.ofIntLE_eq_ofInt]
|
||||
@[simp] theorem Int16.toISize_ofInt {n : Int} (h₁ : Int16.minValue.toInt ≤ n) (h₂ : n ≤ Int16.maxValue.toInt) :
|
||||
(Int16.ofInt n).toISize = ISize.ofInt n := by rw [← Int16.ofIntLE_eq_ofInt h₁ h₂, toISize_ofIntLE, ISize.ofIntLE_eq_ofInt]
|
||||
|
||||
@[simp] theorem Int16.toInt32_ofNat' {n : Nat} (h : n ≤ Int16.maxValue.toInt) :
|
||||
(Int16.ofNat n).toInt32 = Int32.ofNat n := by
|
||||
rw [← ofInt_eq_ofNat, toInt32_ofInt (by simp [toInt_minValue]) h, Int32.ofInt_eq_ofNat]
|
||||
@[simp] theorem Int16.toInt64_ofNat' {n : Nat} (h : n ≤ Int16.maxValue.toInt) :
|
||||
(Int16.ofNat n).toInt64 = Int64.ofNat n := by
|
||||
rw [← ofInt_eq_ofNat, toInt64_ofInt (by simp [toInt_minValue]) h, Int64.ofInt_eq_ofNat]
|
||||
@[simp] theorem Int16.toISize_ofNat' {n : Nat} (h : n ≤ Int16.maxValue.toInt) :
|
||||
(Int16.ofNat n).toISize = ISize.ofNat n := by
|
||||
rw [← ofInt_eq_ofNat, toISize_ofInt (by simp [toInt_minValue]) h, ISize.ofInt_eq_ofNat]
|
||||
|
||||
@[simp] theorem Int16.toInt32_ofNat {n : Nat} (h : n ≤ 32767) :
|
||||
toInt32 (no_index (OfNat.ofNat n)) = OfNat.ofNat n := Int16.toInt32_ofNat' (by rw [toInt_maxValue]; omega)
|
||||
@[simp] theorem Int16.toInt64_ofNat {n : Nat} (h : n ≤ 32767) :
|
||||
toInt64 (no_index (OfNat.ofNat n)) = OfNat.ofNat n := Int16.toInt64_ofNat' (by rw [toInt_maxValue]; omega)
|
||||
@[simp] theorem Int16.toISize_ofNat {n : Nat} (h : n ≤ 32767) :
|
||||
toISize (no_index (OfNat.ofNat n)) = OfNat.ofNat n := Int16.toISize_ofNat' (by rw [toInt_maxValue]; omega)
|
||||
|
||||
theorem Int32.toInt64_ofIntLE {n : Int} (h₁ h₂) :
|
||||
(Int32.ofIntLE n h₁ h₂).toInt64 = Int64.ofIntLE n (Int.le_trans (by decide) h₁) (Int.le_trans h₂ (by decide)) :=
|
||||
Int64.toInt.inj (by simp)
|
||||
theorem Int32.toISize_ofIntLE {n : Int} (h₁ h₂) :
|
||||
(Int32.ofIntLE n h₁ h₂).toISize = ISize.ofIntLE n (Int.le_trans minValue.iSizeMinValue_le_toInt h₁)
|
||||
(Int.le_trans h₂ maxValue.toInt_le_iSizeMaxValue) :=
|
||||
ISize.toInt.inj (by simp)
|
||||
|
||||
@[simp] theorem Int32.toInt64_ofBitVec (b) : (Int32.ofBitVec b).toInt64 = Int64.ofBitVec (b.signExtend _) := rfl
|
||||
@[simp] theorem Int32.toISize_ofBitVec (b) : (Int32.ofBitVec b).toISize = ISize.ofBitVec (b.signExtend _) := rfl
|
||||
|
||||
@[simp] theorem Int32.toInt64_ofInt {n : Int} (h₁ : Int32.minValue.toInt ≤ n) (h₂ : n ≤ Int32.maxValue.toInt) :
|
||||
(Int32.ofInt n).toInt64 = Int64.ofInt n := by rw [← Int32.ofIntLE_eq_ofInt h₁ h₂, toInt64_ofIntLE, Int64.ofIntLE_eq_ofInt]
|
||||
@[simp] theorem Int32.toISize_ofInt {n : Int} (h₁ : Int32.minValue.toInt ≤ n) (h₂ : n ≤ Int32.maxValue.toInt) :
|
||||
(Int32.ofInt n).toISize = ISize.ofInt n := by rw [← Int32.ofIntLE_eq_ofInt h₁ h₂, toISize_ofIntLE, ISize.ofIntLE_eq_ofInt]
|
||||
|
||||
@[simp] theorem Int32.toInt64_ofNat' {n : Nat} (h : n ≤ Int32.maxValue.toInt) :
|
||||
(Int32.ofNat n).toInt64 = Int64.ofNat n := by
|
||||
rw [← ofInt_eq_ofNat, toInt64_ofInt (by simp [toInt_minValue]) h, Int64.ofInt_eq_ofNat]
|
||||
@[simp] theorem Int32.toISize_ofNat' {n : Nat} (h : n ≤ Int32.maxValue.toInt) :
|
||||
(Int32.ofNat n).toISize = ISize.ofNat n := by
|
||||
rw [← ofInt_eq_ofNat, toISize_ofInt (by simp [toInt_minValue]) h, ISize.ofInt_eq_ofNat]
|
||||
|
||||
@[simp] theorem Int32.toInt64_ofNat {n : Nat} (h : n ≤ 2147483647) :
|
||||
toInt64 (no_index (OfNat.ofNat n)) = OfNat.ofNat n := Int32.toInt64_ofNat' (by rw [toInt_maxValue]; omega)
|
||||
@[simp] theorem Int32.toISize_ofNat {n : Nat} (h : n ≤ 2147483647) :
|
||||
toISize (no_index (OfNat.ofNat n)) = OfNat.ofNat n := Int32.toISize_ofNat' (by rw [toInt_maxValue]; omega)
|
||||
|
||||
theorem ISize.toInt64_ofIntLE {n : Int} (h₁ h₂) :
|
||||
(ISize.ofIntLE n h₁ h₂).toInt64 = Int64.ofIntLE n (Int.le_trans minValue.int64MinValue_le_toInt h₁)
|
||||
(Int.le_trans h₂ maxValue.toInt_le_int64MaxValue) :=
|
||||
Int64.toInt.inj (by simp)
|
||||
|
||||
@[simp] theorem ISize.toInt64_ofBitVec (b) : (ISize.ofBitVec b).toInt64 = Int64.ofBitVec (b.signExtend _) := rfl
|
||||
|
||||
@[simp] theorem ISize.toInt64_ofInt {n : Int} (h₁ : ISize.minValue.toInt ≤ n) (h₂ : n ≤ ISize.maxValue.toInt) :
|
||||
(ISize.ofInt n).toInt64 = Int64.ofInt n := by rw [← ISize.ofIntLE_eq_ofInt h₁ h₂, toInt64_ofIntLE, Int64.ofIntLE_eq_ofInt]
|
||||
|
||||
@[simp] theorem ISize.toInt64_ofNat' {n : Nat} (h : n ≤ ISize.maxValue.toInt) :
|
||||
(ISize.ofNat n).toInt64 = Int64.ofNat n := by
|
||||
rw [← ofInt_eq_ofNat, toInt64_ofInt _ h, Int64.ofInt_eq_ofNat]
|
||||
refine Int.le_trans ?_ (Int.zero_le_ofNat _)
|
||||
cases System.Platform.numBits_eq <;> simp_all
|
||||
|
||||
@[simp] theorem ISize.toInt64_ofNat {n : Nat} (h : n ≤ 2147483647) :
|
||||
toInt64 (no_index (OfNat.ofNat n)) = OfNat.ofNat n :=
|
||||
ISize.toInt64_ofNat' (by rw [toInt_maxValue]; cases System.Platform.numBits_eq <;> simp_all <;> omega)
|
||||
|
|
|
|||
|
|
@ -1205,3 +1205,51 @@ theorem USize.toUInt64_ofNatTruncate_of_lt {n : Nat} (hn : n < USize.size) :
|
|||
theorem USize.toUInt64_ofNatTruncate_of_le {n : Nat} (hn : USize.size ≤ n) :
|
||||
(USize.ofNatTruncate n).toUInt64 = UInt64.ofNatLT (USize.size - 1) (by cases USize.size_eq <;> simp_all +decide) :=
|
||||
UInt64.toNat.inj (by simp [toNat_ofNatTruncate_of_le hn])
|
||||
|
||||
@[simp] theorem UInt8.toUInt16_ofNat' {n : Nat} (hn : n < UInt8.size) : (UInt8.ofNat n).toUInt16 = UInt16.ofNat n := by
|
||||
rw [← UInt8.ofNatLT_eq_ofNat (h := hn), toUInt16_ofNatLT, UInt16.ofNatLT_eq_ofNat]
|
||||
@[simp] theorem UInt8.toUInt32_ofNat' {n : Nat} (hn : n < UInt8.size) : (UInt8.ofNat n).toUInt32 = UInt32.ofNat n := by
|
||||
rw [← UInt8.ofNatLT_eq_ofNat (h := hn), toUInt32_ofNatLT, UInt32.ofNatLT_eq_ofNat]
|
||||
@[simp] theorem UInt8.toUInt64_ofNat' {n : Nat} (hn : n < UInt8.size) : (UInt8.ofNat n).toUInt64 = UInt64.ofNat n := by
|
||||
rw [← UInt8.ofNatLT_eq_ofNat (h := hn), toUInt64_ofNatLT, UInt64.ofNatLT_eq_ofNat]
|
||||
@[simp] theorem UInt8.toUSize_ofNat' {n : Nat} (hn : n < UInt8.size) : (UInt8.ofNat n).toUSize = USize.ofNat n := by
|
||||
rw [← UInt8.ofNatLT_eq_ofNat (h := hn), toUSize_ofNatLT, USize.ofNatLT_eq_ofNat]
|
||||
|
||||
@[simp] theorem UInt16.toUInt32_ofNat' {n : Nat} (hn : n < UInt16.size) : (UInt16.ofNat n).toUInt32 = UInt32.ofNat n := by
|
||||
rw [← UInt16.ofNatLT_eq_ofNat (h := hn), toUInt32_ofNatLT, UInt32.ofNatLT_eq_ofNat]
|
||||
@[simp] theorem UInt16.toUInt64_ofNat' {n : Nat} (hn : n < UInt16.size) : (UInt16.ofNat n).toUInt64 = UInt64.ofNat n := by
|
||||
rw [← UInt16.ofNatLT_eq_ofNat (h := hn), toUInt64_ofNatLT, UInt64.ofNatLT_eq_ofNat]
|
||||
@[simp] theorem UInt16.toUSize_ofNat' {n : Nat} (hn : n < UInt16.size) : (UInt16.ofNat n).toUSize = USize.ofNat n := by
|
||||
rw [← UInt16.ofNatLT_eq_ofNat (h := hn), toUSize_ofNatLT, USize.ofNatLT_eq_ofNat]
|
||||
|
||||
@[simp] theorem UInt32.toUInt64_ofNat' {n : Nat} (hn : n < UInt32.size) : (UInt32.ofNat n).toUInt64 = UInt64.ofNat n := by
|
||||
rw [← UInt32.ofNatLT_eq_ofNat (h := hn), toUInt64_ofNatLT, UInt64.ofNatLT_eq_ofNat]
|
||||
@[simp] theorem UInt32.toUSize_ofNat' {n : Nat} (hn : n < UInt32.size) : (UInt32.ofNat n).toUSize = USize.ofNat n := by
|
||||
rw [← UInt32.ofNatLT_eq_ofNat (h := hn), toUSize_ofNatLT, USize.ofNatLT_eq_ofNat]
|
||||
|
||||
@[simp] theorem USize.toUInt64_ofNat' {n : Nat} (hn : n < USize.size) : (USize.ofNat n).toUInt64 = UInt64.ofNat n := by
|
||||
rw [← USize.ofNatLT_eq_ofNat (h := hn), toUInt64_ofNatLT, UInt64.ofNatLT_eq_ofNat]
|
||||
|
||||
@[simp] theorem UInt8.toUInt16_ofNat {n : Nat} (hn : n < 256) : toUInt16 (no_index (OfNat.ofNat n)) = OfNat.ofNat n :=
|
||||
UInt8.toUInt16_ofNat' hn
|
||||
@[simp] theorem UInt8.toUInt32_ofNat {n : Nat} (hn : n < 256) : toUInt32 (no_index (OfNat.ofNat n)) = OfNat.ofNat n :=
|
||||
UInt8.toUInt32_ofNat' hn
|
||||
@[simp] theorem UInt8.toUInt64_ofNat {n : Nat} (hn : n < 256) : toUInt64 (no_index (OfNat.ofNat n)) = OfNat.ofNat n :=
|
||||
UInt8.toUInt64_ofNat' hn
|
||||
@[simp] theorem UInt8.toUSize_ofNat {n : Nat} (hn : n < 256) : toUSize (no_index (OfNat.ofNat n)) = OfNat.ofNat n :=
|
||||
UInt8.toUSize_ofNat' hn
|
||||
|
||||
@[simp] theorem UInt16.toUInt32_ofNat {n : Nat} (hn : n < 65536) : toUInt32 (no_index (OfNat.ofNat n)) = OfNat.ofNat n :=
|
||||
UInt16.toUInt32_ofNat' hn
|
||||
@[simp] theorem UInt16.toUInt64_ofNat {n : Nat} (hn : n < 65536) : toUInt64 (no_index (OfNat.ofNat n)) = OfNat.ofNat n :=
|
||||
UInt16.toUInt64_ofNat' hn
|
||||
@[simp] theorem UInt16.toUSize_ofNat {n : Nat} (hn : n < 65536) : toUSize (no_index (OfNat.ofNat n)) = OfNat.ofNat n :=
|
||||
UInt16.toUSize_ofNat' hn
|
||||
|
||||
@[simp] theorem UInt32.toUInt64_ofNat {n : Nat} (hn : n < 4294967296) : toUInt64 (no_index (OfNat.ofNat n)) = OfNat.ofNat n :=
|
||||
UInt32.toUInt64_ofNat' hn
|
||||
@[simp] theorem UInt32.toUSize_ofNat {n : Nat} (hn : n < 4294967296) : toUSize (no_index (OfNat.ofNat n)) = OfNat.ofNat n :=
|
||||
UInt32.toUSize_ofNat' hn
|
||||
|
||||
@[simp] theorem USize.toUInt64_ofNat {n : Nat} (hn : n < 4294967296) : toUInt64 (no_index (OfNat.ofNat n)) = OfNat.ofNat n :=
|
||||
USize.toUInt64_ofNat' (Nat.lt_of_lt_of_le hn UInt32.size_le_usizeSize)
|
||||
|
|
|
|||
|
|
@ -26,9 +26,11 @@ def target : String := getTarget ()
|
|||
theorem numBits_pos : 0 < numBits := by
|
||||
cases numBits_eq <;> next h => simp [h]
|
||||
|
||||
@[simp]
|
||||
theorem le_numBits : 32 ≤ numBits := by
|
||||
cases numBits_eq <;> next h => simp [h]
|
||||
|
||||
@[simp]
|
||||
theorem numBits_le : numBits ≤ 64 := by
|
||||
cases numBits_eq <;> next h => simp [h]
|
||||
|
||||
|
|
|
|||
73
tests/lean/run/simpSInt.lean
Normal file
73
tests/lean/run/simpSInt.lean
Normal file
|
|
@ -0,0 +1,73 @@
|
|||
#check_simp (-64 : Int8).toBitVec ~> 192#8
|
||||
#check_simp (-64 : Int16).toBitVec ~> 65472#16
|
||||
#check_simp (-64 : Int32).toBitVec ~> 4294967232#32
|
||||
#check_simp (-64 : Int64).toBitVec ~> 18446744073709551552#64
|
||||
|
||||
#check_simp (64 : UInt8).toUInt16 ~> 64
|
||||
#check_simp (64 : UInt8).toUInt32 ~> 64
|
||||
#check_simp (64 : UInt8).toUInt64 ~> 64
|
||||
#check_simp (64 : UInt8).toUSize ~> 64
|
||||
|
||||
#check_simp (64 : UInt16).toUInt8 ~> 64
|
||||
#check_simp (64 : UInt16).toUInt32 ~> 64
|
||||
#check_simp (64 : UInt16).toUInt64 ~> 64
|
||||
#check_simp (64 : UInt16).toUSize ~> 64
|
||||
|
||||
#check_simp (64 : UInt32).toUInt8 ~> 64
|
||||
#check_simp (64 : UInt32).toUInt16 ~> 64
|
||||
#check_simp (64 : UInt32).toUInt64 ~> 64
|
||||
#check_simp (64 : UInt32).toUSize ~> 64
|
||||
|
||||
#check_simp (64 : UInt64).toUInt8 ~> 64
|
||||
#check_simp (64 : UInt64).toUInt16 ~> 64
|
||||
#check_simp (64 : UInt64).toUInt32 ~> 64
|
||||
#check_simp (64 : UInt64).toUSize ~> 64
|
||||
|
||||
#check_simp (64 : USize).toUInt8 ~> 64
|
||||
#check_simp (64 : USize).toUInt16 ~> 64
|
||||
#check_simp (64 : USize).toUInt32 ~> 64
|
||||
|
||||
#check_simp (-64 : Int8).toInt16 ~> -64
|
||||
#check_simp (-64 : Int8).toInt32 ~> -64
|
||||
#check_simp (-64 : Int8).toInt64 ~> -64
|
||||
#check_simp (-64 : Int8).toISize ~> -64
|
||||
|
||||
#check_simp (-64 : Int16).toInt8 ~> -64
|
||||
#check_simp (-64 : Int16).toInt32 ~> -64
|
||||
#check_simp (-64 : Int16).toInt64 ~> -64
|
||||
#check_simp (-64 : Int16).toISize ~> -64
|
||||
|
||||
#check_simp (-64 : Int32).toInt8 ~> -64
|
||||
#check_simp (-64 : Int32).toInt16 ~> -64
|
||||
#check_simp (-64 : Int32).toInt64 ~> -64
|
||||
#check_simp (-64 : Int32).toISize ~> -64
|
||||
|
||||
#check_simp (-64 : Int64).toInt8 ~> -64
|
||||
#check_simp (-64 : Int64).toInt16 ~> -64
|
||||
#check_simp (-64 : Int64).toInt32 ~> -64
|
||||
#check_simp (-64 : Int64).toISize ~> -64
|
||||
|
||||
#check_simp (-64 : ISize).toInt8 ~> -64
|
||||
#check_simp (-64 : ISize).toInt16 ~> -64
|
||||
#check_simp (-64 : ISize).toInt32 ~> -64
|
||||
|
||||
-- This could be fixed with some additional work
|
||||
#check_simp (-64 : ISize).toInt64 !~>
|
||||
|
||||
#check_simp (-127 : Int8).toInt16 ~> -127
|
||||
#check_simp (-128 : Int8).toInt16 !~>
|
||||
|
||||
-- All of these could probably made to reduce using an additional simproc
|
||||
#check_simp (300 : UInt8) !~>
|
||||
#check_simp (300 : Int8) !~>
|
||||
#check_simp (-32767 : Int16).toInt8 ~> -32767
|
||||
#check_simp (-32768 : Int16).toInt8 ~> -32768
|
||||
#check_simp (-32769 : Int16).toInt8 ~> -32769
|
||||
|
||||
#check_simp (-32767 : Int16).toInt32 ~> -32767
|
||||
#check_simp (-32768 : Int16).toInt32 !~>
|
||||
|
||||
#check_simp (-2147483647 : Int32).toInt64 ~> -2147483647
|
||||
#check_simp (-2147483648 : Int32).toInt64 !~>
|
||||
|
||||
-- see also simprocSInt.lean
|
||||
|
|
@ -202,3 +202,5 @@ section
|
|||
#check_simp ISize.toInt (-2147483648) ~> -2147483648
|
||||
|
||||
end
|
||||
|
||||
-- see also simpSInt.lean
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue