Skip to content

Commit 1bf2d8e

Browse files
TwoFXTwoFX
authored
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.
1 parent 5348ce9 commit 1bf2d8e

File tree

1 file changed

+118
-0
lines changed

1 file changed

+118
-0
lines changed

‎src/Init/Data/SInt/Lemmas.lean

+118
Original file line numberDiff line numberDiff line change
@@ -3271,3 +3271,121 @@ protected theorem Int64.ne_of_lt {a b : Int64} : a < b → a ≠ b := by
32713271
simpa [Int64.lt_iff_toInt_lt, ← Int64.toInt_inj] using Int.ne_of_lt
32723272
protected theorem ISize.ne_of_lt {a b : ISize} : a < b → a ≠ b := by
32733273
simpa [ISize.lt_iff_toInt_lt, ← ISize.toInt_inj] using Int.ne_of_lt
3274+
3275+
@[simp] theorem Int8.toInt_mod (a b : Int8) : (a % b).toInt = a.toInt.tmod b.toInt := by
3276+
rw [← toInt_toBitVec, Int8.toBitVec_mod, BitVec.toInt_srem, toInt_toBitVec, toInt_toBitVec]
3277+
@[simp] theorem Int16.toInt_mod (a b : Int16) : (a % b).toInt = a.toInt.tmod b.toInt := by
3278+
rw [← toInt_toBitVec, Int16.toBitVec_mod, BitVec.toInt_srem, toInt_toBitVec, toInt_toBitVec]
3279+
@[simp] theorem Int32.toInt_mod (a b : Int32) : (a % b).toInt = a.toInt.tmod b.toInt := by
3280+
rw [← toInt_toBitVec, Int32.toBitVec_mod, BitVec.toInt_srem, toInt_toBitVec, toInt_toBitVec]
3281+
@[simp] theorem Int64.toInt_mod (a b : Int64) : (a % b).toInt = a.toInt.tmod b.toInt := by
3282+
rw [← toInt_toBitVec, Int64.toBitVec_mod, BitVec.toInt_srem, toInt_toBitVec, toInt_toBitVec]
3283+
@[simp] theorem ISize.toInt_mod (a b : ISize) : (a % b).toInt = a.toInt.tmod b.toInt := by
3284+
rw [← toInt_toBitVec, ISize.toBitVec_mod, BitVec.toInt_srem, toInt_toBitVec, toInt_toBitVec]
3285+
3286+
@[simp] theorem Int8.toInt16_mod (a b : Int8) : (a % b).toInt16 = a.toInt16 % b.toInt16 := Int16.toInt.inj (by simp)
3287+
@[simp] theorem Int8.toInt32_mod (a b : Int8) : (a % b).toInt32 = a.toInt32 % b.toInt32 := Int32.toInt.inj (by simp)
3288+
@[simp] theorem Int8.toInt64_mod (a b : Int8) : (a % b).toInt64 = a.toInt64 % b.toInt64 := Int64.toInt.inj (by simp)
3289+
@[simp] theorem Int8.toISize_mod (a b : Int8) : (a % b).toISize = a.toISize % b.toISize := ISize.toInt.inj (by simp)
3290+
3291+
@[simp] theorem Int16.toInt32_mod (a b : Int16) : (a % b).toInt32 = a.toInt32 % b.toInt32 := Int32.toInt.inj (by simp)
3292+
@[simp] theorem Int16.toInt64_mod (a b : Int16) : (a % b).toInt64 = a.toInt64 % b.toInt64 := Int64.toInt.inj (by simp)
3293+
@[simp] theorem Int16.toISize_mod (a b : Int16) : (a % b).toISize = a.toISize % b.toISize := ISize.toInt.inj (by simp)
3294+
3295+
@[simp] theorem Int32.toInt64_mod (a b : Int32) : (a % b).toInt64 = a.toInt64 % b.toInt64 := Int64.toInt.inj (by simp)
3296+
@[simp] theorem Int32.toISize_mod (a b : Int32) : (a % b).toISize = a.toISize % b.toISize := ISize.toInt.inj (by simp)
3297+
3298+
@[simp] theorem ISize.toInt64_mod (a b : ISize) : (a % b).toInt64 = a.toInt64 % b.toInt64 := Int64.toInt.inj (by simp)
3299+
3300+
theorem Int8.ofInt_tmod {a b : Int} (ha₁ : minValue.toInt ≤ a) (ha₂ : a ≤ maxValue.toInt)
3301+
(hb₁ : minValue.toInt ≤ b) (hb₂ : b ≤ maxValue.toInt) : Int8.ofInt (a.tmod b) = Int8.ofInt a % Int8.ofInt b := by
3302+
rw [Int8.ofInt_eq_iff_bmod_eq_toInt, ← toInt_bmod_size, toInt_mod, toInt_ofInt, toInt_ofInt,
3303+
Int.bmod_eq_self_of_le (n := a), Int.bmod_eq_self_of_le (n := b)]
3304+
· exact hb₁
3305+
· exact Int.lt_of_le_sub_one hb₂
3306+
· exact ha₁
3307+
· exact Int.lt_of_le_sub_one ha₂
3308+
theorem Int16.ofInt_tmod {a b : Int} (ha₁ : minValue.toInt ≤ a) (ha₂ : a ≤ maxValue.toInt)
3309+
(hb₁ : minValue.toInt ≤ b) (hb₂ : b ≤ maxValue.toInt) : Int16.ofInt (a.tmod b) = Int16.ofInt a % Int16.ofInt b := by
3310+
rw [Int16.ofInt_eq_iff_bmod_eq_toInt, ← toInt_bmod_size, toInt_mod, toInt_ofInt, toInt_ofInt,
3311+
Int.bmod_eq_self_of_le (n := a), Int.bmod_eq_self_of_le (n := b)]
3312+
· exact hb₁
3313+
· exact Int.lt_of_le_sub_one hb₂
3314+
· exact ha₁
3315+
· exact Int.lt_of_le_sub_one ha₂
3316+
theorem Int32.ofInt_tmod {a b : Int} (ha₁ : minValue.toInt ≤ a) (ha₂ : a ≤ maxValue.toInt)
3317+
(hb₁ : minValue.toInt ≤ b) (hb₂ : b ≤ maxValue.toInt) : Int32.ofInt (a.tmod b) = Int32.ofInt a % Int32.ofInt b := by
3318+
rw [Int32.ofInt_eq_iff_bmod_eq_toInt, ← toInt_bmod_size, toInt_mod, toInt_ofInt, toInt_ofInt,
3319+
Int.bmod_eq_self_of_le (n := a), Int.bmod_eq_self_of_le (n := b)]
3320+
· exact hb₁
3321+
· exact Int.lt_of_le_sub_one hb₂
3322+
· exact ha₁
3323+
· exact Int.lt_of_le_sub_one ha₂
3324+
theorem Int64.ofInt_tmod {a b : Int} (ha₁ : minValue.toInt ≤ a) (ha₂ : a ≤ maxValue.toInt)
3325+
(hb₁ : minValue.toInt ≤ b) (hb₂ : b ≤ maxValue.toInt) : Int64.ofInt (a.tmod b) = Int64.ofInt a % Int64.ofInt b := by
3326+
rw [Int64.ofInt_eq_iff_bmod_eq_toInt, ← toInt_bmod_size, toInt_mod, toInt_ofInt, toInt_ofInt,
3327+
Int.bmod_eq_self_of_le (n := a), Int.bmod_eq_self_of_le (n := b)]
3328+
· exact hb₁
3329+
· exact Int.lt_of_le_sub_one hb₂
3330+
· exact ha₁
3331+
· exact Int.lt_of_le_sub_one ha₂
3332+
theorem ISize.ofInt_tmod {a b : Int} (ha₁ : minValue.toInt ≤ a) (ha₂ : a ≤ maxValue.toInt)
3333+
(hb₁ : minValue.toInt ≤ b) (hb₂ : b ≤ maxValue.toInt) : ISize.ofInt (a.tmod b) = ISize.ofInt a % ISize.ofInt b := by
3334+
rw [ISize.ofInt_eq_iff_bmod_eq_toInt, ← toInt_bmod_size, toInt_mod, toInt_ofInt, toInt_ofInt,
3335+
Int.bmod_eq_self_of_le (n := a), Int.bmod_eq_self_of_le (n := b)]
3336+
· exact le_of_eq_of_le (by cases System.Platform.numBits_eq <;> simp_all [size, toInt_ofInt, toInt_neg]) hb₁
3337+
· refine Int.lt_of_le_sub_one (le_of_le_of_eq hb₂ ?_)
3338+
cases System.Platform.numBits_eq <;> simp_all [size, toInt_ofInt]
3339+
· exact le_of_eq_of_le (by cases System.Platform.numBits_eq <;> simp_all [size, toInt_ofInt, toInt_neg]) ha₁
3340+
· refine Int.lt_of_le_sub_one (le_of_le_of_eq ha₂ ?_)
3341+
cases System.Platform.numBits_eq <;> simp_all [size, toInt_ofInt]
3342+
3343+
theorem Int8.ofInt_eq_ofIntLE_mod {a b : Int} (ha₁ ha₂ hb₁ hb₂) :
3344+
Int8.ofInt (a.tmod b) = Int8.ofIntLE a ha₁ ha₂ % Int8.ofIntLE b hb₁ hb₂ := by
3345+
rw [ofIntLE_eq_ofInt, ofIntLE_eq_ofInt, ofInt_tmod ha₁ ha₂ hb₁ hb₂]
3346+
theorem Int16.ofInt_eq_ofIntLE_mod {a b : Int} (ha₁ ha₂ hb₁ hb₂) :
3347+
Int16.ofInt (a.tmod b) = Int16.ofIntLE a ha₁ ha₂ % Int16.ofIntLE b hb₁ hb₂ := by
3348+
rw [ofIntLE_eq_ofInt, ofIntLE_eq_ofInt, ofInt_tmod ha₁ ha₂ hb₁ hb₂]
3349+
theorem Int32.ofInt_eq_ofIntLE_mod {a b : Int} (ha₁ ha₂ hb₁ hb₂) :
3350+
Int32.ofInt (a.tmod b) = Int32.ofIntLE a ha₁ ha₂ % Int32.ofIntLE b hb₁ hb₂ := by
3351+
rw [ofIntLE_eq_ofInt, ofIntLE_eq_ofInt, ofInt_tmod ha₁ ha₂ hb₁ hb₂]
3352+
theorem Int64.ofInt_eq_ofIntLE_mod {a b : Int} (ha₁ ha₂ hb₁ hb₂) :
3353+
Int64.ofInt (a.tmod b) = Int64.ofIntLE a ha₁ ha₂ % Int64.ofIntLE b hb₁ hb₂ := by
3354+
rw [ofIntLE_eq_ofInt, ofIntLE_eq_ofInt, ofInt_tmod ha₁ ha₂ hb₁ hb₂]
3355+
theorem ISize.ofInt_eq_ofIntLE_mod {a b : Int} (ha₁ ha₂ hb₁ hb₂) :
3356+
ISize.ofInt (a.tmod b) = ISize.ofIntLE a ha₁ ha₂ % ISize.ofIntLE b hb₁ hb₂ := by
3357+
rw [ofIntLE_eq_ofInt, ofIntLE_eq_ofInt, ofInt_tmod ha₁ ha₂ hb₁ hb₂]
3358+
3359+
theorem Int8.ofNat_mod {a b : Nat} (ha : a < 2 ^ 7) (hb : b < 2 ^ 7) :
3360+
Int8.ofNat (a % b) = Int8.ofNat a % Int8.ofNat b := by
3361+
rw [← ofInt_eq_ofNat, ← ofInt_eq_ofNat, ← ofInt_eq_ofNat, Int.ofNat_tmod,
3362+
ofInt_tmod (by simp) _ (by simp)]
3363+
· exact Int.le_of_lt_add_one (Int.ofNat_le.2 hb)
3364+
· exact Int.le_of_lt_add_one (Int.ofNat_le.2 ha)
3365+
theorem Int16.ofNat_mod {a b : Nat} (ha : a < 2 ^ 15) (hb : b < 2 ^ 15) :
3366+
Int16.ofNat (a % b) = Int16.ofNat a % Int16.ofNat b := by
3367+
rw [← ofInt_eq_ofNat, ← ofInt_eq_ofNat, ← ofInt_eq_ofNat, Int.ofNat_tmod,
3368+
ofInt_tmod (by simp) _ (by simp)]
3369+
· exact Int.le_of_lt_add_one (Int.ofNat_le.2 hb)
3370+
· exact Int.le_of_lt_add_one (Int.ofNat_le.2 ha)
3371+
theorem Int32.ofNat_mod {a b : Nat} (ha : a < 2 ^ 31) (hb : b < 2 ^ 31) :
3372+
Int32.ofNat (a % b) = Int32.ofNat a % Int32.ofNat b := by
3373+
rw [← ofInt_eq_ofNat, ← ofInt_eq_ofNat, ← ofInt_eq_ofNat, Int.ofNat_tmod,
3374+
ofInt_tmod (by simp) _ (by simp)]
3375+
· exact Int.le_of_lt_add_one (Int.ofNat_le.2 hb)
3376+
· exact Int.le_of_lt_add_one (Int.ofNat_le.2 ha)
3377+
theorem Int64.ofNat_mod {a b : Nat} (ha : a < 2 ^ 63) (hb : b < 2 ^ 63) :
3378+
Int64.ofNat (a % b) = Int64.ofNat a % Int64.ofNat b := by
3379+
rw [← ofInt_eq_ofNat, ← ofInt_eq_ofNat, ← ofInt_eq_ofNat, Int.ofNat_tmod,
3380+
ofInt_tmod (by simp) _ (by simp)]
3381+
· exact Int.le_of_lt_add_one (Int.ofNat_le.2 hb)
3382+
· exact Int.le_of_lt_add_one (Int.ofNat_le.2 ha)
3383+
theorem ISize.ofNat_mod {a b : Nat} (ha : a < 2 ^ (System.Platform.numBits - 1)) (hb : b < 2 ^ (System.Platform.numBits - 1)) :
3384+
ISize.ofNat (a % b) = ISize.ofNat a % ISize.ofNat b := by
3385+
rw [← ofInt_eq_ofNat, ← ofInt_eq_ofNat, ← ofInt_eq_ofNat, Int.ofNat_tmod, ofInt_tmod]
3386+
· exact Int.le_of_lt (Int.lt_of_lt_of_le ISize.toInt_minValue_lt_zero (Int.ofNat_zero_le _))
3387+
· apply Int.le_of_lt_add_one
3388+
simpa only [toInt_maxValue_add_one, ← Int.ofNat_lt, Int.natCast_pow] using ha
3389+
· exact Int.le_of_lt (Int.lt_of_lt_of_le ISize.toInt_minValue_lt_zero (Int.ofNat_zero_le _))
3390+
· apply Int.le_of_lt_add_one
3391+
simpa only [toInt_maxValue_add_one, ← Int.ofNat_lt, Int.natCast_pow] using hb

0 commit comments

Comments
 (0)