From 8de623332622007ca3c114ab14f7cd5ed2ec5cd8 Mon Sep 17 00:00:00 2001 From: Markus Himmel Date: Wed, 5 Mar 2025 07:27:53 +0100 Subject: [PATCH] feat: `IntX` conversion lemmas (#7274) This PR adds lemmas about iterated conversions between finite types, starting with something of type `IntX`. --- src/Init/Data/BitVec/Bitblast.lean | 9 + src/Init/Data/BitVec/Lemmas.lean | 71 ++- src/Init/Data/Int/DivMod/Lemmas.lean | 3 + src/Init/Data/Int/LemmasAux.lean | 12 + src/Init/Data/SInt/Lemmas.lean | 809 +++++++++++++++++++++++++-- 5 files changed, 849 insertions(+), 55 deletions(-) diff --git a/src/Init/Data/BitVec/Bitblast.lean b/src/Init/Data/BitVec/Bitblast.lean index f1c077a556..cd846be380 100644 --- a/src/Init/Data/BitVec/Bitblast.lean +++ b/src/Init/Data/BitVec/Bitblast.lean @@ -544,6 +544,15 @@ theorem slt_eq_not_carry (x y : BitVec w) : theorem sle_eq_not_slt (x y : BitVec w) : x.sle y = !y.slt x := by simp only [BitVec.sle, BitVec.slt, ← decide_not, decide_eq_decide]; omega +theorem zero_sle_eq_not_msb {w : Nat} {x : BitVec w} : BitVec.sle 0#w x = !x.msb := by + rw [sle_eq_not_slt, BitVec.slt_zero_eq_msb] + +theorem zero_sle_iff_msb_eq_false {w : Nat} {x : BitVec w} : BitVec.sle 0#w x ↔ x.msb = false := by + simp [zero_sle_eq_not_msb] + +theorem toNat_toInt_of_sle {w : Nat} (b : BitVec w) (hb : BitVec.sle 0#w b) : b.toInt.toNat = b.toNat := + toNat_toInt_of_msb b (zero_sle_iff_msb_eq_false.1 hb) + theorem sle_eq_carry (x y : BitVec w) : x.sle y = !((x.msb == y.msb).xor (carry w y (~~~x) true)) := by rw [sle_eq_not_slt, slt_eq_not_carry, beq_comm] diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean index 4e7e56a17d..9052789a7a 100644 --- a/src/Init/Data/BitVec/Lemmas.lean +++ b/src/Init/Data/BitVec/Lemmas.lean @@ -529,6 +529,9 @@ theorem toInt_eq_toNat_of_msb {x : BitVec w} (h : x.msb = false) : x.toInt = x.toNat := by simp [toInt_eq_msb_cond, h] +theorem toNat_toInt_of_msb {w : Nat} (b : BitVec w) (hb : b.msb = false) : b.toInt.toNat = b.toNat := by + simp [b.toInt_eq_toNat_of_msb hb] + theorem toInt_eq_toNat_bmod (x : BitVec n) : x.toInt = Int.bmod x.toNat (2^n) := by simp only [toInt_eq_toNat_cond] split @@ -651,6 +654,12 @@ theorem slt_zero_iff_msb_cond {x : BitVec w} : x.slt 0#w ↔ x.msb = true := by simp [BitVec.slt, this] omega +theorem slt_zero_eq_msb {w : Nat} {x : BitVec w} : x.slt 0#w = x.msb := by + rw [Bool.eq_iff_iff, BitVec.slt_zero_iff_msb_cond] + +theorem sle_iff_toInt_le {w : Nat} {b b' : BitVec w} : b.sle b' ↔ b.toInt ≤ b'.toInt := + decide_eq_true_iff + /-! ### setWidth, zeroExtend and truncate -/ @[simp] @@ -2058,7 +2067,7 @@ theorem signExtend_eq_setWidth_of_lt (x : BitVec w) {v : Nat} (hv : v ≤ w): simp [getElem_signExtend, show i < w by omega] /-- Sign extending to the same bitwidth is a no op. -/ -theorem signExtend_eq (x : BitVec w) : x.signExtend w = x := by +@[simp] theorem signExtend_eq (x : BitVec w) : x.signExtend w = x := by rw [signExtend_eq_setWidth_of_lt _ (Nat.le_refl _), setWidth_eq] /-- Sign extending to a larger bitwidth depends on the msb. @@ -2100,43 +2109,63 @@ theorem toNat_signExtend (x : BitVec w) {v : Nat} : · 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)] -/- +/-- If the current width `w` is smaller than the extended width `v`, then the value when interpreted as an integer does not change. -/ -theorem toInt_signExtend_of_lt {x : BitVec w} (hv : w < v): +theorem toInt_signExtend_of_le {x : BitVec w} (h : w ≤ v) : (x.signExtend v).toInt = x.toInt := by - simp only [toInt_eq_msb_cond, toNat_signExtend] - have : (x.signExtend v).msb = x.msb := by - rw [msb_eq_getLsbD_last, getLsbD_eq_getElem (Nat.sub_one_lt_of_lt hv)] - simp [getElem_signExtend, Nat.le_sub_one_of_lt hv] + by_cases hlt : w < v + · rw [toInt_signExtend_of_lt hlt] + · obtain rfl : w = v := by omega + simp +where + toInt_signExtend_of_lt {x : BitVec w} (hv : w < v): + (x.signExtend v).toInt = x.toInt := by + simp only [toInt_eq_msb_cond, toNat_signExtend] + have : (x.signExtend v).msb = x.msb := by + rw [msb_eq_getLsbD_last, getLsbD_eq_getElem (Nat.sub_one_lt_of_lt hv)] + simp [getElem_signExtend, Nat.le_sub_one_of_lt hv] + omega + have H : 2^w ≤ 2^v := Nat.pow_le_pow_right (by omega) (by omega) + simp only [this, toNat_setWidth, Int.natCast_add, Int.ofNat_emod, Int.natCast_mul] + by_cases h : x.msb + <;> norm_cast + <;> simp [h, Nat.mod_eq_of_lt (Nat.lt_of_lt_of_le x.isLt H)] omega - have H : 2^w ≤ 2^v := Nat.pow_le_pow_right (by omega) (by omega) - simp only [this, toNat_setWidth, Int.natCast_add, Int.ofNat_emod, Int.natCast_mul] - by_cases h : x.msb - <;> norm_cast - <;> simp [h, Nat.mod_eq_of_lt (Nat.lt_of_lt_of_le x.isLt H)] - omega -/- +/-- If the current width `w` is larger than the extended width `v`, then the value when interpreted as an integer is truncated, and we compute a modulo by `2^v`. -/ -theorem toInt_signExtend_of_le {x : BitVec w} (hv : v ≤ w) : +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] -/- +/-- Interpreting the sign extension of `(x : BitVec w)` to width `v` -computes `x % 2^v` (where `%` is the balanced mod). +computes `x % 2^v` (where `%` is the balanced mod). See `toInt_signExtend` for a version stated +in terms of `toInt` instead of `toNat`. -/ -theorem toInt_signExtend (x : BitVec w) : - (x.signExtend v).toInt = Int.bmod x.toNat (2^(min v w)) := by +theorem toInt_signExtend_eq_toNat_bmod (x : BitVec w) : + (x.signExtend v).toInt = Int.bmod x.toNat (2 ^ min v w) := by by_cases hv : v ≤ w - · simp [toInt_signExtend_of_le hv, Nat.min_eq_left hv] + · simp [toInt_signExtend_eq_toNat_bmod_of_le hv, Nat.min_eq_left hv] · simp only [Nat.not_le] at hv - rw [toInt_signExtend_of_lt hv, Nat.min_eq_right (by omega), toInt_eq_toNat_bmod] + rw [toInt_signExtend_of_le (Nat.le_of_lt hv), + Nat.min_eq_right (by omega), toInt_eq_toNat_bmod] + +theorem toInt_signExtend (x : BitVec w) : + (x.signExtend v).toInt = x.toInt.bmod (2 ^ min v w) := by + rw [toInt_signExtend_eq_toNat_bmod, BitVec.toInt_eq_toNat_bmod, Int.bmod_bmod_of_dvd] + exact Nat.pow_dvd_pow _ (Nat.min_le_right v w) + +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 -/ diff --git a/src/Init/Data/Int/DivMod/Lemmas.lean b/src/Init/Data/Int/DivMod/Lemmas.lean index 63f22e51e5..b34523e3a7 100644 --- a/src/Init/Data/Int/DivMod/Lemmas.lean +++ b/src/Init/Data/Int/DivMod/Lemmas.lean @@ -1382,6 +1382,9 @@ theorem bmod_add_mul_cancel (x : Int) (n : Nat) (k : Int) : Int.bmod (x + n * k) theorem bmod_sub_cancel (x : Int) (n : Nat) : Int.bmod (x - n) n = Int.bmod x n := by simp [bmod_def] +@[simp] theorem Int.bmod_sub_mul_cancel (x : Int) (n : Nat) (k : Int) : (x - n * k).bmod n = x.bmod n := by + rw [Int.sub_eq_add_neg, Int.neg_mul_eq_mul_neg, Int.bmod_add_mul_cancel] + @[simp] theorem emod_add_bmod_congr (x : Int) (n : Nat) : Int.bmod (x%n + y) n = Int.bmod (x + y) n := by simp [Int.emod_def, Int.sub_eq_add_neg] diff --git a/src/Init/Data/Int/LemmasAux.lean b/src/Init/Data/Int/LemmasAux.lean index e04b43d90c..20c1ab1721 100644 --- a/src/Init/Data/Int/LemmasAux.lean +++ b/src/Init/Data/Int/LemmasAux.lean @@ -65,4 +65,16 @@ theorem bmod_eq_self_of_le {n : Int} {m : Nat} (hn' : -(m / 2) ≤ n) (hn : n < apply eq_zero_of_dvd_of_natAbs_lt_natAbs Int.dvd_bmod_sub_self omega +theorem sub_eq_iff_eq_add {b a c : Int} : a - b = c ↔ a = c + b := by omega +theorem sub_eq_iff_eq_add' {b a c : Int} : a - b = c ↔ a = b + c := by omega + +theorem bmod_bmod_of_dvd {a : Int} {n m : Nat} (hnm : n ∣ m) : + (a.bmod m).bmod n = a.bmod n := by + rw [← sub_eq_iff_eq_add.2 (bmod_add_bdiv a m).symm] + obtain ⟨k, rfl⟩ := hnm + simp [Int.mul_assoc] + +@[simp] theorem toNat_le {m : Int} {n : Nat} : m.toNat ≤ n ↔ m ≤ n := by omega +@[simp] theorem toNat_lt' {m : Int} {n : Nat} (hn : 0 < n) : m.toNat < n ↔ m < n := by omega + end Int diff --git a/src/Init/Data/SInt/Lemmas.lean b/src/Init/Data/SInt/Lemmas.lean index 6216e41440..405942851b 100644 --- a/src/Init/Data/SInt/Lemmas.lean +++ b/src/Init/Data/SInt/Lemmas.lean @@ -5,7 +5,8 @@ Authors: Markus Himmel -/ prelude import Init.Data.SInt.Basic -import Init.Data.BitVec.Lemmas +import Init.Data.BitVec.Bitblast +import Init.Data.Int.LemmasAux open Lean in set_option hygiene false in @@ -34,6 +35,118 @@ declare_int_theorems Int32 32 declare_int_theorems Int64 64 declare_int_theorems ISize System.Platform.numBits +theorem Int8.toInt.inj {x y : Int8} (h : x.toInt = y.toInt) : x = y := Int8.toBitVec.inj (BitVec.eq_of_toInt_eq h) +theorem Int8.toInt_inj {x y : Int8} : x.toInt = y.toInt ↔ x = y := ⟨Int8.toInt.inj, fun h => h ▸ rfl⟩ +theorem Int16.toInt.inj {x y : Int16} (h : x.toInt = y.toInt) : x = y := Int16.toBitVec.inj (BitVec.eq_of_toInt_eq h) +theorem Int16.toInt_inj {x y : Int16} : x.toInt = y.toInt ↔ x = y := ⟨Int16.toInt.inj, fun h => h ▸ rfl⟩ +theorem Int32.toInt.inj {x y : Int32} (h : x.toInt = y.toInt) : x = y := Int32.toBitVec.inj (BitVec.eq_of_toInt_eq h) +theorem Int32.toInt_inj {x y : Int32} : x.toInt = y.toInt ↔ x = y := ⟨Int32.toInt.inj, fun h => h ▸ rfl⟩ +theorem Int64.toInt.inj {x y : Int64} (h : x.toInt = y.toInt) : x = y := Int64.toBitVec.inj (BitVec.eq_of_toInt_eq h) +theorem Int64.toInt_inj {x y : Int64} : x.toInt = y.toInt ↔ x = y := ⟨Int64.toInt.inj, fun h => h ▸ rfl⟩ +theorem ISize.toInt.inj {x y : ISize} (h : x.toInt = y.toInt) : x = y := ISize.toBitVec.inj (BitVec.eq_of_toInt_eq h) +theorem ISize.toInt_inj {x y : ISize} : x.toInt = y.toInt ↔ x = y := ⟨ISize.toInt.inj, fun h => h ▸ rfl⟩ + +@[simp] theorem Int8.toBitVec_neg (x : Int8) : (-x).toBitVec = -x.toBitVec := rfl +@[simp] theorem Int16.toBitVec_neg (x : Int16) : (-x).toBitVec = -x.toBitVec := rfl +@[simp] theorem Int32.toBitVec_neg (x : Int32) : (-x).toBitVec = -x.toBitVec := rfl +@[simp] theorem Int64.toBitVec_neg (x : Int64) : (-x).toBitVec = -x.toBitVec := rfl +@[simp] theorem ISize.toBitVec_neg (x : ISize) : (-x).toBitVec = -x.toBitVec := rfl + +@[simp] theorem ISize.toBitVec_zero : (0 : ISize).toBitVec = 0 := rfl + +@[simp] theorem Int8.toBitVec_ofInt (i : Int) : (ofInt i).toBitVec = BitVec.ofInt _ i := rfl +@[simp] theorem Int16.toBitVec_ofInt (i : Int) : (ofInt i).toBitVec = BitVec.ofInt _ i := rfl +@[simp] theorem Int32.toBitVec_ofInt (i : Int) : (ofInt i).toBitVec = BitVec.ofInt _ i := rfl +@[simp] theorem Int64.toBitVec_ofInt (i : Int) : (ofInt i).toBitVec = BitVec.ofInt _ i := rfl +@[simp] theorem ISize.toBitVec_ofInt (i : Int) : (ofInt i).toBitVec = BitVec.ofInt _ i := rfl + +@[simp] theorem Int8.neg_zero : -(0 : Int8) = 0 := rfl +@[simp] theorem Int16.neg_zero : -(0 : Int16) = 0 := rfl +@[simp] theorem Int32.neg_zero : -(0 : Int32) = 0 := rfl +@[simp] theorem Int64.neg_zero : -(0 : Int64) = 0 := rfl +@[simp] theorem ISize.neg_zero : -(0 : ISize) = 0 := ISize.toBitVec.inj (by simp) + +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 + 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 + 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 + 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 + 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 + rw [toInt, toBitVec_ofInt, BitVec.toInt_ofInt_eq_self] <;> cases System.Platform.numBits_eq + <;> (simp_all; try omega) + +theorem ISize.toInt_ofInt_of_two_pow_numBits_le {n : Int} (hn : -2 ^ (System.Platform.numBits - 1) ≤ n) + (hn' : n < 2 ^ (System.Platform.numBits - 1)) : toInt (ofInt n) = n := by + rw [toInt, toBitVec_ofInt, BitVec.toInt_ofInt_eq_self _ hn hn'] + cases System.Platform.numBits_eq <;> simp_all + +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] + +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) := + toBitVec.inj (by simp [BitVec.ofInt_neg]) + +theorem Int8.ofInt_eq_ofNat {n : Nat} : ofInt n = ofNat n := toBitVec.inj (by simp) +theorem Int16.ofInt_eq_ofNat {n : Nat} : ofInt n = ofNat n := toBitVec.inj (by simp) +theorem Int32.ofInt_eq_ofNat {n : Nat} : ofInt n = ofNat n := toBitVec.inj (by simp) +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) + +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] +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] + +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)] +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)] +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)] +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)] +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)] +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)] +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)] + +theorem Int8.toInt_zero : toInt 0 = 0 := by simp +theorem Int16.toInt_zero : toInt 0 = 0 := by simp +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 + +@[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 +@[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 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 @@ -52,47 +165,675 @@ declare_int_theorems ISize System.Platform.numBits @[simp] theorem UInt64.toUInt64_toInt64 (x : UInt64) : x.toInt64.toUInt64 = x := rfl @[simp] theorem USize.toUSize_toISize (x : USize) : x.toISize.toUSize = x := rfl -@[simp] theorem ISize.toBitVec_neg (x : ISize) : (-x).toBitVec = -x.toBitVec := rfl -@[simp] theorem ISize.toBitVec_zero : (0 : ISize).toBitVec = 0 := rfl -@[simp] theorem ISize.toBitVec_ofInt (i : Int) : (ofInt i).toBitVec = BitVec.ofInt _ i := rfl +@[simp] theorem Int8.toNat_toInt (x : Int8) : x.toInt.toNat = x.toNatClampNeg := rfl +@[simp] theorem Int16.toNat_toInt (x : Int16) : x.toInt.toNat = x.toNatClampNeg := rfl +@[simp] theorem Int32.toNat_toInt (x : Int32) : x.toInt.toNat = x.toNatClampNeg := rfl +@[simp] theorem Int64.toNat_toInt (x : Int64) : x.toInt.toNat = x.toNatClampNeg := rfl +@[simp] theorem ISize.toNat_toInt (x : ISize) : x.toInt.toNat = x.toNatClampNeg := rfl -@[simp] theorem Int8.neg_zero : -(0 : Int8) = 0 := rfl -@[simp] theorem Int16.neg_zero : -(0 : Int16) = 0 := rfl -@[simp] theorem Int32.neg_zero : -(0 : Int32) = 0 := rfl -@[simp] theorem Int64.neg_zero : -(0 : Int64) = 0 := rfl -@[simp] theorem ISize.neg_zero : -(0 : ISize) = 0 := ISize.toBitVec.inj (by simp) +@[simp] theorem Int8.toInt_toBitVec (x : Int8) : x.toBitVec.toInt = x.toInt := rfl +@[simp] theorem Int16.toInt_toBitVec (x : Int16) : x.toBitVec.toInt = x.toInt := rfl +@[simp] theorem Int32.toInt_toBitVec (x : Int32) : x.toBitVec.toInt = x.toInt := rfl +@[simp] theorem Int64.toInt_toBitVec (x : Int64) : x.toBitVec.toInt = x.toInt := rfl +@[simp] theorem ISize.toInt_toBitVec (x : ISize) : x.toBitVec.toInt = x.toInt := rfl -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)) +@[simp] theorem Int8.toBitVec_toInt16 (x : Int8) : x.toInt16.toBitVec = x.toBitVec.signExtend 16 := rfl +@[simp] theorem Int8.toBitVec_toInt32 (x : Int8) : x.toInt32.toBitVec = x.toBitVec.signExtend 32 := rfl +@[simp] theorem Int8.toBitVec_toInt64 (x : Int8) : x.toInt64.toBitVec = x.toBitVec.signExtend 64 := rfl +@[simp] theorem Int8.toBitVec_toISize (x : Int8) : x.toISize.toBitVec = x.toBitVec.signExtend System.Platform.numBits := rfl -theorem ISize.toInt_ofInt {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) +@[simp] theorem Int16.toBitVec_toInt8 (x : Int16) : x.toInt8.toBitVec = x.toBitVec.signExtend 8 := rfl +@[simp] theorem Int16.toBitVec_toInt32 (x : Int16) : x.toInt32.toBitVec = x.toBitVec.signExtend 32 := rfl +@[simp] theorem Int16.toBitVec_toInt64 (x : Int16) : x.toInt64.toBitVec = x.toBitVec.signExtend 64 := rfl +@[simp] theorem Int16.toBitVec_toISize (x : Int16) : x.toISize.toBitVec = x.toBitVec.signExtend System.Platform.numBits := rfl -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] +@[simp] theorem Int32.toBitVec_toInt8 (x : Int32) : x.toInt8.toBitVec = x.toBitVec.signExtend 8 := rfl +@[simp] theorem Int32.toBitVec_toInt16 (x : Int32) : x.toInt16.toBitVec = x.toBitVec.signExtend 16 := rfl +@[simp] theorem Int32.toBitVec_toInt64 (x : Int32) : x.toInt64.toBitVec = x.toBitVec.signExtend 64 := rfl +@[simp] theorem Int32.toBitVec_toISize (x : Int32) : x.toISize.toBitVec = x.toBitVec.signExtend System.Platform.numBits := rfl -theorem ISize.neg_ofInt {n : Int} : -ofInt n = ofInt (-n) := - toBitVec.inj (by simp [BitVec.ofInt_neg]) +@[simp] theorem Int64.toBitVec_toInt8 (x : Int64) : x.toInt8.toBitVec = x.toBitVec.signExtend 8 := rfl +@[simp] theorem Int64.toBitVec_toInt16 (x : Int64) : x.toInt16.toBitVec = x.toBitVec.signExtend 16 := rfl +@[simp] theorem Int64.toBitVec_toInt32 (x : Int64) : x.toInt32.toBitVec = x.toBitVec.signExtend 32 := rfl +@[simp] theorem Int64.toBitVec_toISize (x : Int64) : x.toISize.toBitVec = x.toBitVec.signExtend System.Platform.numBits := rfl -theorem ISize.ofInt_eq_ofNat {n : Nat} : ofInt n = ofNat n := - toBitVec.inj (by simp) +@[simp] theorem ISize.toBitVec_toInt8 (x : ISize) : x.toInt8.toBitVec = x.toBitVec.signExtend 8 := rfl +@[simp] theorem ISize.toBitVec_toInt16 (x : ISize) : x.toInt16.toBitVec = x.toBitVec.signExtend 16 := 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 ISize.neg_ofNat {n : Nat} : -ofNat n = ofInt (-n) := by - rw [← neg_ofInt, ofInt_eq_ofNat] +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 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 + have := x.toBitVec.le_toInt; cases System.Platform.numBits_eq <;> simp_all <;> omega +theorem ISize.toInt_lt (x : ISize) : x.toInt < 2 ^ 63 := by + have := x.toBitVec.toInt_lt; cases System.Platform.numBits_eq <;> simp_all <;> omega +theorem ISize.le_toInt (x : ISize) : -2 ^ 63 ≤ x.toInt := by + have := x.toBitVec.le_toInt; cases System.Platform.numBits_eq <;> simp_all <;> omega -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] +theorem Int8.toInt_le (x : Int8) : x.toInt ≤ Int8.maxValue.toInt := Int.le_of_lt_add_one x.toInt_lt +theorem Int16.toInt_le (x : Int16) : x.toInt ≤ Int16.maxValue.toInt := Int.le_of_lt_add_one x.toInt_lt +theorem Int32.toInt_le (x : Int32) : x.toInt ≤ Int32.maxValue.toInt := Int.le_of_lt_add_one x.toInt_lt +theorem Int64.toInt_le (x : Int64) : x.toInt ≤ Int64.maxValue.toInt := Int.le_of_lt_add_one x.toInt_lt +theorem ISize.toInt_le (x : ISize) : x.toInt ≤ ISize.maxValue.toInt := by + rw [toInt_ofInt_of_two_pow_numBits_le] + · exact Int.le_of_lt_add_one (by simpa using x.toInt_lt_two_pow_numBits) + · cases System.Platform.numBits_eq <;> simp_all + · cases System.Platform.numBits_eq <;> simp_all +theorem Int8.minValue_le_toInt (x : Int8) : Int8.minValue.toInt ≤ x.toInt := x.le_toInt +theorem Int16.minValue_le_toInt (x : Int16) : Int16.minValue.toInt ≤ x.toInt := x.le_toInt +theorem Int32.minValue_le_toInt (x : Int32) : Int32.minValue.toInt ≤ x.toInt := x.le_toInt +theorem Int64.minValue_le_toInt (x : Int64) : Int64.minValue.toInt ≤ x.toInt := x.le_toInt +theorem ISize.minValue_le_toInt (x : ISize) : ISize.minValue.toInt ≤ x.toInt := by + rw [toInt_ofInt_of_two_pow_numBits_le] + · exact x.two_pow_numBits_le_toInt + · cases System.Platform.numBits_eq <;> simp_all + · cases System.Platform.numBits_eq <;> simp_all -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 ISize.toInt_minValue_le : ISize.minValue.toInt ≤ -2^31 := by + rw [minValue, toInt_ofInt_of_two_pow_numBits_le] <;> cases System.Platform.numBits_eq + <;> simp_all -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)] +theorem ISize.le_toInt_maxValue : 2 ^ 31 - 1 ≤ ISize.maxValue.toInt := by + rw [maxValue, toInt_ofInt_of_two_pow_numBits_le] <;> cases System.Platform.numBits_eq + <;> simp_all -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)] +theorem Int8.iSizeMinValue_le_toInt (x : Int8) : ISize.minValue.toInt ≤ x.toInt := + Int.le_trans (Int.le_trans ISize.toInt_minValue_le (by decide)) x.le_toInt +theorem Int8.toInt_le_iSizeMaxValue (x : Int8) : x.toInt ≤ ISize.maxValue.toInt := + Int.le_trans x.toInt_le (Int.le_trans (by decide) ISize.le_toInt_maxValue) +theorem Int16.iSizeMinValue_le_toInt (x : Int16) : ISize.minValue.toInt ≤ x.toInt := + Int.le_trans (Int.le_trans ISize.toInt_minValue_le (by decide)) x.le_toInt +theorem Int16.toInt_le_iSizeMaxValue (x : Int16) : x.toInt ≤ ISize.maxValue.toInt := + Int.le_trans x.toInt_le (Int.le_trans (by decide) ISize.le_toInt_maxValue) +theorem Int32.iSizeMinValue_le_toInt (x : Int32) : ISize.minValue.toInt ≤ x.toInt := + Int.le_trans (Int.le_trans ISize.toInt_minValue_le (by decide)) x.le_toInt +theorem Int32.toInt_le_iSizeMaxValue (x : Int32) : x.toInt ≤ ISize.maxValue.toInt := + Int.le_trans x.toInt_le (Int.le_trans (by decide) ISize.le_toInt_maxValue) + +theorem ISize.int64MinValue_le_toInt (x : ISize) : Int64.minValue.toInt ≤ x.toInt := + Int.le_trans (by decide) x.le_toInt +theorem ISize.toInt_le_int64MaxValue (x : ISize) : x.toInt ≤ Int64.maxValue.toInt := + Int.le_of_lt_add_one x.toInt_lt + +theorem Int8.toNatClampNeg_lt (x : Int8) : x.toNatClampNeg < 2 ^ 7 := (Int.toNat_lt' (by decide)).2 x.toInt_lt +theorem Int16.toNatClampNeg_lt (x : Int16) : x.toNatClampNeg < 2 ^ 15 := (Int.toNat_lt' (by decide)).2 x.toInt_lt +theorem Int32.toNatClampNeg_lt (x : Int32) : x.toNatClampNeg < 2 ^ 31 := (Int.toNat_lt' (by decide)).2 x.toInt_lt +theorem Int64.toNatClampNeg_lt (x : Int64) : x.toNatClampNeg < 2 ^ 63 := (Int.toNat_lt' (by decide)).2 x.toInt_lt +theorem ISize.toNatClampNeg_lt_two_pow_numBits (x : ISize) : x.toNatClampNeg < 2 ^ (System.Platform.numBits - 1) := by + rw [toNatClampNeg, Int.toNat_lt', Int.natCast_pow] + · exact x.toInt_lt_two_pow_numBits + · cases System.Platform.numBits_eq <;> simp_all +theorem ISize.toNatClampNeg_lt (x : ISize) : x.toNatClampNeg < 2 ^ 63 := (Int.toNat_lt' (by decide)).2 x.toInt_lt + +@[simp] theorem Int8.toInt_toInt16 (x : Int8) : x.toInt16.toInt = x.toInt := + x.toBitVec.toInt_signExtend_of_le (by decide) +@[simp] theorem Int8.toInt_toInt32 (x : Int8) : x.toInt32.toInt = x.toInt := + x.toBitVec.toInt_signExtend_of_le (by decide) +@[simp] theorem Int8.toInt_toInt64 (x : Int8) : x.toInt64.toInt = x.toInt := + x.toBitVec.toInt_signExtend_of_le (by decide) +@[simp] theorem Int8.toInt_toISize (x : Int8) : x.toISize.toInt = x.toInt := + x.toBitVec.toInt_signExtend_of_le (by cases System.Platform.numBits_eq <;> simp_all) + +@[simp] theorem Int16.toInt_toInt8 (x : Int16) : x.toInt8.toInt = x.toInt.bmod (2 ^ 8) := + x.toBitVec.toInt_signExtend_eq_toInt_bmod_of_le (by decide) +@[simp] theorem Int16.toInt_toInt32 (x : Int16) : x.toInt32.toInt = x.toInt := + x.toBitVec.toInt_signExtend_of_le (by decide) +@[simp] theorem Int16.toInt_toInt64 (x : Int16) : x.toInt64.toInt = x.toInt := + x.toBitVec.toInt_signExtend_of_le (by decide) +@[simp] theorem Int16.toInt_toISize (x : Int16) : x.toISize.toInt = x.toInt := + x.toBitVec.toInt_signExtend_of_le (by cases System.Platform.numBits_eq <;> simp_all) + +@[simp] theorem Int32.toInt_toInt8 (x : Int32) : x.toInt8.toInt = x.toInt.bmod (2 ^ 8) := + x.toBitVec.toInt_signExtend_eq_toInt_bmod_of_le (by decide) +@[simp] theorem Int32.toInt_toInt16 (x : Int32) : x.toInt16.toInt = x.toInt.bmod (2 ^ 16) := + x.toBitVec.toInt_signExtend_eq_toInt_bmod_of_le (by decide) +@[simp] theorem Int32.toInt_toInt64 (x : Int32) : x.toInt64.toInt = x.toInt := + x.toBitVec.toInt_signExtend_of_le (by decide) +@[simp] theorem Int32.toInt_toISize (x : Int32) : x.toISize.toInt = x.toInt := + x.toBitVec.toInt_signExtend_of_le (by cases System.Platform.numBits_eq <;> simp_all) + +@[simp] theorem Int64.toInt_toInt8 (x : Int64) : x.toInt8.toInt = x.toInt.bmod (2 ^ 8) := + x.toBitVec.toInt_signExtend_eq_toInt_bmod_of_le (by decide) +@[simp] theorem Int64.toInt_toInt16 (x : Int64) : x.toInt16.toInt = x.toInt.bmod (2 ^ 16) := + x.toBitVec.toInt_signExtend_eq_toInt_bmod_of_le (by decide) +@[simp] theorem Int64.toInt_toInt32 (x : Int64) : x.toInt32.toInt = x.toInt.bmod (2 ^ 32) := + x.toBitVec.toInt_signExtend_eq_toInt_bmod_of_le (by decide) +@[simp] theorem Int64.toInt_toISize (x : Int64) : x.toISize.toInt = x.toInt.bmod (2 ^ System.Platform.numBits) := + x.toBitVec.toInt_signExtend_eq_toInt_bmod_of_le (by cases System.Platform.numBits_eq <;> simp_all) + +@[simp] theorem ISize.toInt_toInt8 (x : ISize) : x.toInt8.toInt = x.toInt.bmod (2 ^ 8) := + x.toBitVec.toInt_signExtend_eq_toInt_bmod_of_le (by cases System.Platform.numBits_eq <;> simp_all) +@[simp] theorem ISize.toInt_toInt16 (x : ISize) : x.toInt16.toInt = x.toInt.bmod (2 ^ 16) := + x.toBitVec.toInt_signExtend_eq_toInt_bmod_of_le (by cases System.Platform.numBits_eq <;> simp_all) +@[simp] theorem ISize.toInt_toInt32 (x : ISize) : x.toInt32.toInt = x.toInt.bmod (2 ^ 32) := + x.toBitVec.toInt_signExtend_eq_toInt_bmod_of_le (by cases System.Platform.numBits_eq <;> simp_all) +@[simp] theorem ISize.toInt_toInt64 (x : ISize) : x.toInt64.toInt = x.toInt := + x.toBitVec.toInt_signExtend_of_le (by cases System.Platform.numBits_eq <;> simp_all) + +@[simp] theorem Int8.toNatClampNeg_toInt16 (x : Int8) : x.toInt16.toNatClampNeg = x.toNatClampNeg := + congrArg Int.toNat x.toInt_toInt16 +@[simp] theorem Int8.toNatClampNeg_toInt32 (x : Int8) : x.toInt32.toNatClampNeg = x.toNatClampNeg := + congrArg Int.toNat x.toInt_toInt32 +@[simp] theorem Int8.toNatClampNeg_toInt64 (x : Int8) : x.toInt64.toNatClampNeg = x.toNatClampNeg := + congrArg Int.toNat x.toInt_toInt64 +@[simp] theorem Int8.toNatClampNeg_toISize (x : Int8) : x.toISize.toNatClampNeg = x.toNatClampNeg := + congrArg Int.toNat x.toInt_toISize + +@[simp] theorem Int16.toNatClampNeg_toInt32 (x : Int16) : x.toInt32.toNatClampNeg = x.toNatClampNeg := + congrArg Int.toNat x.toInt_toInt32 +@[simp] theorem Int16.toNatClampNeg_toInt64 (x : Int16) : x.toInt64.toNatClampNeg = x.toNatClampNeg := + congrArg Int.toNat x.toInt_toInt64 +@[simp] theorem Int16.toNatClampNeg_toISize (x : Int16) : x.toISize.toNatClampNeg = x.toNatClampNeg := + congrArg Int.toNat x.toInt_toISize + +@[simp] theorem Int32.toNatClampNeg_toInt64 (x : Int32) : x.toInt64.toNatClampNeg = x.toNatClampNeg := + congrArg Int.toNat x.toInt_toInt64 +@[simp] theorem Int32.toNatClampNeg_toISize (x : Int32) : x.toISize.toNatClampNeg = x.toNatClampNeg := + congrArg Int.toNat x.toInt_toISize + +@[simp] theorem ISize.toNatClampNeg_toInt64 (x : ISize) : x.toInt64.toNatClampNeg = x.toNatClampNeg := + congrArg Int.toNat x.toInt_toInt64 + +@[simp] theorem Int8.toInt8_toUInt8 (x : Int8) : x.toUInt8.toInt8 = x := rfl +@[simp] theorem Int16.toInt16_toUInt16 (x : Int16) : x.toUInt16.toInt16 = x := rfl +@[simp] theorem Int32.toInt32_toUInt32 (x : Int32) : x.toUInt32.toInt32 = x := rfl +@[simp] theorem Int64.toInt64_toUInt64 (x : Int64) : x.toUInt64.toInt64 = x := rfl +@[simp] theorem ISize.toISize_toUSize (x : ISize) : x.toUSize.toISize = x := rfl + +-- TODO: possibly good simp lemmas in the reverse direction? +theorem Int8.toNat_toBitVec (x : Int8) : x.toBitVec.toNat = x.toUInt8.toNat := rfl +theorem Int16.toNat_toBitVec (x : Int16) : x.toBitVec.toNat = x.toUInt16.toNat := rfl +theorem Int32.toNat_toBitVec (x : Int32) : x.toBitVec.toNat = x.toUInt32.toNat := rfl +theorem Int64.toNat_toBitVec (x : Int64) : x.toBitVec.toNat = x.toUInt64.toNat := rfl +theorem ISize.toNat_toBitVec (x : ISize) : x.toBitVec.toNat = x.toUSize.toNat := rfl + +theorem Int8.toNat_toBitVec_of_le {x : Int8} (hx : 0 ≤ x) : x.toBitVec.toNat = x.toNatClampNeg := + (x.toBitVec.toNat_toInt_of_sle hx).symm +theorem Int16.toNat_toBitVec_of_le {x : Int16} (hx : 0 ≤ x) : x.toBitVec.toNat = x.toNatClampNeg := + (x.toBitVec.toNat_toInt_of_sle hx).symm +theorem Int32.toNat_toBitVec_of_le {x : Int32} (hx : 0 ≤ x) : x.toBitVec.toNat = x.toNatClampNeg := + (x.toBitVec.toNat_toInt_of_sle hx).symm +theorem Int64.toNat_toBitVec_of_le {x : Int64} (hx : 0 ≤ x) : x.toBitVec.toNat = x.toNatClampNeg := + (x.toBitVec.toNat_toInt_of_sle hx).symm +theorem ISize.toNat_toBitVec_of_le {x : ISize} (hx : 0 ≤ x) : x.toBitVec.toNat = x.toNatClampNeg := + (x.toBitVec.toNat_toInt_of_sle hx).symm + +theorem Int8.toNat_toUInt8_of_le {x : Int8} (hx : 0 ≤ x) : x.toUInt8.toNat = x.toNatClampNeg := by + rw [← toNat_toBitVec, toNat_toBitVec_of_le hx] +theorem Int16.toNat_toUInt16_of_le {x : Int16} (hx : 0 ≤ x) : x.toUInt16.toNat = x.toNatClampNeg := by + rw [← toNat_toBitVec, toNat_toBitVec_of_le hx] +theorem Int32.toNat_toUInt32_of_le {x : Int32} (hx : 0 ≤ x) : x.toUInt32.toNat = x.toNatClampNeg := by + rw [← toNat_toBitVec, toNat_toBitVec_of_le hx] +theorem Int64.toNat_toUInt64_of_le {x : Int64} (hx : 0 ≤ x) : x.toUInt64.toNat = x.toNatClampNeg := by + rw [← toNat_toBitVec, toNat_toBitVec_of_le hx] +theorem ISize.toNat_toUISize_of_le {x : ISize} (hx : 0 ≤ x) : x.toUSize.toNat = x.toNatClampNeg := by + rw [← toNat_toBitVec, toNat_toBitVec_of_le hx] + +-- TODO: possibly good simp lemmas in the reverse direction? +theorem Int8.toFin_toBitVec (x : Int8) : x.toBitVec.toFin = x.toUInt8.toFin := rfl +theorem Int16.toFin_toBitVec (x : Int16) : x.toBitVec.toFin = x.toUInt16.toFin := rfl +theorem Int32.toFin_toBitVec (x : Int32) : x.toBitVec.toFin = x.toUInt32.toFin := rfl +theorem Int64.toFin_toBitVec (x : Int64) : x.toBitVec.toFin = x.toUInt64.toFin := rfl +theorem ISize.toFin_toBitVec (x : ISize) : x.toBitVec.toFin = x.toUSize.toFin := rfl + +@[simp] theorem Int8.toBitVec_toUInt8 (x : Int8) : x.toUInt8.toBitVec = x.toBitVec := rfl +@[simp] theorem Int16.toBitVec_toUInt16 (x : Int16) : x.toUInt16.toBitVec = x.toBitVec := rfl +@[simp] theorem Int32.toBitVec_toUInt32 (x : Int32) : x.toUInt32.toBitVec = x.toBitVec := rfl +@[simp] theorem Int64.toBitVec_toUInt64 (x : Int64) : x.toUInt64.toBitVec = x.toBitVec := rfl +@[simp] theorem ISize.toBitVec_toUISize (x : ISize) : x.toUSize.toBitVec = x.toBitVec := rfl + +@[simp] theorem UInt8.ofBitVec_int8ToBitVec (x : Int8) : UInt8.ofBitVec x.toBitVec = x.toUInt8 := rfl +@[simp] theorem UInt16.ofBitVec_int16ToBitVec (x : Int16) : UInt16.ofBitVec x.toBitVec = x.toUInt16 := rfl +@[simp] theorem UInt32.ofBitVec_int32ToBitVec (x : Int32) : UInt32.ofBitVec x.toBitVec = x.toUInt32 := rfl +@[simp] theorem UInt64.ofBitVec_int64ToBitVec (x : Int64) : UInt64.ofBitVec x.toBitVec = x.toUInt64 := rfl +@[simp] theorem USize.ofBitVec_iSizeToBitVec (x : ISize) : USize.ofBitVec x.toBitVec = x.toUSize := rfl + +@[simp] theorem Int8.ofBitVec_toBitVec (x : Int8) : Int8.ofBitVec x.toBitVec = x := rfl +@[simp] theorem Int16.ofBitVec_toBitVec (x : Int16) : Int16.ofBitVec x.toBitVec = x := rfl +@[simp] theorem Int32.ofBitVec_toBitVec (x : Int32) : Int32.ofBitVec x.toBitVec = x := rfl +@[simp] theorem Int64.ofBitVec_toBitVec (x : Int64) : Int64.ofBitVec x.toBitVec = x := rfl +@[simp] theorem ISize.ofBitVec_toBitVec (x : ISize) : ISize.ofBitVec x.toBitVec = x := rfl + +@[simp] theorem Int8.ofBitVec_int16ToBitVec (x : Int16) : Int8.ofBitVec (x.toBitVec.signExtend 8) = x.toInt8 := rfl +@[simp] theorem Int8.ofBitVec_int32ToBitVec (x : Int32) : Int8.ofBitVec (x.toBitVec.signExtend 8) = x.toInt8 := rfl +@[simp] theorem Int8.ofBitVec_int64ToBitVec (x : Int64) : Int8.ofBitVec (x.toBitVec.signExtend 8) = x.toInt8 := rfl +@[simp] theorem Int8.ofBitVec_iSizeToBitVec (x : ISize) : Int8.ofBitVec (x.toBitVec.signExtend 8) = x.toInt8 := rfl + +@[simp] theorem Int16.ofBitVec_int8toBitVec (x : Int8) : Int16.ofBitVec (x.toBitVec.signExtend 16) = x.toInt16 := rfl +@[simp] theorem Int16.ofBitVec_int32ToBitVec (x : Int32) : Int16.ofBitVec (x.toBitVec.signExtend 16) = x.toInt16 := rfl +@[simp] theorem Int16.ofBitVec_int64ToBitVec (x : Int64) : Int16.ofBitVec (x.toBitVec.signExtend 16) = x.toInt16 := rfl +@[simp] theorem Int16.ofBitVec_iSizeToBitVec (x : ISize) : Int16.ofBitVec (x.toBitVec.signExtend 16) = x.toInt16 := rfl + +@[simp] theorem Int32.ofBitVec_int8toBitVec (x : Int8) : Int32.ofBitVec (x.toBitVec.signExtend 32) = x.toInt32 := rfl +@[simp] theorem Int32.ofBitVec_int16ToBitVec (x : Int16) : Int32.ofBitVec (x.toBitVec.signExtend 32) = x.toInt32 := rfl +@[simp] theorem Int32.ofBitVec_int64ToBitVec (x : Int64) : Int32.ofBitVec (x.toBitVec.signExtend 32) = x.toInt32 := rfl +@[simp] theorem Int32.ofBitVec_iSizeToBitVec (x : ISize) : Int32.ofBitVec (x.toBitVec.signExtend 32) = x.toInt32 := rfl + +@[simp] theorem Int64.ofBitVec_int8toBitVec (x : Int8) : Int64.ofBitVec (x.toBitVec.signExtend 64) = x.toInt64 := rfl +@[simp] theorem Int64.ofBitVec_int16ToBitVec (x : Int16) : Int64.ofBitVec (x.toBitVec.signExtend 64) = x.toInt64 := rfl +@[simp] theorem Int64.ofBitVec_int32ToBitVec (x : Int32) : Int64.ofBitVec (x.toBitVec.signExtend 64) = x.toInt64 := rfl +@[simp] theorem Int64.ofBitVec_iSizeToBitVec (x : ISize) : Int64.ofBitVec (x.toBitVec.signExtend 64) = x.toInt64 := rfl + +@[simp] theorem ISize.ofBitVec_int8toBitVec (x : Int8) : ISize.ofBitVec (x.toBitVec.signExtend System.Platform.numBits) = x.toISize := rfl +@[simp] theorem ISize.ofBitVec_int16ToBitVec (x : Int16) : ISize.ofBitVec (x.toBitVec.signExtend System.Platform.numBits) = x.toISize := rfl +@[simp] theorem ISize.ofBitVec_int32ToBitVec (x : Int32) : ISize.ofBitVec (x.toBitVec.signExtend System.Platform.numBits) = x.toISize := rfl +@[simp] theorem ISize.ofBitVec_int64ToBitVec (x : Int64) : ISize.ofBitVec (x.toBitVec.signExtend System.Platform.numBits) = x.toISize := rfl + +@[simp] theorem Int8.toBitVec_ofIntLE (x : Int) (h₁ h₂) : (Int8.ofIntLE x h₁ h₂).toBitVec = BitVec.ofInt 8 x := rfl +@[simp] theorem Int16.toBitVec_ofIntLE (x : Int) (h₁ h₂) : (Int16.ofIntLE x h₁ h₂).toBitVec = BitVec.ofInt 16 x := rfl +@[simp] theorem Int32.toBitVec_ofIntLE (x : Int) (h₁ h₂) : (Int32.ofIntLE x h₁ h₂).toBitVec = BitVec.ofInt 32 x := rfl +@[simp] theorem Int64.toBitVec_ofIntLE (x : Int) (h₁ h₂) : (Int64.ofIntLE x h₁ h₂).toBitVec = BitVec.ofInt 64 x := rfl +@[simp] theorem ISize.toBitVec_ofIntLE (x : Int) (h₁ h₂) : (ISize.ofIntLE x h₁ h₂).toBitVec = BitVec.ofInt System.Platform.numBits x := rfl + +@[simp] theorem Int8.toInt_bmod (x : Int8) : x.toInt.bmod 256 = x.toInt := Int.bmod_eq_self_of_le x.le_toInt x.toInt_lt +@[simp] theorem Int16.toInt_bmod (x : Int16) : x.toInt.bmod 65536 = x.toInt := Int.bmod_eq_self_of_le x.le_toInt x.toInt_lt +@[simp] theorem Int32.toInt_bmod (x : Int32) : x.toInt.bmod 4294967296 = x.toInt := Int.bmod_eq_self_of_le x.le_toInt x.toInt_lt +@[simp] theorem Int64.toInt_bmod (x : Int64) : x.toInt.bmod 18446744073709551616 = x.toInt := Int.bmod_eq_self_of_le x.le_toInt x.toInt_lt +@[simp] theorem ISize.toInt_bmod_two_pow_numBits (x : ISize) : x.toInt.bmod (2 ^ System.Platform.numBits) = x.toInt := by + refine Int.bmod_eq_self_of_le ?_ ?_ + · have := x.two_pow_numBits_le_toInt + cases System.Platform.numBits_eq <;> simp_all + · have := x.toInt_lt_two_pow_numBits + cases System.Platform.numBits_eq <;> simp_all + +@[simp] theorem Int8.toInt_bmod_65536 (x : Int8) : x.toInt.bmod 65536 = x.toInt := + Int.bmod_eq_self_of_le (Int.le_trans (by decide) x.le_toInt) (Int.lt_of_lt_of_le x.toInt_lt (by decide)) +@[simp] theorem Int8.toInt_bmod_4294967296 (x : Int8) : x.toInt.bmod 4294967296 = x.toInt := + Int.bmod_eq_self_of_le (Int.le_trans (by decide) x.le_toInt) (Int.lt_of_lt_of_le x.toInt_lt (by decide)) +@[simp] theorem Int16.toInt_bmod_4294967296 (x : Int16) : x.toInt.bmod 4294967296 = x.toInt := + Int.bmod_eq_self_of_le (Int.le_trans (by decide) x.le_toInt) (Int.lt_of_lt_of_le x.toInt_lt (by decide)) +@[simp] theorem Int8.toInt_bmod_18446744073709551616 (x : Int8) : x.toInt.bmod 18446744073709551616 = x.toInt := + Int.bmod_eq_self_of_le (Int.le_trans (by decide) x.le_toInt) (Int.lt_of_lt_of_le x.toInt_lt (by decide)) +@[simp] theorem Int16.toInt_bmod_18446744073709551616 (x : Int16) : x.toInt.bmod 18446744073709551616 = x.toInt := + Int.bmod_eq_self_of_le (Int.le_trans (by decide) x.le_toInt) (Int.lt_of_lt_of_le x.toInt_lt (by decide)) +@[simp] theorem Int32.toInt_bmod_18446744073709551616 (x : Int32) : x.toInt.bmod 18446744073709551616 = x.toInt := + Int.bmod_eq_self_of_le (Int.le_trans (by decide) x.le_toInt) (Int.lt_of_lt_of_le x.toInt_lt (by decide)) +@[simp] theorem ISize.toInt_bmod_18446744073709551616 (x : ISize) : x.toInt.bmod 18446744073709551616 = x.toInt := + Int.bmod_eq_self_of_le x.le_toInt x.toInt_lt +@[simp] theorem Int8.toInt_bmod_two_pow_numBits (x : Int8) : x.toInt.bmod (2 ^ System.Platform.numBits) = x.toInt := by + refine Int.bmod_eq_self_of_le (Int.le_trans ?_ x.iSizeMinValue_le_toInt) + (Int.lt_of_le_sub_one (Int.le_trans x.toInt_le_iSizeMaxValue ?_)) + all_goals cases System.Platform.numBits_eq <;> simp_all +@[simp] theorem Int16.toInt_bmod_two_pow_numBits (x : Int16) : x.toInt.bmod (2 ^ System.Platform.numBits) = x.toInt := by + refine Int.bmod_eq_self_of_le (Int.le_trans ?_ x.iSizeMinValue_le_toInt) + (Int.lt_of_le_sub_one (Int.le_trans x.toInt_le_iSizeMaxValue ?_)) + all_goals cases System.Platform.numBits_eq <;> simp_all +@[simp] theorem Int32.toInt_bmod_two_pow_numBits (x : Int32) : x.toInt.bmod (2 ^ System.Platform.numBits) = x.toInt := by + refine Int.bmod_eq_self_of_le (Int.le_trans ?_ x.iSizeMinValue_le_toInt) + (Int.lt_of_le_sub_one (Int.le_trans x.toInt_le_iSizeMaxValue ?_)) + all_goals cases System.Platform.numBits_eq <;> simp_all + +@[simp] theorem BitVec.ofInt_int8ToInt (x : Int8) : BitVec.ofInt 8 x.toInt = x.toBitVec := BitVec.eq_of_toInt_eq (by simp) +@[simp] theorem BitVec.ofInt_int16ToInt (x : Int16) : BitVec.ofInt 16 x.toInt = x.toBitVec := BitVec.eq_of_toInt_eq (by simp) +@[simp] theorem BitVec.ofInt_int32ToInt (x : Int32) : BitVec.ofInt 32 x.toInt = x.toBitVec := BitVec.eq_of_toInt_eq (by simp) +@[simp] theorem BitVec.ofInt_int64ToInt (x : Int64) : BitVec.ofInt 64 x.toInt = x.toBitVec := BitVec.eq_of_toInt_eq (by simp) +@[simp] theorem BitVec.ofInt_iSizeToInt (x : ISize) : BitVec.ofInt System.Platform.numBits x.toInt = x.toBitVec := + BitVec.eq_of_toInt_eq (by simp) + +@[simp] theorem Int8.ofIntLE_toInt (x : Int8) : Int8.ofIntLE x.toInt x.minValue_le_toInt x.toInt_le = x := Int8.toBitVec.inj (by simp) +@[simp] theorem Int16.ofIntLE_toInt (x : Int16) : Int16.ofIntLE x.toInt x.minValue_le_toInt x.toInt_le = x := Int16.toBitVec.inj (by simp) +@[simp] theorem Int32.ofIntLE_toInt (x : Int32) : Int32.ofIntLE x.toInt x.minValue_le_toInt x.toInt_le = x := Int32.toBitVec.inj (by simp) +@[simp] theorem Int64.ofIntLE_toInt (x : Int64) : Int64.ofIntLE x.toInt x.minValue_le_toInt x.toInt_le = x := Int64.toBitVec.inj (by simp) +@[simp] theorem ISize.ofIntLE_toInt (x : ISize) : ISize.ofIntLE x.toInt x.minValue_le_toInt x.toInt_le = x := ISize.toBitVec.inj (by simp) + +theorem Int8.ofIntLE_int16ToInt (x : Int16) {h₁ h₂} : Int8.ofIntLE x.toInt h₁ h₂ = x.toInt8 := rfl +theorem Int8.ofIntLE_int32ToInt (x : Int32) {h₁ h₂} : Int8.ofIntLE x.toInt h₁ h₂ = x.toInt8 := rfl +theorem Int8.ofIntLE_int64ToInt (x : Int64) {h₁ h₂} : Int8.ofIntLE x.toInt h₁ h₂ = x.toInt8 := rfl +theorem Int8.ofIntLE_iSizeToInt (x : ISize) {h₁ h₂} : Int8.ofIntLE x.toInt h₁ h₂ = x.toInt8 := rfl + +@[simp] theorem Int16.ofIntLE_int8ToInt (x : Int8) : + Int16.ofIntLE x.toInt (Int.le_trans (by decide) x.minValue_le_toInt) (Int.le_trans x.toInt_le (by decide)) = x.toInt16 := rfl +theorem Int16.ofIntLE_int32ToInt (x : Int32) {h₁ h₂} : Int16.ofIntLE x.toInt h₁ h₂ = x.toInt16 := rfl +theorem Int16.ofIntLE_int64ToInt (x : Int64) {h₁ h₂} : Int16.ofIntLE x.toInt h₁ h₂ = x.toInt16 := rfl +theorem Int16.ofIntLE_iSizeToInt (x : ISize) {h₁ h₂} : Int16.ofIntLE x.toInt h₁ h₂ = x.toInt16 := rfl + +@[simp] theorem Int32.ofIntLE_int8ToInt (x : Int8) : + Int32.ofIntLE x.toInt (Int.le_trans (by decide) x.minValue_le_toInt) (Int.le_trans x.toInt_le (by decide)) = x.toInt32 := rfl +@[simp] theorem Int32.ofIntLE_int16ToInt (x : Int16) : + Int32.ofIntLE x.toInt (Int.le_trans (by decide) x.minValue_le_toInt) (Int.le_trans x.toInt_le (by decide)) = x.toInt32 := rfl +theorem Int32.ofIntLE_int64ToInt (x : Int64) {h₁ h₂} : Int32.ofIntLE x.toInt h₁ h₂ = x.toInt32 := rfl +theorem Int32.ofIntLE_iSizeToInt (x : ISize) {h₁ h₂} : Int32.ofIntLE x.toInt h₁ h₂ = x.toInt32 := rfl + +@[simp] theorem Int64.ofIntLE_int8ToInt (x : Int8) : + Int64.ofIntLE x.toInt (Int.le_trans (by decide) x.minValue_le_toInt) (Int.le_trans x.toInt_le (by decide)) = x.toInt64 := rfl +@[simp] theorem Int64.ofIntLE_int16ToInt (x : Int16) : + Int64.ofIntLE x.toInt (Int.le_trans (by decide) x.minValue_le_toInt) (Int.le_trans x.toInt_le (by decide)) = x.toInt64 := rfl +@[simp] theorem Int64.ofIntLE_int32ToInt (x : Int32) : + Int64.ofIntLE x.toInt (Int.le_trans (by decide) x.minValue_le_toInt) (Int.le_trans x.toInt_le (by decide)) = x.toInt64 := rfl +@[simp] theorem Int64.ofIntLE_iSizeToInt (x : ISize) : + Int64.ofIntLE x.toInt x.int64MinValue_le_toInt x.toInt_le_int64MaxValue = x.toInt64 := rfl + +@[simp] theorem ISize.ofIntLE_int8ToInt (x : Int8) : + ISize.ofIntLE x.toInt x.iSizeMinValue_le_toInt x.toInt_le_iSizeMaxValue = x.toISize := rfl +@[simp] theorem ISize.ofIntLE_int16ToInt (x : Int16) : + ISize.ofIntLE x.toInt x.iSizeMinValue_le_toInt x.toInt_le_iSizeMaxValue = x.toISize := rfl +@[simp] theorem ISize.ofIntLE_int32ToInt (x : Int32) : + ISize.ofIntLE x.toInt x.iSizeMinValue_le_toInt x.toInt_le_iSizeMaxValue = x.toISize := rfl +theorem ISize.ofIntLE_int64ToInt (x : Int64) {h₁ h₂} : ISize.ofIntLE x.toInt h₁ h₂ = x.toISize := rfl + +@[simp] theorem Int8.ofInt_toInt (x : Int8) : Int8.ofInt x.toInt = x := Int8.toBitVec.inj (by simp) +@[simp] theorem Int16.ofInt_toInt (x : Int16) : Int16.ofInt x.toInt = x := Int16.toBitVec.inj (by simp) +@[simp] theorem Int32.ofInt_toInt (x : Int32) : Int32.ofInt x.toInt = x := Int32.toBitVec.inj (by simp) +@[simp] theorem Int64.ofInt_toInt (x : Int64) : Int64.ofInt x.toInt = x := Int64.toBitVec.inj (by simp) +@[simp] theorem ISize.ofInt_toInt (x : ISize) : ISize.ofInt x.toInt = x := ISize.toBitVec.inj (by simp) + +@[simp] theorem Int8.ofInt_int16ToInt (x : Int16) : Int8.ofInt x.toInt = x.toInt8 := rfl +@[simp] theorem Int8.ofInt_int32ToInt (x : Int32) : Int8.ofInt x.toInt = x.toInt8 := rfl +@[simp] theorem Int8.ofInt_int64ToInt (x : Int64) : Int8.ofInt x.toInt = x.toInt8 := rfl +@[simp] theorem Int8.ofInt_iSizeToInt (x : ISize) : Int8.ofInt x.toInt = x.toInt8 := rfl + +@[simp] theorem Int16.ofInt_int8ToInt (x : Int8) : Int16.ofInt x.toInt = x.toInt16 := rfl +@[simp] theorem Int16.ofInt_int32ToInt (x : Int32) : Int16.ofInt x.toInt = x.toInt16 := rfl +@[simp] theorem Int16.ofInt_int64ToInt (x : Int64) : Int16.ofInt x.toInt = x.toInt16 := rfl +@[simp] theorem Int16.ofInt_iSizeToInt (x : ISize) : Int16.ofInt x.toInt = x.toInt16 := rfl + +@[simp] theorem Int32.ofInt_int8ToInt (x : Int8) : Int32.ofInt x.toInt = x.toInt32 := rfl +@[simp] theorem Int32.ofInt_int16ToInt (x : Int16) : Int32.ofInt x.toInt = x.toInt32 := rfl +@[simp] theorem Int32.ofInt_int64ToInt (x : Int64) : Int32.ofInt x.toInt = x.toInt32 := rfl +@[simp] theorem Int32.ofInt_iSizeToInt (x : ISize) : Int32.ofInt x.toInt = x.toInt32 := rfl + +@[simp] theorem Int64.ofInt_int8ToInt (x : Int8) : Int64.ofInt x.toInt = x.toInt64 := rfl +@[simp] theorem Int64.ofInt_int16ToInt (x : Int16) : Int64.ofInt x.toInt = x.toInt64 := rfl +@[simp] theorem Int64.ofInt_int32ToInt (x : Int32) : Int64.ofInt x.toInt = x.toInt64 := rfl +@[simp] theorem Int64.ofInt_iSizeToInt (x : ISize) : Int64.ofInt x.toInt = x.toInt64 := rfl + +@[simp] theorem ISize.ofInt_int8ToInt (x : Int8) : ISize.ofInt x.toInt = x.toISize := rfl +@[simp] theorem ISize.ofInt_int16ToInt (x : Int16) : ISize.ofInt x.toInt = x.toISize := rfl +@[simp] theorem ISize.ofInt_int32ToInt (x : Int32) : ISize.ofInt x.toInt = x.toISize := rfl +@[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₂)] +@[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₂)] +@[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₂)] +@[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₂)] +@[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₁ + · apply Int.lt_of_le_sub_one + simpa using h₂ + +theorem Int8.ofIntLE_eq_ofIntTruncate {x : Int} {h₁ h₂} : (ofIntLE x h₁ h₂) = ofIntTruncate x := by + rw [ofIntTruncate, dif_pos h₁, dif_pos h₂] +theorem Int16.ofIntLE_eq_ofIntTruncate {x : Int} {h₁ h₂} : (ofIntLE x h₁ h₂) = ofIntTruncate x := by + rw [ofIntTruncate, dif_pos h₁, dif_pos h₂] +theorem Int32.ofIntLE_eq_ofIntTruncate {x : Int} {h₁ h₂} : (ofIntLE x h₁ h₂) = ofIntTruncate x := by + rw [ofIntTruncate, dif_pos h₁, dif_pos h₂] +theorem Int64.ofIntLE_eq_ofIntTruncate {x : Int} {h₁ h₂} : (ofIntLE x h₁ h₂) = ofIntTruncate x := by + rw [ofIntTruncate, dif_pos h₁, dif_pos 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.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] +theorem Int16.toInt_ofIntTruncate {x : Int} (h₁ : Int16.minValue.toInt ≤ x) + (h₂ : x ≤ Int16.maxValue.toInt) : (Int16.ofIntTruncate x).toInt = x := by + rw [← ofIntLE_eq_ofIntTruncate (h₁ := h₁) (h₂ := h₂), toInt_ofIntLE] +theorem Int32.toInt_ofIntTruncate {x : Int} (h₁ : Int32.minValue.toInt ≤ x) + (h₂ : x ≤ Int32.maxValue.toInt) : (Int32.ofIntTruncate x).toInt = x := by + rw [← ofIntLE_eq_ofIntTruncate (h₁ := h₁) (h₂ := h₂), toInt_ofIntLE] +theorem Int64.toInt_ofIntTruncate {x : Int} (h₁ : Int64.minValue.toInt ≤ x) + (h₂ : x ≤ Int64.maxValue.toInt) : (Int64.ofIntTruncate x).toInt = x := by + rw [← ofIntLE_eq_ofIntTruncate (h₁ := h₁) (h₂ := h₂), toInt_ofIntLE] +theorem ISize.toInt_ofIntTruncate {x : Int} (h₁ : ISize.minValue.toInt ≤ x) + (h₂ : x ≤ ISize.maxValue.toInt) : (ISize.ofIntTruncate x).toInt = x := by + rw [← ofIntLE_eq_ofIntTruncate (h₁ := h₁) (h₂ := h₂), toInt_ofIntLE] + +@[simp] theorem Int8.ofIntTruncate_toInt (x : Int8) : Int8.ofIntTruncate x.toInt = x := + Int8.toInt.inj (toInt_ofIntTruncate x.minValue_le_toInt x.toInt_le) +@[simp] theorem Int16.ofIntTruncate_toInt (x : Int16) : Int16.ofIntTruncate x.toInt = x := + Int16.toInt.inj (toInt_ofIntTruncate x.minValue_le_toInt x.toInt_le) +@[simp] theorem Int32.ofIntTruncate_toInt (x : Int32) : Int32.ofIntTruncate x.toInt = x := + Int32.toInt.inj (toInt_ofIntTruncate x.minValue_le_toInt x.toInt_le) +@[simp] theorem Int64.ofIntTruncate_toInt (x : Int64) : Int64.ofIntTruncate x.toInt = x := + Int64.toInt.inj (toInt_ofIntTruncate x.minValue_le_toInt x.toInt_le) +@[simp] theorem ISize.ofIntTruncate_toInt (x : ISize) : ISize.ofIntTruncate x.toInt = x := + ISize.toInt.inj (toInt_ofIntTruncate x.minValue_le_toInt x.toInt_le) + +@[simp] theorem Int16.ofIntTruncate_int8ToInt (x : Int8) : Int16.ofIntTruncate x.toInt = x.toInt16 := + Int16.toInt.inj (by + rw [toInt_ofIntTruncate, Int8.toInt_toInt16] + · exact Int.le_trans (by decide) x.minValue_le_toInt + · exact Int.le_trans x.toInt_le (by decide)) +@[simp] theorem Int32.ofIntTruncate_int8ToInt (x : Int8) : Int32.ofIntTruncate x.toInt = x.toInt32 := + Int32.toInt.inj (by + rw [toInt_ofIntTruncate, Int8.toInt_toInt32] + · exact Int.le_trans (by decide) x.minValue_le_toInt + · exact Int.le_trans x.toInt_le (by decide)) +@[simp] theorem Int64.ofIntTruncate_int8ToInt (x : Int8) : Int64.ofIntTruncate x.toInt = x.toInt64 := + Int64.toInt.inj (by + rw [toInt_ofIntTruncate, Int8.toInt_toInt64] + · exact Int.le_trans (by decide) x.minValue_le_toInt + · exact Int.le_trans x.toInt_le (by decide)) +@[simp] theorem ISize.ofIntTruncate_int8ToInt (x : Int8) : ISize.ofIntTruncate x.toInt = x.toISize := + ISize.toInt.inj (by + rw [toInt_ofIntTruncate, Int8.toInt_toISize] + · exact x.iSizeMinValue_le_toInt + · exact x.toInt_le_iSizeMaxValue) + +@[simp] theorem Int32.ofIntTruncate_int16ToInt (x : Int16) : Int32.ofIntTruncate x.toInt = x.toInt32 := + Int32.toInt.inj (by + rw [toInt_ofIntTruncate, Int16.toInt_toInt32] + · exact Int.le_trans (by decide) x.minValue_le_toInt + · exact Int.le_trans x.toInt_le (by decide)) +@[simp] theorem Int64.ofIntTruncate_int16ToInt (x : Int16) : Int64.ofIntTruncate x.toInt = x.toInt64 := + Int64.toInt.inj (by + rw [toInt_ofIntTruncate, Int16.toInt_toInt64] + · exact Int.le_trans (by decide) x.minValue_le_toInt + · exact Int.le_trans x.toInt_le (by decide)) +@[simp] theorem ISize.ofIntTruncate_int16ToInt (x : Int16) : ISize.ofIntTruncate x.toInt = x.toISize := + ISize.toInt.inj (by + rw [toInt_ofIntTruncate, Int16.toInt_toISize] + · exact x.iSizeMinValue_le_toInt + · exact x.toInt_le_iSizeMaxValue) + +@[simp] theorem Int64.ofIntTruncate_int32ToInt (x : Int32) : Int64.ofIntTruncate x.toInt = x.toInt64 := + Int64.toInt.inj (by + rw [toInt_ofIntTruncate, Int32.toInt_toInt64] + · exact Int.le_trans (by decide) x.minValue_le_toInt + · exact Int.le_trans x.toInt_le (by decide)) +@[simp] theorem ISize.ofIntTruncate_int32ToInt (x : Int32) : ISize.ofIntTruncate x.toInt = x.toISize := + ISize.toInt.inj (by + rw [toInt_ofIntTruncate, Int32.toInt_toISize] + · exact x.iSizeMinValue_le_toInt + · exact x.toInt_le_iSizeMaxValue) + +@[simp] theorem Int64.ofIntTruncate_iSizeToInt (x : ISize) : Int64.ofIntTruncate x.toInt = x.toInt64 := + Int64.toInt.inj (by + rw [toInt_ofIntTruncate, ISize.toInt_toInt64] + · exact x.int64MinValue_le_toInt + · exact x.toInt_le_int64MaxValue) + +theorem Int8.le_iff_toInt_le {x y : Int8} : x ≤ y ↔ x.toInt ≤ y.toInt := BitVec.sle_iff_toInt_le +theorem Int16.le_iff_toInt_le {x y : Int16} : x ≤ y ↔ x.toInt ≤ y.toInt := BitVec.sle_iff_toInt_le +theorem Int32.le_iff_toInt_le {x y : Int32} : x ≤ y ↔ x.toInt ≤ y.toInt := BitVec.sle_iff_toInt_le +theorem Int64.le_iff_toInt_le {x y : Int64} : x ≤ y ↔ x.toInt ≤ y.toInt := BitVec.sle_iff_toInt_le +theorem ISize.le_iff_toInt_le {x y : ISize} : x ≤ y ↔ x.toInt ≤ y.toInt := BitVec.sle_iff_toInt_le + +theorem Int8.cast_toNatClampNeg (x : Int8) (hx : 0 ≤ x) : x.toNatClampNeg = x.toInt := by + rw [toNatClampNeg, toInt, Int.toNat_of_nonneg (by simpa using le_iff_toInt_le.1 hx)] +theorem Int16.cast_toNatClampNeg (x : Int16) (hx : 0 ≤ x) : x.toNatClampNeg = x.toInt := by + rw [toNatClampNeg, toInt, Int.toNat_of_nonneg (by simpa using le_iff_toInt_le.1 hx)] +theorem Int32.cast_toNatClampNeg (x : Int32) (hx : 0 ≤ x) : x.toNatClampNeg = x.toInt := by + rw [toNatClampNeg, toInt, Int.toNat_of_nonneg (by simpa using le_iff_toInt_le.1 hx)] +theorem Int64.cast_toNatClampNeg (x : Int64) (hx : 0 ≤ x) : x.toNatClampNeg = x.toInt := by + rw [toNatClampNeg, toInt, Int.toNat_of_nonneg (by simpa using le_iff_toInt_le.1 hx)] +theorem ISize.cast_toNatClampNeg (x : ISize) (hx : 0 ≤ x) : x.toNatClampNeg = x.toInt := by + rw [toNatClampNeg, toInt, Int.toNat_of_nonneg (by simpa using le_iff_toInt_le.1 hx)] + +theorem Int8.ofNat_toNatClampNeg (x : Int8) (hx : 0 ≤ x) : Int8.ofNat x.toNatClampNeg = x := + Int8.toInt.inj (by rw [Int8.toInt_ofNat_of_lt x.toNatClampNeg_lt, cast_toNatClampNeg _ hx]) +theorem Int16.ofNat_toNatClampNeg (x : Int16) (hx : 0 ≤ x) : Int16.ofNat x.toNatClampNeg = x := + Int16.toInt.inj (by rw [Int16.toInt_ofNat_of_lt x.toNatClampNeg_lt, cast_toNatClampNeg _ hx]) +theorem Int32.ofNat_toNatClampNeg (x : Int32) (hx : 0 ≤ x) : Int32.ofNat x.toNatClampNeg = x := + Int32.toInt.inj (by rw [Int32.toInt_ofNat_of_lt x.toNatClampNeg_lt, cast_toNatClampNeg _ hx]) +theorem Int64.ofNat_toNatClampNeg (x : Int64) (hx : 0 ≤ x) : Int64.ofNat x.toNatClampNeg = x := + Int64.toInt.inj (by rw [Int64.toInt_ofNat_of_lt x.toNatClampNeg_lt, cast_toNatClampNeg _ hx]) +theorem ISize.ofNat_toNatClampNeg (x : ISize) (hx : 0 ≤ x) : ISize.ofNat x.toNatClampNeg = x := + ISize.toInt.inj (by rw [ISize.toInt_ofNat_of_lt_two_pow_numBits x.toNatClampNeg_lt_two_pow_numBits, + cast_toNatClampNeg _ hx]) + +theorem Int16.ofNat_int8ToNatClampNeg (x : Int8) (hx : 0 ≤ x) : Int16.ofNat x.toNatClampNeg = x.toInt16 := + Int16.toInt.inj (by rw [Int16.toInt_ofNat_of_lt (Nat.lt_of_lt_of_le x.toNatClampNeg_lt (by decide)), + Int8.cast_toNatClampNeg _ hx, Int8.toInt_toInt16]) +theorem Int32.ofNat_int8ToNatClampNeg (x : Int8) (hx : 0 ≤ x) : Int32.ofNat x.toNatClampNeg = x.toInt32 := + Int32.toInt.inj (by rw [Int32.toInt_ofNat_of_lt (Nat.lt_of_lt_of_le x.toNatClampNeg_lt (by decide)), + Int8.cast_toNatClampNeg _ hx, Int8.toInt_toInt32]) +theorem Int64.ofNat_int8ToNatClampNeg (x : Int8) (hx : 0 ≤ x) : Int64.ofNat x.toNatClampNeg = x.toInt64 := + Int64.toInt.inj (by rw [Int64.toInt_ofNat_of_lt (Nat.lt_of_lt_of_le x.toNatClampNeg_lt (by decide)), + Int8.cast_toNatClampNeg _ hx, Int8.toInt_toInt64]) +theorem ISize.ofNat_int8ToNatClampNeg (x : Int8) (hx : 0 ≤ x) : ISize.ofNat x.toNatClampNeg = x.toISize := + ISize.toInt.inj (by rw [ISize.toInt_ofNat_of_lt (Nat.lt_of_lt_of_le x.toNatClampNeg_lt (by decide)), + Int8.cast_toNatClampNeg _ hx, Int8.toInt_toISize]) + +theorem Int32.ofNat_int16ToNatClampNeg (x : Int16) (hx : 0 ≤ x) : Int32.ofNat x.toNatClampNeg = x.toInt32 := + Int32.toInt.inj (by rw [Int32.toInt_ofNat_of_lt (Nat.lt_of_lt_of_le x.toNatClampNeg_lt (by decide)), + Int16.cast_toNatClampNeg _ hx, Int16.toInt_toInt32]) +theorem Int64.ofNat_int16ToNatClampNeg (x : Int16) (hx : 0 ≤ x) : Int64.ofNat x.toNatClampNeg = x.toInt64 := + Int64.toInt.inj (by rw [Int64.toInt_ofNat_of_lt (Nat.lt_of_lt_of_le x.toNatClampNeg_lt (by decide)), + Int16.cast_toNatClampNeg _ hx, Int16.toInt_toInt64]) +theorem ISize.ofNat_int16ToNatClampNeg (x : Int16) (hx : 0 ≤ x) : ISize.ofNat x.toNatClampNeg = x.toISize := + ISize.toInt.inj (by rw [ISize.toInt_ofNat_of_lt (Nat.lt_of_lt_of_le x.toNatClampNeg_lt (by decide)), + Int16.cast_toNatClampNeg _ hx, Int16.toInt_toISize]) + +theorem Int64.ofNat_int32ToNatClampNeg (x : Int32) (hx : 0 ≤ x) : Int64.ofNat x.toNatClampNeg = x.toInt64 := + Int64.toInt.inj (by rw [Int64.toInt_ofNat_of_lt (Nat.lt_of_lt_of_le x.toNatClampNeg_lt (by decide)), + Int32.cast_toNatClampNeg _ hx, Int32.toInt_toInt64]) +theorem ISize.ofNat_int32ToNatClampNeg (x : Int32) (hx : 0 ≤ x) : ISize.ofNat x.toNatClampNeg = x.toISize := + ISize.toInt.inj (by rw [ISize.toInt_ofNat_of_lt (Nat.lt_of_lt_of_le x.toNatClampNeg_lt (by decide)), + Int32.cast_toNatClampNeg _ hx, Int32.toInt_toISize]) + +@[simp] theorem Int8.toInt8_toInt16 (n : Int8) : n.toInt16.toInt8 = n := + Int8.toInt.inj (by simp) +@[simp] theorem Int8.toInt8_toInt32 (n : Int8) : n.toInt32.toInt8 = n := + Int8.toInt.inj (by simp) +@[simp] theorem Int8.toInt8_toInt64 (n : Int8) : n.toInt64.toInt8 = n := + Int8.toInt.inj (by simp) +@[simp] theorem Int8.toInt8_toISize (n : Int8) : n.toISize.toInt8 = n := + Int8.toInt.inj (by simp) + +@[simp] theorem Int8.toInt16_toInt32 (n : Int8) : n.toInt32.toInt16 = n.toInt16 := + Int16.toInt.inj (by simp) +@[simp] theorem Int8.toInt16_toInt64 (n : Int8) : n.toInt64.toInt16 = n.toInt16 := + Int16.toInt.inj (by simp) +@[simp] theorem Int8.toInt16_toISize (n : Int8) : n.toISize.toInt16 = n.toInt16 := + Int16.toInt.inj (by simp) + +@[simp] theorem Int8.toInt32_toInt16 (n : Int8) : n.toInt16.toInt32 = n.toInt32 := + Int32.toInt.inj (by simp) +@[simp] theorem Int8.toInt32_toInt64 (n : Int8) : n.toInt64.toInt32 = n.toInt32 := + Int32.toInt.inj (by simp) +@[simp] theorem Int8.toInt32_toISize (n : Int8) : n.toISize.toInt32 = n.toInt32 := + Int32.toInt.inj (by simp) + +@[simp] theorem Int8.toInt64_toInt16 (n : Int8) : n.toInt16.toInt64 = n.toInt64 := + Int64.toInt.inj (by simp) +@[simp] theorem Int8.toInt64_toInt32 (n : Int8) : n.toInt32.toInt64 = n.toInt64 := + Int64.toInt.inj (by simp) +@[simp] theorem Int8.toInt64_toISize (n : Int8) : n.toISize.toInt64 = n.toInt64 := + Int64.toInt.inj (by simp) + +@[simp] theorem Int8.toISize_toInt16 (n : Int8) : n.toInt16.toISize = n.toISize := + ISize.toInt.inj (by simp) +@[simp] theorem Int8.toISize_toInt32 (n : Int8) : n.toInt32.toISize = n.toISize := + ISize.toInt.inj (by simp) +@[simp] theorem Int8.toISize_toInt64 (n : Int8) : n.toInt64.toISize = n.toISize := + ISize.toInt.inj (by simp) + +@[simp] theorem Int16.toInt8_toInt32 (n : Int16) : n.toInt32.toInt8 = n.toInt8 := + Int8.toInt.inj (by simp) +@[simp] theorem Int16.toInt8_toInt64 (n : Int16) : n.toInt64.toInt8 = n.toInt8 := + Int8.toInt.inj (by simp) +@[simp] theorem Int16.toInt8_toISize (n : Int16) : n.toISize.toInt8 = n.toInt8 := + Int8.toInt.inj (by simp) + +@[simp] theorem Int16.toInt16_toInt32 (n : Int16) : n.toInt32.toInt16 = n := + Int16.toInt.inj (by simp) +@[simp] theorem Int16.toInt16_toInt64 (n : Int16) : n.toInt64.toInt16 = n := + Int16.toInt.inj (by simp) +@[simp] theorem Int16.toInt16_toISize (n : Int16) : n.toISize.toInt16 = n := + Int16.toInt.inj (by simp) + +@[simp] theorem Int16.toInt32_toInt64 (n : Int16) : n.toInt64.toInt32 = n.toInt32 := + Int32.toInt.inj (by simp) +@[simp] theorem Int16.toInt32_toISize (n : Int16) : n.toISize.toInt32 = n.toInt32 := + Int32.toInt.inj (by simp) + +@[simp] theorem Int16.toInt64_toInt32 (n : Int16) : n.toInt32.toInt64 = n.toInt64 := + Int64.toInt.inj (by simp) +@[simp] theorem Int16.toInt64_toISize (n : Int16) : n.toISize.toInt64 = n.toInt64 := + Int64.toInt.inj (by simp) + +@[simp] theorem Int16.toISize_toInt32 (n : Int16) : n.toInt32.toISize = n.toISize := + ISize.toInt.inj (by simp) +@[simp] theorem Int16.toISize_toInt64 (n : Int16) : n.toInt64.toISize = n.toISize := + ISize.toInt.inj (by simp) + +@[simp] theorem Int32.toInt8_toInt16 (n : Int32) : n.toInt16.toInt8 = n.toInt8 := + Int8.toInt.inj (by simpa using Int.bmod_bmod_of_dvd (by decide)) +@[simp] theorem Int32.toInt8_toInt64 (n : Int32) : n.toInt64.toInt8 = n.toInt8 := + Int8.toInt.inj (by simp) +@[simp] theorem Int32.toInt8_toISize (n : Int32) : n.toISize.toInt8 = n.toInt8 := + Int8.toInt.inj (by simp) + +@[simp] theorem Int32.toInt16_toInt64 (n : Int32) : n.toInt64.toInt16 = n.toInt16 := + Int16.toInt.inj (by simp) +@[simp] theorem Int32.toInt16_toISize (n : Int32) : n.toISize.toInt16 = n.toInt16 := + Int16.toInt.inj (by simp) + +@[simp] theorem Int32.toInt32_toInt64 (n : Int32) : n.toInt64.toInt32 = n := + Int32.toInt.inj (by simp) +@[simp] theorem Int32.toInt32_toISize (n : Int32) : n.toISize.toInt32 = n := + Int32.toInt.inj (by simp) + +@[simp] theorem Int32.toInt64_toISize (n : Int32) : n.toISize.toInt64 = n.toInt64 := + Int64.toInt.inj (by simp) + +@[simp] theorem Int32.toISize_toInt64 (n : Int32) : n.toInt64.toISize = n.toISize := + ISize.toInt.inj (by simp) + +@[simp] theorem Int64.toInt8_toInt16 (n : Int64) : n.toInt16.toInt8 = n.toInt8 := + Int8.toInt.inj (by simpa using Int.bmod_bmod_of_dvd (by decide)) +@[simp] theorem Int64.toInt8_toInt32 (n : Int64) : n.toInt32.toInt8 = n.toInt8 := + Int8.toInt.inj (by simpa using Int.bmod_bmod_of_dvd (by decide)) +@[simp] theorem Int64.toInt8_toISize (n : Int64) : n.toISize.toInt8 = n.toInt8 := + Int8.toInt.inj (by simpa using Int.bmod_bmod_of_dvd (by cases System.Platform.numBits_eq <;> simp_all)) + +@[simp] theorem Int64.toInt16_toInt32 (n : Int64) : n.toInt32.toInt16 = n.toInt16 := + Int16.toInt.inj (by simpa using Int.bmod_bmod_of_dvd (by decide)) +@[simp] theorem Int64.toInt16_toISize (n : Int64) : n.toISize.toInt16 = n.toInt16 := + Int16.toInt.inj (by simpa using Int.bmod_bmod_of_dvd (by cases System.Platform.numBits_eq <;> simp_all)) + +@[simp] theorem Int64.toInt32_toISize (n : Int64) : n.toISize.toInt32 = n.toInt32 := + Int32.toInt.inj (by simpa using Int.bmod_bmod_of_dvd (by cases System.Platform.numBits_eq <;> simp_all)) + +@[simp] theorem ISize.toInt8_toInt16 (n : ISize) : n.toInt16.toInt8 = n.toInt8 := + Int8.toInt.inj (by simpa using Int.bmod_bmod_of_dvd (by decide)) +@[simp] theorem ISize.toInt8_toInt32 (n : ISize) : n.toInt32.toInt8 = n.toInt8 := + Int8.toInt.inj (by simpa using Int.bmod_bmod_of_dvd (by decide)) +@[simp] theorem ISize.toInt8_toInt64 (n : ISize) : n.toInt64.toInt8 = n.toInt8 := + Int8.toInt.inj (by simp) + +@[simp] theorem ISize.toInt16_toInt32 (n : ISize) : n.toInt32.toInt16 = n.toInt16 := + Int16.toInt.inj (by simpa using Int.bmod_bmod_of_dvd (by decide)) +@[simp] theorem ISize.toInt16_toInt64 (n : ISize) : n.toInt64.toInt16 = n.toInt16 := + Int16.toInt.inj (by simp) + +@[simp] theorem ISize.toInt32_toInt64 (n : ISize) : n.toInt64.toInt32 = n.toInt32 := + Int32.toInt.inj (by simp) + +@[simp] theorem ISize.toISize_toInt64 (n : ISize) : n.toInt64.toISize = n := + ISize.toInt.inj (by simp)