feat: IntX modulo lemmas (#7704)
This PR adds lemmas about the modulo operation defined on signed bounded integers. The results depend on the lemma ```lean theorem BitVec.toInt_srem (a b : BitVec w) : (a.srem b).toInt = a.toInt.tmod b.toInt := sorry ``` which is missing at the time of posting the PR.
This commit is contained in:
Markus Himmel
GitHub
parent
5348ce9632
commit
1bf2d8eba2
1 changed files with 118 additions and 0 deletions
|
|
@ -3271,3 +3271,121 @@ protected theorem Int64.ne_of_lt {a b : Int64} : a < b → a ≠ b := by
|
|||
simpa [Int64.lt_iff_toInt_lt, ← Int64.toInt_inj] using Int.ne_of_lt
|
||||
protected theorem ISize.ne_of_lt {a b : ISize} : a < b → a ≠ b := by
|
||||
simpa [ISize.lt_iff_toInt_lt, ← ISize.toInt_inj] using Int.ne_of_lt
|
||||
|
||||
@[simp] theorem Int8.toInt_mod (a b : Int8) : (a % b).toInt = a.toInt.tmod b.toInt := by
|
||||
rw [← toInt_toBitVec, Int8.toBitVec_mod, BitVec.toInt_srem, toInt_toBitVec, toInt_toBitVec]
|
||||
@[simp] theorem Int16.toInt_mod (a b : Int16) : (a % b).toInt = a.toInt.tmod b.toInt := by
|
||||
rw [← toInt_toBitVec, Int16.toBitVec_mod, BitVec.toInt_srem, toInt_toBitVec, toInt_toBitVec]
|
||||
@[simp] theorem Int32.toInt_mod (a b : Int32) : (a % b).toInt = a.toInt.tmod b.toInt := by
|
||||
rw [← toInt_toBitVec, Int32.toBitVec_mod, BitVec.toInt_srem, toInt_toBitVec, toInt_toBitVec]
|
||||
@[simp] theorem Int64.toInt_mod (a b : Int64) : (a % b).toInt = a.toInt.tmod b.toInt := by
|
||||
rw [← toInt_toBitVec, Int64.toBitVec_mod, BitVec.toInt_srem, toInt_toBitVec, toInt_toBitVec]
|
||||
@[simp] theorem ISize.toInt_mod (a b : ISize) : (a % b).toInt = a.toInt.tmod b.toInt := by
|
||||
rw [← toInt_toBitVec, ISize.toBitVec_mod, BitVec.toInt_srem, toInt_toBitVec, toInt_toBitVec]
|
||||
|
||||
@[simp] theorem Int8.toInt16_mod (a b : Int8) : (a % b).toInt16 = a.toInt16 % b.toInt16 := Int16.toInt.inj (by simp)
|
||||
@[simp] theorem Int8.toInt32_mod (a b : Int8) : (a % b).toInt32 = a.toInt32 % b.toInt32 := Int32.toInt.inj (by simp)
|
||||
@[simp] theorem Int8.toInt64_mod (a b : Int8) : (a % b).toInt64 = a.toInt64 % b.toInt64 := Int64.toInt.inj (by simp)
|
||||
@[simp] theorem Int8.toISize_mod (a b : Int8) : (a % b).toISize = a.toISize % b.toISize := ISize.toInt.inj (by simp)
|
||||
|
||||
@[simp] theorem Int16.toInt32_mod (a b : Int16) : (a % b).toInt32 = a.toInt32 % b.toInt32 := Int32.toInt.inj (by simp)
|
||||
@[simp] theorem Int16.toInt64_mod (a b : Int16) : (a % b).toInt64 = a.toInt64 % b.toInt64 := Int64.toInt.inj (by simp)
|
||||
@[simp] theorem Int16.toISize_mod (a b : Int16) : (a % b).toISize = a.toISize % b.toISize := ISize.toInt.inj (by simp)
|
||||
|
||||
@[simp] theorem Int32.toInt64_mod (a b : Int32) : (a % b).toInt64 = a.toInt64 % b.toInt64 := Int64.toInt.inj (by simp)
|
||||
@[simp] theorem Int32.toISize_mod (a b : Int32) : (a % b).toISize = a.toISize % b.toISize := ISize.toInt.inj (by simp)
|
||||
|
||||
@[simp] theorem ISize.toInt64_mod (a b : ISize) : (a % b).toInt64 = a.toInt64 % b.toInt64 := Int64.toInt.inj (by simp)
|
||||
|
||||
theorem Int8.ofInt_tmod {a b : Int} (ha₁ : minValue.toInt ≤ a) (ha₂ : a ≤ maxValue.toInt)
|
||||
(hb₁ : minValue.toInt ≤ b) (hb₂ : b ≤ maxValue.toInt) : Int8.ofInt (a.tmod b) = Int8.ofInt a % Int8.ofInt b := by
|
||||
rw [Int8.ofInt_eq_iff_bmod_eq_toInt, ← toInt_bmod_size, toInt_mod, toInt_ofInt, toInt_ofInt,
|
||||
Int.bmod_eq_self_of_le (n := a), Int.bmod_eq_self_of_le (n := b)]
|
||||
· exact hb₁
|
||||
· exact Int.lt_of_le_sub_one hb₂
|
||||
· exact ha₁
|
||||
· exact Int.lt_of_le_sub_one ha₂
|
||||
theorem Int16.ofInt_tmod {a b : Int} (ha₁ : minValue.toInt ≤ a) (ha₂ : a ≤ maxValue.toInt)
|
||||
(hb₁ : minValue.toInt ≤ b) (hb₂ : b ≤ maxValue.toInt) : Int16.ofInt (a.tmod b) = Int16.ofInt a % Int16.ofInt b := by
|
||||
rw [Int16.ofInt_eq_iff_bmod_eq_toInt, ← toInt_bmod_size, toInt_mod, toInt_ofInt, toInt_ofInt,
|
||||
Int.bmod_eq_self_of_le (n := a), Int.bmod_eq_self_of_le (n := b)]
|
||||
· exact hb₁
|
||||
· exact Int.lt_of_le_sub_one hb₂
|
||||
· exact ha₁
|
||||
· exact Int.lt_of_le_sub_one ha₂
|
||||
theorem Int32.ofInt_tmod {a b : Int} (ha₁ : minValue.toInt ≤ a) (ha₂ : a ≤ maxValue.toInt)
|
||||
(hb₁ : minValue.toInt ≤ b) (hb₂ : b ≤ maxValue.toInt) : Int32.ofInt (a.tmod b) = Int32.ofInt a % Int32.ofInt b := by
|
||||
rw [Int32.ofInt_eq_iff_bmod_eq_toInt, ← toInt_bmod_size, toInt_mod, toInt_ofInt, toInt_ofInt,
|
||||
Int.bmod_eq_self_of_le (n := a), Int.bmod_eq_self_of_le (n := b)]
|
||||
· exact hb₁
|
||||
· exact Int.lt_of_le_sub_one hb₂
|
||||
· exact ha₁
|
||||
· exact Int.lt_of_le_sub_one ha₂
|
||||
theorem Int64.ofInt_tmod {a b : Int} (ha₁ : minValue.toInt ≤ a) (ha₂ : a ≤ maxValue.toInt)
|
||||
(hb₁ : minValue.toInt ≤ b) (hb₂ : b ≤ maxValue.toInt) : Int64.ofInt (a.tmod b) = Int64.ofInt a % Int64.ofInt b := by
|
||||
rw [Int64.ofInt_eq_iff_bmod_eq_toInt, ← toInt_bmod_size, toInt_mod, toInt_ofInt, toInt_ofInt,
|
||||
Int.bmod_eq_self_of_le (n := a), Int.bmod_eq_self_of_le (n := b)]
|
||||
· exact hb₁
|
||||
· exact Int.lt_of_le_sub_one hb₂
|
||||
· exact ha₁
|
||||
· exact Int.lt_of_le_sub_one ha₂
|
||||
theorem ISize.ofInt_tmod {a b : Int} (ha₁ : minValue.toInt ≤ a) (ha₂ : a ≤ maxValue.toInt)
|
||||
(hb₁ : minValue.toInt ≤ b) (hb₂ : b ≤ maxValue.toInt) : ISize.ofInt (a.tmod b) = ISize.ofInt a % ISize.ofInt b := by
|
||||
rw [ISize.ofInt_eq_iff_bmod_eq_toInt, ← toInt_bmod_size, toInt_mod, toInt_ofInt, toInt_ofInt,
|
||||
Int.bmod_eq_self_of_le (n := a), Int.bmod_eq_self_of_le (n := b)]
|
||||
· exact le_of_eq_of_le (by cases System.Platform.numBits_eq <;> simp_all [size, toInt_ofInt, toInt_neg]) hb₁
|
||||
· refine Int.lt_of_le_sub_one (le_of_le_of_eq hb₂ ?_)
|
||||
cases System.Platform.numBits_eq <;> simp_all [size, toInt_ofInt]
|
||||
· exact le_of_eq_of_le (by cases System.Platform.numBits_eq <;> simp_all [size, toInt_ofInt, toInt_neg]) ha₁
|
||||
· refine Int.lt_of_le_sub_one (le_of_le_of_eq ha₂ ?_)
|
||||
cases System.Platform.numBits_eq <;> simp_all [size, toInt_ofInt]
|
||||
|
||||
theorem Int8.ofInt_eq_ofIntLE_mod {a b : Int} (ha₁ ha₂ hb₁ hb₂) :
|
||||
Int8.ofInt (a.tmod b) = Int8.ofIntLE a ha₁ ha₂ % Int8.ofIntLE b hb₁ hb₂ := by
|
||||
rw [ofIntLE_eq_ofInt, ofIntLE_eq_ofInt, ofInt_tmod ha₁ ha₂ hb₁ hb₂]
|
||||
theorem Int16.ofInt_eq_ofIntLE_mod {a b : Int} (ha₁ ha₂ hb₁ hb₂) :
|
||||
Int16.ofInt (a.tmod b) = Int16.ofIntLE a ha₁ ha₂ % Int16.ofIntLE b hb₁ hb₂ := by
|
||||
rw [ofIntLE_eq_ofInt, ofIntLE_eq_ofInt, ofInt_tmod ha₁ ha₂ hb₁ hb₂]
|
||||
theorem Int32.ofInt_eq_ofIntLE_mod {a b : Int} (ha₁ ha₂ hb₁ hb₂) :
|
||||
Int32.ofInt (a.tmod b) = Int32.ofIntLE a ha₁ ha₂ % Int32.ofIntLE b hb₁ hb₂ := by
|
||||
rw [ofIntLE_eq_ofInt, ofIntLE_eq_ofInt, ofInt_tmod ha₁ ha₂ hb₁ hb₂]
|
||||
theorem Int64.ofInt_eq_ofIntLE_mod {a b : Int} (ha₁ ha₂ hb₁ hb₂) :
|
||||
Int64.ofInt (a.tmod b) = Int64.ofIntLE a ha₁ ha₂ % Int64.ofIntLE b hb₁ hb₂ := by
|
||||
rw [ofIntLE_eq_ofInt, ofIntLE_eq_ofInt, ofInt_tmod ha₁ ha₂ hb₁ hb₂]
|
||||
theorem ISize.ofInt_eq_ofIntLE_mod {a b : Int} (ha₁ ha₂ hb₁ hb₂) :
|
||||
ISize.ofInt (a.tmod b) = ISize.ofIntLE a ha₁ ha₂ % ISize.ofIntLE b hb₁ hb₂ := by
|
||||
rw [ofIntLE_eq_ofInt, ofIntLE_eq_ofInt, ofInt_tmod ha₁ ha₂ hb₁ hb₂]
|
||||
|
||||
theorem Int8.ofNat_mod {a b : Nat} (ha : a < 2 ^ 7) (hb : b < 2 ^ 7) :
|
||||
Int8.ofNat (a % b) = Int8.ofNat a % Int8.ofNat b := by
|
||||
rw [← ofInt_eq_ofNat, ← ofInt_eq_ofNat, ← ofInt_eq_ofNat, Int.ofNat_tmod,
|
||||
ofInt_tmod (by simp) _ (by simp)]
|
||||
· exact Int.le_of_lt_add_one (Int.ofNat_le.2 hb)
|
||||
· exact Int.le_of_lt_add_one (Int.ofNat_le.2 ha)
|
||||
theorem Int16.ofNat_mod {a b : Nat} (ha : a < 2 ^ 15) (hb : b < 2 ^ 15) :
|
||||
Int16.ofNat (a % b) = Int16.ofNat a % Int16.ofNat b := by
|
||||
rw [← ofInt_eq_ofNat, ← ofInt_eq_ofNat, ← ofInt_eq_ofNat, Int.ofNat_tmod,
|
||||
ofInt_tmod (by simp) _ (by simp)]
|
||||
· exact Int.le_of_lt_add_one (Int.ofNat_le.2 hb)
|
||||
· exact Int.le_of_lt_add_one (Int.ofNat_le.2 ha)
|
||||
theorem Int32.ofNat_mod {a b : Nat} (ha : a < 2 ^ 31) (hb : b < 2 ^ 31) :
|
||||
Int32.ofNat (a % b) = Int32.ofNat a % Int32.ofNat b := by
|
||||
rw [← ofInt_eq_ofNat, ← ofInt_eq_ofNat, ← ofInt_eq_ofNat, Int.ofNat_tmod,
|
||||
ofInt_tmod (by simp) _ (by simp)]
|
||||
· exact Int.le_of_lt_add_one (Int.ofNat_le.2 hb)
|
||||
· exact Int.le_of_lt_add_one (Int.ofNat_le.2 ha)
|
||||
theorem Int64.ofNat_mod {a b : Nat} (ha : a < 2 ^ 63) (hb : b < 2 ^ 63) :
|
||||
Int64.ofNat (a % b) = Int64.ofNat a % Int64.ofNat b := by
|
||||
rw [← ofInt_eq_ofNat, ← ofInt_eq_ofNat, ← ofInt_eq_ofNat, Int.ofNat_tmod,
|
||||
ofInt_tmod (by simp) _ (by simp)]
|
||||
· exact Int.le_of_lt_add_one (Int.ofNat_le.2 hb)
|
||||
· exact Int.le_of_lt_add_one (Int.ofNat_le.2 ha)
|
||||
theorem ISize.ofNat_mod {a b : Nat} (ha : a < 2 ^ (System.Platform.numBits - 1)) (hb : b < 2 ^ (System.Platform.numBits - 1)) :
|
||||
ISize.ofNat (a % b) = ISize.ofNat a % ISize.ofNat b := by
|
||||
rw [← ofInt_eq_ofNat, ← ofInt_eq_ofNat, ← ofInt_eq_ofNat, Int.ofNat_tmod, ofInt_tmod]
|
||||
· exact Int.le_of_lt (Int.lt_of_lt_of_le ISize.toInt_minValue_lt_zero (Int.ofNat_zero_le _))
|
||||
· apply Int.le_of_lt_add_one
|
||||
simpa only [toInt_maxValue_add_one, ← Int.ofNat_lt, Int.natCast_pow] using ha
|
||||
· exact Int.le_of_lt (Int.lt_of_lt_of_le ISize.toInt_minValue_lt_zero (Int.ofNat_zero_le _))
|
||||
· apply Int.le_of_lt_add_one
|
||||
simpa only [toInt_maxValue_add_one, ← Int.ofNat_lt, Int.natCast_pow] using hb
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue