From a2695ab452057661bcdbc0fd6ab4f64cdd43e5ed Mon Sep 17 00:00:00 2001 From: luisacicolini Date: Tue, 4 Feb 2025 12:08:59 +0000 Subject: [PATCH 01/19] chore: first cleaning pass --- src/Init/Data/BitVec/Basic.lean | 12 ++ src/Init/Data/BitVec/Bitblast.lean | 157 ++++++++++++++++++ src/Init/Data/BitVec/Lemmas.lean | 16 ++ src/Std/Tactic/BVDecide/Normalize/BitVec.lean | 4 + 4 files changed, 189 insertions(+) diff --git a/src/Init/Data/BitVec/Basic.lean b/src/Init/Data/BitVec/Basic.lean index 451482e76711..cc92bd77143f 100644 --- a/src/Init/Data/BitVec/Basic.lean +++ b/src/Init/Data/BitVec/Basic.lean @@ -682,4 +682,16 @@ def reverse : {w : Nat} → BitVec w → BitVec w | 0, x => x | w + 1, x => concat (reverse (x.truncate w)) (x.msb) +/-- Overflow predicate for unsigned multiplication modulo 2^w. + SMT-Lib name: `bvumulo`. +-/ + +def umulOverflow {w : Nat} (x y : BitVec w) : Bool := x.toNat * y.toNat ≥ 2 ^ w + +/-- Overflow predicate for signed multiplication on w-bit 2's complement. + SMT-Lib name: `bvsmulo`. +-/ + +def smulOverflow {w : Nat} (x y : BitVec w) : Bool := (x.toInt * y.toInt ≥ 2 ^ (w - 1)) || (x.toInt * y.toInt < - 2 ^ (w - 1)) + end BitVec diff --git a/src/Init/Data/BitVec/Bitblast.lean b/src/Init/Data/BitVec/Bitblast.lean index 003d35aa2ca3..88918e7c38f0 100644 --- a/src/Init/Data/BitVec/Bitblast.lean +++ b/src/Init/Data/BitVec/Bitblast.lean @@ -1230,4 +1230,161 @@ theorem shiftRight_eq_ushiftRightRec (x : BitVec w₁) (y : BitVec w₂) : · simp [of_length_zero] · simp [ushiftRightRec_eq] +/-- ### Overflow +-/ + +theorem Int.emod_eq_add_self_emod {a b : Int} : a % b = (a + b) % b := + Int.add_emod_self.symm + +theorem bmod_eq_iff_of_lt_of_lt {x : Int} {y : Nat} (hge : -y ≤ x * 2) (hlt : x * 2 < y) : + x.bmod y = x := by + simp only [Int.bmod_def] + by_cases 0 ≤ x + · rw [Int.emod_eq_of_lt (by omega) (by omega)]; omega + · rw [Int.emod_eq_add_self_emod, Int.emod_eq_of_lt (by omega) (by omega)]; omega + +theorem toInt_twoPow {w i : Nat} : + (BitVec.twoPow w i).toInt = if w ≤ i then (0 : Int) else (if i + 1 = w then -(1 <<< i:Int) else (1 <<< i)) := by + simp only [BitVec.twoPow, BitVec.toInt] + rcases w with _|w' + · simp + · by_cases h : w' + 1 ≤ i + · simp [h]; norm_cast; omega + · simp only [toNat_shiftLeft, toNat_ofNat, zero_lt_succ, one_mod_two_pow, Int.ofNat_emod, h, + ↓reduceIte, Nat.add_right_cancel_iff] + have hy : (2 ^ i % 2 ^ (w' + 1)) = 2 ^ i := by rw [Nat.mod_eq_of_lt (by rw [Nat.pow_lt_pow_iff_right (by omega)]; omega)] + have hj : 2 * 2 ^ i = 2 ^ (i + 1) := by rw [Nat.pow_add, Nat.mul_comm] + norm_cast + simp only [Nat.shiftLeft_eq, Nat.one_mul, hy, hj] + by_cases i + 1 = (w' + 1) + · simp only [show i = w' by omega, Nat.lt_irrefl, ↓reduceIte]; omega + · have sl : 2 ^ (i + 1) < 2 ^ (w' + 1) := by + rw [Nat.pow_lt_pow_iff_right (by omega)] + omega + simp only [sl, ↓reduceIte] + omega + +theorem mul_le_mul_neg {a b c d : Int} + (hac : a ≤ c) (hbd : d ≤ b) (hb : 0 ≤ b) (hc : c ≤ 0) : a * b ≤ c * d := + Int.le_trans (Int.mul_le_mul_of_nonneg_right hac hb) (Int.mul_le_mul_of_nonpos_left hc hbd) + +theorem Int.mul_le_mul_self {x y : Int} {s : Nat} (lbx : -s ≤ x) (ubx : x < s) (lby : -s ≤ y) (uby : y < s) : + x * y ≤ s * s := by + have := Nat.mul_pos (n := s) (m := s) (by omega) (by omega) + by_cases hx : 0 < x <;> by_cases hy : 0 < y + · exact Int.mul_le_mul (by omega) (by omega) (by omega) (by omega) + · have : x * y ≤ 0 := Int.mul_nonpos_of_nonneg_of_nonpos (by omega) (by omega); omega + · rw [Int.mul_comm] + have : y * x ≤ 0 := Int.mul_nonpos_of_nonneg_of_nonpos (by omega) (by omega); omega + · have : -x * -y ≤ s * s := Int.mul_le_mul (by omega) (by omega) (by omega) (by omega) + simp_all + +theorem toInt_mul_toInt_lt {x y : BitVec w} : x.toInt * y.toInt ≤ 2 ^ (w * 2 - 2) := by + have xlt := toInt_lt (x := x); have xle := le_toInt (x := x) + have ylt := toInt_lt (x := y); have yle := le_toInt (x := y) + have h : 2 ^ (w * 2 - 2) = 2 ^ (w - 1) * 2 ^ (w - 1) := by + rw [← Nat.pow_add, ←Nat.mul_two, Nat.mul_comm (m := 2) (n := (w - 1)), Nat.mul_sub_one, Nat.mul_comm] + rw_mod_cast [h] + exact Int.mul_le_mul_self xle xlt yle ylt + +theorem Int.neg_mul_self_le_mul {x y : Int} {s : Nat} (lbx : -s ≤ x) (ubx : x < s) (lby : -s ≤ y) (uby : y < s) : + -(s * s) ≤ x * y := by + have := Nat.mul_pos (n := s) (m := s) (by omega) (by omega) + by_cases 0 ≤ x <;> by_cases 0 ≤ y + · have : 0 ≤ x * y := Int.mul_nonneg (by omega) (by omega); omega + · rw [← Int.neg_mul, Int.mul_comm (a := x)]; exact mul_le_mul_neg (by omega) (by omega) (by omega) (by omega) + · rw [← Int.neg_mul]; exact mul_le_mul_neg (by omega) (by omega) (by omega) (by omega) + · have : 0 < x * y := Int.mul_pos_of_neg_of_neg (by omega) (by omega) ;omega + +theorem le_toInt_mul_toInt {x y : BitVec w} : -(2 ^ (w * 2 - 2)) ≤ x.toInt * y.toInt := by + have xlt := toInt_lt (x := x); have xle := le_toInt (x := x) + have ylt := toInt_lt (x := y); have yle := le_toInt (x := y) + have h : 2 ^ (w * 2 - 2) = 2 ^ (w - 1) * 2 ^ (w - 1) := by + rw [← Nat.pow_add, ←Nat.mul_two, Nat.mul_comm (m := 2) (n := (w - 1)), Nat.mul_sub_one, Nat.mul_comm] + rw_mod_cast [h] + exact Int.neg_mul_self_le_mul xle xlt yle ylt + +theorem toInt_twoPow_of_eq {w i : Nat} (h : i + 1 = w) : + (BitVec.twoPow w i).toInt = -(2 ^ i) := by + simp only [toInt_twoPow, show ¬(w ≤ i) by omega, ↓reduceIte, h, Nat.shiftLeft_eq, Nat.one_mul] + norm_cast + +@[simp] +theorem toInt_one {w : Nat} (h : 1 < w ) : (1#w).toInt = 1 := by + have : 1 < 2 ^ w := Nat.one_lt_two_pow (by omega) + unfold BitVec.toInt + simp only [BitVec.toNat_ofNat, Int.ofNat_emod] + rw [Nat.mod_eq_of_lt (by omega)] + by_cases hw' : 2 * 1 < 2 ^ w + · simp only [Nat.mul_one, hw', ↓reduceIte, Int.Nat.cast_ofNat_Int] + norm_cast + rw [Nat.mod_eq_of_lt (by omega)] + · simp only [Int.not_lt] at hw' + have h2 : 2 * 1 = 2 ^ 1 := by rw [Nat.mul_one, Nat.pow_one] + rw [h2, Nat.pow_lt_pow_iff_right (a := 2) (by omega)] at hw' + omega + +@[simp] +theorem toInt_twoPow_sub_one : (BitVec.twoPow w (w - 1) - 1#w).toInt = 2 ^ (w - 1) - 1 := by + rcases w with _|_|w + · decide + · decide + · have : 1 < 2 ^ (w + 1 + 1) := Nat.one_lt_two_pow (by omega) + rw_mod_cast [BitVec.twoPow, BitVec.toInt_sub, BitVec.toInt_shiftLeft, BitVec.toNat_ofNat, + Int.bmod_sub_bmod_congr, toInt_one (by omega), Nat.shiftLeft_eq, + Nat.mod_eq_of_lt (by omega), bmod_eq_iff_of_lt_of_lt] + simp only [Nat.add_one_sub_one, Nat.one_mul] + · have : 0 < (2 ^ (w + 1 + 1 - 1) - 1) * 2 := by simp; omega + norm_cast + omega + · rw [← Nat.two_pow_pred_add_two_pow_pred (w := w + 1 + 1) (by omega)] + omega + +theorem toNat_mul_toNat_lt {x y : BitVec w} : x.toNat * y.toNat < 2 ^ (w * 2) := by + have := BitVec.isLt x; have := BitVec.isLt y + simp only [Nat.mul_two, Nat.pow_add] + exact Nat.mul_lt_mul_of_le_of_lt (by omega) (by omega) (by omega) + +-- from mathlib +theorem Nat.mul_mod_mod (a b c : Nat) : (a * (b % c)) % c = a * b % c := by + rw [mul_mod, mod_mod, ← mul_mod] + +theorem umulOverflow_eq {w : Nat} (x y : BitVec w) : + umulOverflow x y = + (0 < w && BitVec.twoPow (w * 2) w ≤ x.zeroExtend (w * 2) * y.zeroExtend (w * 2)) := by + simp only [umulOverflow, ge_iff_le, truncate_eq_setWidth, le_def, toNat_twoPow, toNat_mul, + toNat_setWidth, Nat.mul_mod_mod, mod_mul_mod] + rcases w with _|w' + · decide +revert + · simp only [show 0 < w' + 1 by omega, decide_true, Bool.true_and, decide_eq_decide] + rw [Nat.mod_eq_of_lt toNat_mul_toNat_lt, Nat.mod_eq_of_lt] + have := Nat.pow_lt_pow_of_lt (a := 2) (n := (w' + 1)) (m := (w' + 1) * 2) + omega + +theorem Int.pow_lt_pow {a : Int} {b c : Nat} (ha : (1 : Nat) < a) (hbc : b < c): + a ^ b < a ^ c := by + rw [← Int.toNat_of_nonneg (a := a) (by omega), ← Int.natCast_pow, ← Int.natCast_pow] + have := Nat.pow_lt_pow_of_lt (a := a.toNat) (m := c) (n := b) + simp only [Int.ofNat_lt] + omega + +theorem smulOverflow_eq {w : Nat} (x y : BitVec w) : + smulOverflow x y + = (w ≠ 0) || (((BitVec.intMin w).signExtend (w * 2)).sle (x.signExtend (w * 2) * y.signExtend (w * 2)) && + (x.signExtend (w * 2) * y.signExtend (w * 2)).sle ((BitVec.intMax w).signExtend (w * 2))) := by + simp only [smulOverflow] + rcases w with _|w + · decide +revert + · simp only [Bool.false_or, BitVec.intMin, BitVec.intMax, BitVec.sle, BitVec.toInt_mul, + decide_eq_true_eq, BitVec.ofNat_eq_ofNat] + have := Int.pow_lt_pow (a := 2) (b := ((w + 1) * 2 - 2)) (c := ((w + 1) * 2 - 1)) + have := @le_toInt_mul_toInt (w + 1) x y + have hlb : -((2 ^ ((w + 1) * 2 - 1) : Nat) * 2) ≤ x.toInt * y.toInt * 2 := by push_cast; omega + have := @toInt_mul_toInt_lt (w + 1) x y + have hub : x.toInt * y.toInt * 2 < ((2 ^ ((w + 1) * 2 - 1): Nat) * 2) := Int.mul_lt_mul_of_pos_right (by norm_cast at *; omega) (by omega) + rw [BitVec.toInt_signExtend_of_lt (by omega), BitVec.toInt_signExtend_of_lt (by omega), + BitVec.toInt_signExtend_of_lt (by omega), BitVec.toInt_signExtend_of_lt (by omega), toInt_twoPow_of_eq (by omega), ←Nat.two_pow_pred_add_two_pow_pred (by omega)] + simp only [← Nat.mul_two, bmod_eq_iff_of_lt_of_lt hlb hub, toInt_twoPow_sub_one, or_eq_true, decide_eq_true_eq, _root_.eq_iff_iff, and_eq_true] + omega + end BitVec diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean index 74a23069fdaa..fda94d9320d6 100644 --- a/src/Init/Data/BitVec/Lemmas.lean +++ b/src/Init/Data/BitVec/Lemmas.lean @@ -4168,6 +4168,22 @@ instance instDecidableExistsBitVec : | 0, _, _ => inferInstance | _ + 1, _, _ => inferInstance +theorem toInt_lt {w : Nat} {x : BitVec w} : x.toInt < 2 ^ (w - 1) := by + simp only [BitVec.toInt] + rcases w with _|w' + · omega + · rw [← Nat.two_pow_pred_add_two_pow_pred (by omega), ← Nat.two_mul, Nat.add_sub_cancel] + simp only [Nat.zero_lt_succ, Nat.mul_lt_mul_left, Int.natCast_mul, Int.Nat.cast_ofNat_Int] + norm_cast; omega + +theorem le_toInt {w : Nat} {x : BitVec w} : -2 ^ (w - 1) ≤ x.toInt := by + simp only [BitVec.toInt] + rcases w with _|w' + · omega + · rw [← Nat.two_pow_pred_add_two_pow_pred (by omega), ← Nat.two_mul, Nat.add_sub_cancel] + simp only [Nat.zero_lt_succ, Nat.mul_lt_mul_left, Int.natCast_mul, Int.Nat.cast_ofNat_Int] + norm_cast; omega + /-! ### Deprecations -/ set_option linter.missingDocs false diff --git a/src/Std/Tactic/BVDecide/Normalize/BitVec.lean b/src/Std/Tactic/BVDecide/Normalize/BitVec.lean index 34738b27a52a..1c57deab81c3 100644 --- a/src/Std/Tactic/BVDecide/Normalize/BitVec.lean +++ b/src/Std/Tactic/BVDecide/Normalize/BitVec.lean @@ -330,6 +330,10 @@ attribute [bv_normalize] BitVec.umod_zero attribute [bv_normalize] BitVec.umod_one attribute [bv_normalize] BitVec.umod_eq_and +attribute [bv_normalize] BitVec.umulOverflow_eq +attribute [bv_normalize] BitVec.smulOverflow_eq + + /-- `x / (BitVec.ofNat n)` where `n = 2^k` is the same as shifting `x` right by `k`. -/ theorem BitVec.udiv_ofNat_eq_of_lt (w : Nat) (x : BitVec w) (n : Nat) (k : Nat) (hk : 2 ^ k = n) (hlt : k < w) : x / (BitVec.ofNat w n) = x >>> k := by From 540349d567e58395b918b0aa65ca39d126d8ce42 Mon Sep 17 00:00:00 2001 From: luisacicolini Date: Tue, 4 Feb 2025 12:25:02 +0000 Subject: [PATCH 02/19] chore: useless newline --- src/Std/Tactic/BVDecide/Normalize/BitVec.lean | 1 - 1 file changed, 1 deletion(-) diff --git a/src/Std/Tactic/BVDecide/Normalize/BitVec.lean b/src/Std/Tactic/BVDecide/Normalize/BitVec.lean index 1c57deab81c3..93b6d6697e2b 100644 --- a/src/Std/Tactic/BVDecide/Normalize/BitVec.lean +++ b/src/Std/Tactic/BVDecide/Normalize/BitVec.lean @@ -333,7 +333,6 @@ attribute [bv_normalize] BitVec.umod_eq_and attribute [bv_normalize] BitVec.umulOverflow_eq attribute [bv_normalize] BitVec.smulOverflow_eq - /-- `x / (BitVec.ofNat n)` where `n = 2^k` is the same as shifting `x` right by `k`. -/ theorem BitVec.udiv_ofNat_eq_of_lt (w : Nat) (x : BitVec w) (n : Nat) (k : Nat) (hk : 2 ^ k = n) (hlt : k < w) : x / (BitVec.ofNat w n) = x >>> k := by From 5786b41d55f8a0f3ab19b8aa53fbed20a127f127 Mon Sep 17 00:00:00 2001 From: luisacicolini Date: Wed, 5 Feb 2025 11:38:34 +0000 Subject: [PATCH 03/19] chore: reorder theorems --- src/Init/Data/BitVec/Bitblast.lean | 36 +++++++++++++++--------------- 1 file changed, 18 insertions(+), 18 deletions(-) diff --git a/src/Init/Data/BitVec/Bitblast.lean b/src/Init/Data/BitVec/Bitblast.lean index 54a1b29b7e66..2c3af0a32373 100644 --- a/src/Init/Data/BitVec/Bitblast.lean +++ b/src/Init/Data/BitVec/Bitblast.lean @@ -1234,6 +1234,24 @@ theorem shiftRight_eq_ushiftRightRec (x : BitVec w₁) (y : BitVec w₂) : /-- ### Overflow -/ +/-- Unsigned addition overflows iff the final carry bit of the addition circuit is `true`. -/ +theorem uaddOverflow_eq {w : Nat} (x y : BitVec w) : + uaddOverflow x y = (x.setWidth (w + 1) + y.setWidth (w + 1)).msb := by + simp [uaddOverflow, msb_add, msb_setWidth, carry] + +theorem saddOverflow_eq {w : Nat} (x y : BitVec w) : + saddOverflow x y = (x.msb == y.msb && !((x + y).msb == x.msb)) := by + simp only [saddOverflow] + rcases w with _|w + · revert x y; decide + · have := le_toInt (x := x); have := toInt_lt (x := x) + have := le_toInt (x := y); have := toInt_lt (x := y) + simp only [← decide_or, msb_eq_toInt, decide_beq_decide, toInt_add, ← decide_not, ← decide_and, + decide_eq_decide] + rw_mod_cast [Int.bmod_neg_iff (by omega) (by omega)] + simp + omega + theorem Int.emod_eq_add_self_emod {a b : Int} : a % b = (a + b) % b := Int.add_emod_self.symm @@ -1388,24 +1406,6 @@ theorem smulOverflow_eq {w : Nat} (x y : BitVec w) : simp only [← Nat.mul_two, bmod_eq_iff_of_lt_of_lt hlb hub, toInt_twoPow_sub_one, or_eq_true, decide_eq_true_eq, _root_.eq_iff_iff, and_eq_true] omega -/-- Unsigned addition overflows iff the final carry bit of the addition circuit is `true`. -/ -theorem uaddOverflow_eq {w : Nat} (x y : BitVec w) : - uaddOverflow x y = (x.setWidth (w + 1) + y.setWidth (w + 1)).msb := by - simp [uaddOverflow, msb_add, msb_setWidth, carry] - -theorem saddOverflow_eq {w : Nat} (x y : BitVec w) : - saddOverflow x y = (x.msb == y.msb && !((x + y).msb == x.msb)) := by - simp only [saddOverflow] - rcases w with _|w - · revert x y; decide - · have := le_toInt (x := x); have := toInt_lt (x := x) - have := le_toInt (x := y); have := toInt_lt (x := y) - simp only [← decide_or, msb_eq_toInt, decide_beq_decide, toInt_add, ← decide_not, ← decide_and, - decide_eq_decide] - rw_mod_cast [Int.bmod_neg_iff (by omega) (by omega)] - simp - omega - /- ### umod -/ theorem getElem_umod {n d : BitVec w} (hi : i < w) : From 43b174e0be48259b36202daf14e572a8a346955d Mon Sep 17 00:00:00 2001 From: luisacicolini Date: Wed, 5 Feb 2025 12:42:46 +0000 Subject: [PATCH 04/19] chore: fix build --- src/Init/Data/BitVec/Bitblast.lean | 3 +-- src/Init/Data/BitVec/Lemmas.lean | 16 ---------------- 2 files changed, 1 insertion(+), 18 deletions(-) diff --git a/src/Init/Data/BitVec/Bitblast.lean b/src/Init/Data/BitVec/Bitblast.lean index 2c3af0a32373..980315fe7fb4 100644 --- a/src/Init/Data/BitVec/Bitblast.lean +++ b/src/Init/Data/BitVec/Bitblast.lean @@ -1231,8 +1231,7 @@ theorem shiftRight_eq_ushiftRightRec (x : BitVec w₁) (y : BitVec w₂) : · simp [of_length_zero] · simp [ushiftRightRec_eq] -/-- ### Overflow --/ +/-! ### Overflow -/ /-- Unsigned addition overflows iff the final carry bit of the addition circuit is `true`. -/ theorem uaddOverflow_eq {w : Nat} (x y : BitVec w) : diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean index 7093dd56a5f0..8a94958be40a 100644 --- a/src/Init/Data/BitVec/Lemmas.lean +++ b/src/Init/Data/BitVec/Lemmas.lean @@ -4212,22 +4212,6 @@ instance instDecidableExistsBitVec : | 0, _, _ => inferInstance | _ + 1, _, _ => inferInstance -theorem toInt_lt {w : Nat} {x : BitVec w} : x.toInt < 2 ^ (w - 1) := by - simp only [BitVec.toInt] - rcases w with _|w' - · omega - · rw [← Nat.two_pow_pred_add_two_pow_pred (by omega), ← Nat.two_mul, Nat.add_sub_cancel] - simp only [Nat.zero_lt_succ, Nat.mul_lt_mul_left, Int.natCast_mul, Int.Nat.cast_ofNat_Int] - norm_cast; omega - -theorem le_toInt {w : Nat} {x : BitVec w} : -2 ^ (w - 1) ≤ x.toInt := by - simp only [BitVec.toInt] - rcases w with _|w' - · omega - · rw [← Nat.two_pow_pred_add_two_pow_pred (by omega), ← Nat.two_mul, Nat.add_sub_cancel] - simp only [Nat.zero_lt_succ, Nat.mul_lt_mul_left, Int.natCast_mul, Int.Nat.cast_ofNat_Int] - norm_cast; omega - /-! ### Deprecations -/ set_option linter.missingDocs false From 741107e68ed8e325b14f806b6b88384380395dab Mon Sep 17 00:00:00 2001 From: luisacicolini Date: Wed, 5 Feb 2025 14:36:48 +0000 Subject: [PATCH 05/19] chore: giving up --- src/Init/Data/BitVec/Bitblast.lean | 28 +++++++++++++++------------- src/Init/Data/BitVec/Lemmas.lean | 1 + 2 files changed, 16 insertions(+), 13 deletions(-) diff --git a/src/Init/Data/BitVec/Bitblast.lean b/src/Init/Data/BitVec/Bitblast.lean index 980315fe7fb4..d9326621f688 100644 --- a/src/Init/Data/BitVec/Bitblast.lean +++ b/src/Init/Data/BitVec/Bitblast.lean @@ -1254,14 +1254,14 @@ theorem saddOverflow_eq {w : Nat} (x y : BitVec w) : theorem Int.emod_eq_add_self_emod {a b : Int} : a % b = (a + b) % b := Int.add_emod_self.symm -theorem bmod_eq_iff_of_lt_of_lt {x : Int} {y : Nat} (hge : -y ≤ x * 2) (hlt : x * 2 < y) : +theorem Int.bmod_eq_iff_of_lt_of_lt {x : Int} {y : Nat} (hge : -y ≤ x * 2) (hlt : x * 2 < y) : x.bmod y = x := by simp only [Int.bmod_def] by_cases 0 ≤ x · rw [Int.emod_eq_of_lt (by omega) (by omega)]; omega · rw [Int.emod_eq_add_self_emod, Int.emod_eq_of_lt (by omega) (by omega)]; omega -theorem toInt_twoPow {w i : Nat} : +theorem BitVec.toInt_twoPow {w i : Nat} : (BitVec.twoPow w i).toInt = if w ≤ i then (0 : Int) else (if i + 1 = w then -(1 <<< i:Int) else (1 <<< i)) := by simp only [BitVec.twoPow, BitVec.toInt] rcases w with _|w' @@ -1282,7 +1282,7 @@ theorem toInt_twoPow {w i : Nat} : simp only [sl, ↓reduceIte] omega -theorem mul_le_mul_neg {a b c d : Int} +theorem Int.mul_le_mul_neg {a b c d : Int} (hac : a ≤ c) (hbd : d ≤ b) (hb : 0 ≤ b) (hc : c ≤ 0) : a * b ≤ c * d := Int.le_trans (Int.mul_le_mul_of_nonneg_right hac hb) (Int.mul_le_mul_of_nonpos_left hc hbd) @@ -1298,12 +1298,14 @@ theorem Int.mul_le_mul_self {x y : Int} {s : Nat} (lbx : -s ≤ x) (ubx : x < s) simp_all theorem toInt_mul_toInt_lt {x y : BitVec w} : x.toInt * y.toInt ≤ 2 ^ (w * 2 - 2) := by - have xlt := toInt_lt (x := x); have xle := le_toInt (x := x) - have ylt := toInt_lt (x := y); have yle := le_toInt (x := y) - have h : 2 ^ (w * 2 - 2) = 2 ^ (w - 1) * 2 ^ (w - 1) := by - rw [← Nat.pow_add, ←Nat.mul_two, Nat.mul_comm (m := 2) (n := (w - 1)), Nat.mul_sub_one, Nat.mul_comm] - rw_mod_cast [h] - exact Int.mul_le_mul_self xle xlt yle ylt + rcases w with _|w' + . simp [BitVec.toInt, BitVec.toNat] + · have xle := le_toInt (x := x); have xlt := toInt_lt (x := x) + have yle := le_toInt (x := y); have ylt := toInt_lt (x := y) + have h : 2 ^ ((w' + 1) * 2 - 2) = 2 ^ ((w' + 1) - 1) * 2 ^ ((w' + 1) - 1) := by + rw [← Nat.pow_add, ←Nat.mul_two, Nat.mul_comm (m := 2) (n := ((w' + 1) - 1)), Nat.mul_sub_one, Nat.mul_comm] + rw_mod_cast [h] + sorry theorem Int.neg_mul_self_le_mul {x y : Int} {s : Nat} (lbx : -s ≤ x) (ubx : x < s) (lby : -s ≤ y) (uby : y < s) : -(s * s) ≤ x * y := by @@ -1320,11 +1322,11 @@ theorem le_toInt_mul_toInt {x y : BitVec w} : -(2 ^ (w * 2 - 2)) ≤ x.toInt * y have h : 2 ^ (w * 2 - 2) = 2 ^ (w - 1) * 2 ^ (w - 1) := by rw [← Nat.pow_add, ←Nat.mul_two, Nat.mul_comm (m := 2) (n := (w - 1)), Nat.mul_sub_one, Nat.mul_comm] rw_mod_cast [h] - exact Int.neg_mul_self_le_mul xle xlt yle ylt + sorry theorem toInt_twoPow_of_eq {w i : Nat} (h : i + 1 = w) : (BitVec.twoPow w i).toInt = -(2 ^ i) := by - simp only [toInt_twoPow, show ¬(w ≤ i) by omega, ↓reduceIte, h, Nat.shiftLeft_eq, Nat.one_mul] + simp only [BitVec.toInt_twoPow, show ¬(w ≤ i) by omega, ↓reduceIte, h, Nat.shiftLeft_eq, Nat.one_mul] norm_cast @[simp] @@ -1350,7 +1352,7 @@ theorem toInt_twoPow_sub_one : (BitVec.twoPow w (w - 1) - 1#w).toInt = 2 ^ (w - · have : 1 < 2 ^ (w + 1 + 1) := Nat.one_lt_two_pow (by omega) rw_mod_cast [BitVec.twoPow, BitVec.toInt_sub, BitVec.toInt_shiftLeft, BitVec.toNat_ofNat, Int.bmod_sub_bmod_congr, toInt_one (by omega), Nat.shiftLeft_eq, - Nat.mod_eq_of_lt (by omega), bmod_eq_iff_of_lt_of_lt] + Nat.mod_eq_of_lt (by omega), Int.bmod_eq_iff_of_lt_of_lt] simp only [Nat.add_one_sub_one, Nat.one_mul] · have : 0 < (2 ^ (w + 1 + 1 - 1) - 1) * 2 := by simp; omega norm_cast @@ -1402,7 +1404,7 @@ theorem smulOverflow_eq {w : Nat} (x y : BitVec w) : have hub : x.toInt * y.toInt * 2 < ((2 ^ ((w + 1) * 2 - 1): Nat) * 2) := Int.mul_lt_mul_of_pos_right (by norm_cast at *; omega) (by omega) rw [BitVec.toInt_signExtend_of_lt (by omega), BitVec.toInt_signExtend_of_lt (by omega), BitVec.toInt_signExtend_of_lt (by omega), BitVec.toInt_signExtend_of_lt (by omega), toInt_twoPow_of_eq (by omega), ←Nat.two_pow_pred_add_two_pow_pred (by omega)] - simp only [← Nat.mul_two, bmod_eq_iff_of_lt_of_lt hlb hub, toInt_twoPow_sub_one, or_eq_true, decide_eq_true_eq, _root_.eq_iff_iff, and_eq_true] + simp only [← Nat.mul_two, Int.bmod_eq_iff_of_lt_of_lt hlb hub, toInt_twoPow_sub_one, or_eq_true, decide_eq_true_eq, _root_.eq_iff_iff, and_eq_true] omega /- ### umod -/ diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean index 8a94958be40a..2c15e728e33d 100644 --- a/src/Init/Data/BitVec/Lemmas.lean +++ b/src/Init/Data/BitVec/Lemmas.lean @@ -4212,6 +4212,7 @@ instance instDecidableExistsBitVec : | 0, _, _ => inferInstance | _ + 1, _, _ => inferInstance + /-! ### Deprecations -/ set_option linter.missingDocs false From dee6fa2f91daa36a7eda1b1290f8a9fa0665aa92 Mon Sep 17 00:00:00 2001 From: Tobias Grosser Date: Wed, 5 Feb 2025 16:52:06 +0000 Subject: [PATCH 06/19] drop sorries --- src/Init/Data/BitVec/Bitblast.lean | 70 ++++++++++++++++++++++++------ 1 file changed, 57 insertions(+), 13 deletions(-) diff --git a/src/Init/Data/BitVec/Bitblast.lean b/src/Init/Data/BitVec/Bitblast.lean index d9326621f688..66f4e83b3475 100644 --- a/src/Init/Data/BitVec/Bitblast.lean +++ b/src/Init/Data/BitVec/Bitblast.lean @@ -1298,14 +1298,33 @@ theorem Int.mul_le_mul_self {x y : Int} {s : Nat} (lbx : -s ≤ x) (ubx : x < s) simp_all theorem toInt_mul_toInt_lt {x y : BitVec w} : x.toInt * y.toInt ≤ 2 ^ (w * 2 - 2) := by - rcases w with _|w' - . simp [BitVec.toInt, BitVec.toNat] - · have xle := le_toInt (x := x); have xlt := toInt_lt (x := x) - have yle := le_toInt (x := y); have ylt := toInt_lt (x := y) - have h : 2 ^ ((w' + 1) * 2 - 2) = 2 ^ ((w' + 1) - 1) * 2 ^ ((w' + 1) - 1) := by - rw [← Nat.pow_add, ←Nat.mul_two, Nat.mul_comm (m := 2) (n := ((w' + 1) - 1)), Nat.mul_sub_one, Nat.mul_comm] + by_cases h : w = 0 + · subst h + revert x y + decide + · have xlt := toInt_lt (x := x); have xle := le_toInt (x := x) + have ylt := toInt_lt (x := y); have yle := le_toInt (x := y) + have h : 2 ^ (w * 2 - 2) = 2 ^ (w - 1) * 2 ^ (w - 1) := by + rw [← Nat.pow_add, ←Nat.mul_two, Nat.mul_comm (m := 2) (n := (w - 1)), Nat.mul_sub_one, Nat.mul_comm] + have mul_le_mul_self_neg {x y : Int} {s : Nat} (lbx : -s ≤ x) (ubx : x < s) (lby : -s ≤ y) (uby : y < s) : + x * y ≤ s * s := by + have : 0 < s * s := Nat.mul_pos (by omega) (by omega) + by_cases hx : 0 < x <;> by_cases hy : 0 < y + · exact Int.mul_le_mul (by omega) (by omega) (by omega) (by omega) + · have : x * y ≤ 0 := Int.mul_nonpos_of_nonneg_of_nonpos (by omega) (by omega) + omega + · rw [Int.mul_comm] + have : y * x ≤ 0 := Int.mul_nonpos_of_nonneg_of_nonpos (by omega) (by omega) + omega + · have : -x * -y ≤ s * s := Int.mul_le_mul (by omega) (by omega) (by omega) (by omega) + simp_all rw_mod_cast [h] - sorry + rw [← Nat.two_pow_pred_mul_two, Int.natCast_mul] at xlt ylt xle yle + exact mul_le_mul_self_neg (by omega) (by omega) (by omega) (by omega) + omega + omega + omega + omega theorem Int.neg_mul_self_le_mul {x y : Int} {s : Nat} (lbx : -s ≤ x) (ubx : x < s) (lby : -s ≤ y) (uby : y < s) : -(s * s) ≤ x * y := by @@ -1316,13 +1335,38 @@ theorem Int.neg_mul_self_le_mul {x y : Int} {s : Nat} (lbx : -s ≤ x) (ubx : x · rw [← Int.neg_mul]; exact mul_le_mul_neg (by omega) (by omega) (by omega) (by omega) · have : 0 < x * y := Int.mul_pos_of_neg_of_neg (by omega) (by omega) ;omega +theorem mul_le_mul_neg {a b c d : Int} + (hac : a ≤ c) (hbd : d ≤ b) (hb : 0 ≤ b) (hc : c ≤ 0) : a * b ≤ c * d := + Int.le_trans (Int.mul_le_mul_of_nonneg_right hac hb) (Int.mul_le_mul_of_nonpos_left hc hbd) + theorem le_toInt_mul_toInt {x y : BitVec w} : -(2 ^ (w * 2 - 2)) ≤ x.toInt * y.toInt := by - have xlt := toInt_lt (x := x); have xle := le_toInt (x := x) - have ylt := toInt_lt (x := y); have yle := le_toInt (x := y) - have h : 2 ^ (w * 2 - 2) = 2 ^ (w - 1) * 2 ^ (w - 1) := by - rw [← Nat.pow_add, ←Nat.mul_two, Nat.mul_comm (m := 2) (n := (w - 1)), Nat.mul_sub_one, Nat.mul_comm] - rw_mod_cast [h] - sorry + by_cases h : w = 0 + · subst h + revert x y + decide + · have xlt := toInt_lt (x := x); have xle := le_toInt (x := x) + have ylt := toInt_lt (x := y); have yle := le_toInt (x := y) + have h : 2 ^ (w * 2 - 2) = 2 ^ (w - 1) * 2 ^ (w - 1) := by + rw [← Nat.pow_add, ←Nat.mul_two, Nat.mul_comm (m := 2) (n := (w - 1)), Nat.mul_sub_one, Nat.mul_comm] + rw_mod_cast [h] + have mul_self_neg_le_mul {x y : Int} {s : Nat} (lbx : -s ≤ x) (ubx : x < s) (lby : -s ≤ y) (uby : y < s) : + -(s * s) ≤ x * y := by + have : 0 * 0 ≤ s * s := Nat.mul_le_mul (by omega) (by omega) + by_cases 0 ≤ x <;> by_cases 0 ≤ y + · have : 0 ≤ x * y := Int.mul_nonneg (by omega) (by omega) + omega + · rw [← Int.neg_mul, Int.mul_comm (a := x)] + exact mul_le_mul_neg (by omega) (by omega) (by omega) (by omega) + · rw [← Int.neg_mul] + exact mul_le_mul_neg (by omega) (by omega) (by omega) (by omega) + · have : 0 < x * y := Int.mul_pos_of_neg_of_neg (by omega) (by omega) + omega + rw [← Nat.two_pow_pred_mul_two, Int.natCast_mul] at xlt ylt xle yle + apply mul_self_neg_le_mul (by omega) (by omega) (by omega) (by omega) + omega + omega + omega + omega theorem toInt_twoPow_of_eq {w i : Nat} (h : i + 1 = w) : (BitVec.twoPow w i).toInt = -(2 ^ i) := by From 6f7469b430f88b9425c05f3554030101d062cf2c Mon Sep 17 00:00:00 2001 From: luisacicolini Date: Wed, 5 Feb 2025 18:52:05 +0000 Subject: [PATCH 07/19] chore: clean proof --- src/Init/Data/BitVec/Bitblast.lean | 38 ++++-------------------------- 1 file changed, 5 insertions(+), 33 deletions(-) diff --git a/src/Init/Data/BitVec/Bitblast.lean b/src/Init/Data/BitVec/Bitblast.lean index 66f4e83b3475..13a3ffbe90d4 100644 --- a/src/Init/Data/BitVec/Bitblast.lean +++ b/src/Init/Data/BitVec/Bitblast.lean @@ -1297,7 +1297,7 @@ theorem Int.mul_le_mul_self {x y : Int} {s : Nat} (lbx : -s ≤ x) (ubx : x < s) · have : -x * -y ≤ s * s := Int.mul_le_mul (by omega) (by omega) (by omega) (by omega) simp_all -theorem toInt_mul_toInt_lt {x y : BitVec w} : x.toInt * y.toInt ≤ 2 ^ (w * 2 - 2) := by +theorem BitVec.toInt_mul_toInt_lt {x y : BitVec w} : x.toInt * y.toInt ≤ 2 ^ (w * 2 - 2) := by by_cases h : w = 0 · subst h revert x y @@ -1306,25 +1306,9 @@ theorem toInt_mul_toInt_lt {x y : BitVec w} : x.toInt * y.toInt ≤ 2 ^ (w * 2 - have ylt := toInt_lt (x := y); have yle := le_toInt (x := y) have h : 2 ^ (w * 2 - 2) = 2 ^ (w - 1) * 2 ^ (w - 1) := by rw [← Nat.pow_add, ←Nat.mul_two, Nat.mul_comm (m := 2) (n := (w - 1)), Nat.mul_sub_one, Nat.mul_comm] - have mul_le_mul_self_neg {x y : Int} {s : Nat} (lbx : -s ≤ x) (ubx : x < s) (lby : -s ≤ y) (uby : y < s) : - x * y ≤ s * s := by - have : 0 < s * s := Nat.mul_pos (by omega) (by omega) - by_cases hx : 0 < x <;> by_cases hy : 0 < y - · exact Int.mul_le_mul (by omega) (by omega) (by omega) (by omega) - · have : x * y ≤ 0 := Int.mul_nonpos_of_nonneg_of_nonpos (by omega) (by omega) - omega - · rw [Int.mul_comm] - have : y * x ≤ 0 := Int.mul_nonpos_of_nonneg_of_nonpos (by omega) (by omega) - omega - · have : -x * -y ≤ s * s := Int.mul_le_mul (by omega) (by omega) (by omega) (by omega) - simp_all rw_mod_cast [h] - rw [← Nat.two_pow_pred_mul_two, Int.natCast_mul] at xlt ylt xle yle - exact mul_le_mul_self_neg (by omega) (by omega) (by omega) (by omega) - omega - omega - omega - omega + rw [← Nat.two_pow_pred_mul_two (by omega), Int.natCast_mul] at xlt ylt xle yle + exact Int.mul_le_mul_self (by omega) (by omega) (by omega) (by omega) theorem Int.neg_mul_self_le_mul {x y : Int} {s : Nat} (lbx : -s ≤ x) (ubx : x < s) (lby : -s ≤ y) (uby : y < s) : -(s * s) ≤ x * y := by @@ -1349,20 +1333,8 @@ theorem le_toInt_mul_toInt {x y : BitVec w} : -(2 ^ (w * 2 - 2)) ≤ x.toInt * y have h : 2 ^ (w * 2 - 2) = 2 ^ (w - 1) * 2 ^ (w - 1) := by rw [← Nat.pow_add, ←Nat.mul_two, Nat.mul_comm (m := 2) (n := (w - 1)), Nat.mul_sub_one, Nat.mul_comm] rw_mod_cast [h] - have mul_self_neg_le_mul {x y : Int} {s : Nat} (lbx : -s ≤ x) (ubx : x < s) (lby : -s ≤ y) (uby : y < s) : - -(s * s) ≤ x * y := by - have : 0 * 0 ≤ s * s := Nat.mul_le_mul (by omega) (by omega) - by_cases 0 ≤ x <;> by_cases 0 ≤ y - · have : 0 ≤ x * y := Int.mul_nonneg (by omega) (by omega) - omega - · rw [← Int.neg_mul, Int.mul_comm (a := x)] - exact mul_le_mul_neg (by omega) (by omega) (by omega) (by omega) - · rw [← Int.neg_mul] - exact mul_le_mul_neg (by omega) (by omega) (by omega) (by omega) - · have : 0 < x * y := Int.mul_pos_of_neg_of_neg (by omega) (by omega) - omega rw [← Nat.two_pow_pred_mul_two, Int.natCast_mul] at xlt ylt xle yle - apply mul_self_neg_le_mul (by omega) (by omega) (by omega) (by omega) + apply Int.neg_mul_self_le_mul (by omega) (by omega) (by omega) (by omega) omega omega omega @@ -1444,7 +1416,7 @@ theorem smulOverflow_eq {w : Nat} (x y : BitVec w) : have := Int.pow_lt_pow (a := 2) (b := ((w + 1) * 2 - 2)) (c := ((w + 1) * 2 - 1)) have := @le_toInt_mul_toInt (w + 1) x y have hlb : -((2 ^ ((w + 1) * 2 - 1) : Nat) * 2) ≤ x.toInt * y.toInt * 2 := by push_cast; omega - have := @toInt_mul_toInt_lt (w + 1) x y + have := @BitVec.toInt_mul_toInt_lt (w + 1) x y have hub : x.toInt * y.toInt * 2 < ((2 ^ ((w + 1) * 2 - 1): Nat) * 2) := Int.mul_lt_mul_of_pos_right (by norm_cast at *; omega) (by omega) rw [BitVec.toInt_signExtend_of_lt (by omega), BitVec.toInt_signExtend_of_lt (by omega), BitVec.toInt_signExtend_of_lt (by omega), BitVec.toInt_signExtend_of_lt (by omega), toInt_twoPow_of_eq (by omega), ←Nat.two_pow_pred_add_two_pow_pred (by omega)] From a9527249b93d6a246f789fbcd21667a239a67151 Mon Sep 17 00:00:00 2001 From: luisacicolini Date: Thu, 6 Feb 2025 11:43:23 +0000 Subject: [PATCH 08/19] chore: bring the theorems back home --- src/Init/Data/BitVec/Bitblast.lean | 151 +--------------------------- src/Init/Data/BitVec/Lemmas.lean | 81 +++++++++++++++ src/Init/Data/Int/DivModLemmas.lean | 7 ++ src/Init/Data/Int/LemmasAux.lean | 28 ++++++ src/Init/Data/Int/Pow.lean | 7 ++ src/Init/Data/Nat/Lemmas.lean | 3 + 6 files changed, 131 insertions(+), 146 deletions(-) diff --git a/src/Init/Data/BitVec/Bitblast.lean b/src/Init/Data/BitVec/Bitblast.lean index 13a3ffbe90d4..774db99384ce 100644 --- a/src/Init/Data/BitVec/Bitblast.lean +++ b/src/Init/Data/BitVec/Bitblast.lean @@ -1251,159 +1251,18 @@ theorem saddOverflow_eq {w : Nat} (x y : BitVec w) : simp omega -theorem Int.emod_eq_add_self_emod {a b : Int} : a % b = (a + b) % b := - Int.add_emod_self.symm - -theorem Int.bmod_eq_iff_of_lt_of_lt {x : Int} {y : Nat} (hge : -y ≤ x * 2) (hlt : x * 2 < y) : - x.bmod y = x := by - simp only [Int.bmod_def] - by_cases 0 ≤ x - · rw [Int.emod_eq_of_lt (by omega) (by omega)]; omega - · rw [Int.emod_eq_add_self_emod, Int.emod_eq_of_lt (by omega) (by omega)]; omega - -theorem BitVec.toInt_twoPow {w i : Nat} : - (BitVec.twoPow w i).toInt = if w ≤ i then (0 : Int) else (if i + 1 = w then -(1 <<< i:Int) else (1 <<< i)) := by - simp only [BitVec.twoPow, BitVec.toInt] - rcases w with _|w' - · simp - · by_cases h : w' + 1 ≤ i - · simp [h]; norm_cast; omega - · simp only [toNat_shiftLeft, toNat_ofNat, zero_lt_succ, one_mod_two_pow, Int.ofNat_emod, h, - ↓reduceIte, Nat.add_right_cancel_iff] - have hy : (2 ^ i % 2 ^ (w' + 1)) = 2 ^ i := by rw [Nat.mod_eq_of_lt (by rw [Nat.pow_lt_pow_iff_right (by omega)]; omega)] - have hj : 2 * 2 ^ i = 2 ^ (i + 1) := by rw [Nat.pow_add, Nat.mul_comm] - norm_cast - simp only [Nat.shiftLeft_eq, Nat.one_mul, hy, hj] - by_cases i + 1 = (w' + 1) - · simp only [show i = w' by omega, Nat.lt_irrefl, ↓reduceIte]; omega - · have sl : 2 ^ (i + 1) < 2 ^ (w' + 1) := by - rw [Nat.pow_lt_pow_iff_right (by omega)] - omega - simp only [sl, ↓reduceIte] - omega - -theorem Int.mul_le_mul_neg {a b c d : Int} - (hac : a ≤ c) (hbd : d ≤ b) (hb : 0 ≤ b) (hc : c ≤ 0) : a * b ≤ c * d := - Int.le_trans (Int.mul_le_mul_of_nonneg_right hac hb) (Int.mul_le_mul_of_nonpos_left hc hbd) - -theorem Int.mul_le_mul_self {x y : Int} {s : Nat} (lbx : -s ≤ x) (ubx : x < s) (lby : -s ≤ y) (uby : y < s) : - x * y ≤ s * s := by - have := Nat.mul_pos (n := s) (m := s) (by omega) (by omega) - by_cases hx : 0 < x <;> by_cases hy : 0 < y - · exact Int.mul_le_mul (by omega) (by omega) (by omega) (by omega) - · have : x * y ≤ 0 := Int.mul_nonpos_of_nonneg_of_nonpos (by omega) (by omega); omega - · rw [Int.mul_comm] - have : y * x ≤ 0 := Int.mul_nonpos_of_nonneg_of_nonpos (by omega) (by omega); omega - · have : -x * -y ≤ s * s := Int.mul_le_mul (by omega) (by omega) (by omega) (by omega) - simp_all - -theorem BitVec.toInt_mul_toInt_lt {x y : BitVec w} : x.toInt * y.toInt ≤ 2 ^ (w * 2 - 2) := by - by_cases h : w = 0 - · subst h - revert x y - decide - · have xlt := toInt_lt (x := x); have xle := le_toInt (x := x) - have ylt := toInt_lt (x := y); have yle := le_toInt (x := y) - have h : 2 ^ (w * 2 - 2) = 2 ^ (w - 1) * 2 ^ (w - 1) := by - rw [← Nat.pow_add, ←Nat.mul_two, Nat.mul_comm (m := 2) (n := (w - 1)), Nat.mul_sub_one, Nat.mul_comm] - rw_mod_cast [h] - rw [← Nat.two_pow_pred_mul_two (by omega), Int.natCast_mul] at xlt ylt xle yle - exact Int.mul_le_mul_self (by omega) (by omega) (by omega) (by omega) - -theorem Int.neg_mul_self_le_mul {x y : Int} {s : Nat} (lbx : -s ≤ x) (ubx : x < s) (lby : -s ≤ y) (uby : y < s) : - -(s * s) ≤ x * y := by - have := Nat.mul_pos (n := s) (m := s) (by omega) (by omega) - by_cases 0 ≤ x <;> by_cases 0 ≤ y - · have : 0 ≤ x * y := Int.mul_nonneg (by omega) (by omega); omega - · rw [← Int.neg_mul, Int.mul_comm (a := x)]; exact mul_le_mul_neg (by omega) (by omega) (by omega) (by omega) - · rw [← Int.neg_mul]; exact mul_le_mul_neg (by omega) (by omega) (by omega) (by omega) - · have : 0 < x * y := Int.mul_pos_of_neg_of_neg (by omega) (by omega) ;omega - -theorem mul_le_mul_neg {a b c d : Int} - (hac : a ≤ c) (hbd : d ≤ b) (hb : 0 ≤ b) (hc : c ≤ 0) : a * b ≤ c * d := - Int.le_trans (Int.mul_le_mul_of_nonneg_right hac hb) (Int.mul_le_mul_of_nonpos_left hc hbd) - -theorem le_toInt_mul_toInt {x y : BitVec w} : -(2 ^ (w * 2 - 2)) ≤ x.toInt * y.toInt := by - by_cases h : w = 0 - · subst h - revert x y - decide - · have xlt := toInt_lt (x := x); have xle := le_toInt (x := x) - have ylt := toInt_lt (x := y); have yle := le_toInt (x := y) - have h : 2 ^ (w * 2 - 2) = 2 ^ (w - 1) * 2 ^ (w - 1) := by - rw [← Nat.pow_add, ←Nat.mul_two, Nat.mul_comm (m := 2) (n := (w - 1)), Nat.mul_sub_one, Nat.mul_comm] - rw_mod_cast [h] - rw [← Nat.two_pow_pred_mul_two, Int.natCast_mul] at xlt ylt xle yle - apply Int.neg_mul_self_le_mul (by omega) (by omega) (by omega) (by omega) - omega - omega - omega - omega - -theorem toInt_twoPow_of_eq {w i : Nat} (h : i + 1 = w) : - (BitVec.twoPow w i).toInt = -(2 ^ i) := by - simp only [BitVec.toInt_twoPow, show ¬(w ≤ i) by omega, ↓reduceIte, h, Nat.shiftLeft_eq, Nat.one_mul] - norm_cast - -@[simp] -theorem toInt_one {w : Nat} (h : 1 < w ) : (1#w).toInt = 1 := by - have : 1 < 2 ^ w := Nat.one_lt_two_pow (by omega) - unfold BitVec.toInt - simp only [BitVec.toNat_ofNat, Int.ofNat_emod] - rw [Nat.mod_eq_of_lt (by omega)] - by_cases hw' : 2 * 1 < 2 ^ w - · simp only [Nat.mul_one, hw', ↓reduceIte, Int.Nat.cast_ofNat_Int] - norm_cast - rw [Nat.mod_eq_of_lt (by omega)] - · simp only [Int.not_lt] at hw' - have h2 : 2 * 1 = 2 ^ 1 := by rw [Nat.mul_one, Nat.pow_one] - rw [h2, Nat.pow_lt_pow_iff_right (a := 2) (by omega)] at hw' - omega - -@[simp] -theorem toInt_twoPow_sub_one : (BitVec.twoPow w (w - 1) - 1#w).toInt = 2 ^ (w - 1) - 1 := by - rcases w with _|_|w - · decide - · decide - · have : 1 < 2 ^ (w + 1 + 1) := Nat.one_lt_two_pow (by omega) - rw_mod_cast [BitVec.twoPow, BitVec.toInt_sub, BitVec.toInt_shiftLeft, BitVec.toNat_ofNat, - Int.bmod_sub_bmod_congr, toInt_one (by omega), Nat.shiftLeft_eq, - Nat.mod_eq_of_lt (by omega), Int.bmod_eq_iff_of_lt_of_lt] - simp only [Nat.add_one_sub_one, Nat.one_mul] - · have : 0 < (2 ^ (w + 1 + 1 - 1) - 1) * 2 := by simp; omega - norm_cast - omega - · rw [← Nat.two_pow_pred_add_two_pow_pred (w := w + 1 + 1) (by omega)] - omega - -theorem toNat_mul_toNat_lt {x y : BitVec w} : x.toNat * y.toNat < 2 ^ (w * 2) := by - have := BitVec.isLt x; have := BitVec.isLt y - simp only [Nat.mul_two, Nat.pow_add] - exact Nat.mul_lt_mul_of_le_of_lt (by omega) (by omega) (by omega) - --- from mathlib -theorem Nat.mul_mod_mod (a b c : Nat) : (a * (b % c)) % c = a * b % c := by - rw [mul_mod, mod_mod, ← mul_mod] - theorem umulOverflow_eq {w : Nat} (x y : BitVec w) : umulOverflow x y = (0 < w && BitVec.twoPow (w * 2) w ≤ x.zeroExtend (w * 2) * y.zeroExtend (w * 2)) := by simp only [umulOverflow, ge_iff_le, truncate_eq_setWidth, le_def, toNat_twoPow, toNat_mul, - toNat_setWidth, Nat.mul_mod_mod, mod_mul_mod] + toNat_setWidth, Nat.mul_mod_mod, Nat.mod_mul_mod] rcases w with _|w' · decide +revert · simp only [show 0 < w' + 1 by omega, decide_true, Bool.true_and, decide_eq_decide] - rw [Nat.mod_eq_of_lt toNat_mul_toNat_lt, Nat.mod_eq_of_lt] + rw [Nat.mod_eq_of_lt BitVec.toNat_mul_toNat_lt, Nat.mod_eq_of_lt] have := Nat.pow_lt_pow_of_lt (a := 2) (n := (w' + 1)) (m := (w' + 1) * 2) omega -theorem Int.pow_lt_pow {a : Int} {b c : Nat} (ha : (1 : Nat) < a) (hbc : b < c): - a ^ b < a ^ c := by - rw [← Int.toNat_of_nonneg (a := a) (by omega), ← Int.natCast_pow, ← Int.natCast_pow] - have := Nat.pow_lt_pow_of_lt (a := a.toNat) (m := c) (n := b) - simp only [Int.ofNat_lt] - omega - theorem smulOverflow_eq {w : Nat} (x y : BitVec w) : smulOverflow x y = (w ≠ 0) || (((BitVec.intMin w).signExtend (w * 2)).sle (x.signExtend (w * 2) * y.signExtend (w * 2)) && @@ -1414,13 +1273,13 @@ theorem smulOverflow_eq {w : Nat} (x y : BitVec w) : · simp only [Bool.false_or, BitVec.intMin, BitVec.intMax, BitVec.sle, BitVec.toInt_mul, decide_eq_true_eq, BitVec.ofNat_eq_ofNat] have := Int.pow_lt_pow (a := 2) (b := ((w + 1) * 2 - 2)) (c := ((w + 1) * 2 - 1)) - have := @le_toInt_mul_toInt (w + 1) x y + have := @BitVec.le_toInt_mul_toInt (w + 1) x y have hlb : -((2 ^ ((w + 1) * 2 - 1) : Nat) * 2) ≤ x.toInt * y.toInt * 2 := by push_cast; omega have := @BitVec.toInt_mul_toInt_lt (w + 1) x y have hub : x.toInt * y.toInt * 2 < ((2 ^ ((w + 1) * 2 - 1): Nat) * 2) := Int.mul_lt_mul_of_pos_right (by norm_cast at *; omega) (by omega) rw [BitVec.toInt_signExtend_of_lt (by omega), BitVec.toInt_signExtend_of_lt (by omega), - BitVec.toInt_signExtend_of_lt (by omega), BitVec.toInt_signExtend_of_lt (by omega), toInt_twoPow_of_eq (by omega), ←Nat.two_pow_pred_add_two_pow_pred (by omega)] - simp only [← Nat.mul_two, Int.bmod_eq_iff_of_lt_of_lt hlb hub, toInt_twoPow_sub_one, or_eq_true, decide_eq_true_eq, _root_.eq_iff_iff, and_eq_true] + BitVec.toInt_signExtend_of_lt (by omega), BitVec.toInt_signExtend_of_lt (by omega), BitVec.toInt_twoPow_of_eq (by omega), ←Nat.two_pow_pred_add_two_pow_pred (by omega)] + simp only [← Nat.mul_two, Int.bmod_eq_iff_of_lt_of_lt hlb hub, BitVec.toInt_twoPow_sub_one, or_eq_true, decide_eq_true_eq, _root_.eq_iff_iff, and_eq_true] omega /- ### umod -/ diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean index 2c15e728e33d..3ea5ca5feee4 100644 --- a/src/Init/Data/BitVec/Lemmas.lean +++ b/src/Init/Data/BitVec/Lemmas.lean @@ -14,6 +14,7 @@ import Init.Data.Nat.Mod import Init.Data.Nat.Div.Lemmas import Init.Data.Int.Bitwise.Lemmas import Init.Data.Int.Pow +import Init.Data.Int.LemmasAux set_option linter.missingDocs true @@ -301,6 +302,20 @@ theorem getLsbD_ofNat (n : Nat) (x : Nat) (i : Nat) : @[simp] theorem getMsbD_zero : (0#w).getMsbD i = false := by simp [getMsbD] +@[simp] theorem toInt_one {w : Nat} (h : 1 < w ) : (1#w).toInt = 1 := by + have : 1 < 2 ^ w := Nat.one_lt_two_pow (by omega) + unfold BitVec.toInt + simp only [BitVec.toNat_ofNat, Int.ofNat_emod] + rw [Nat.mod_eq_of_lt (by omega)] + by_cases hw' : 2 * 1 < 2 ^ w + · simp only [Nat.mul_one, hw', ↓reduceIte, Int.Nat.cast_ofNat_Int] + norm_cast + rw [Nat.mod_eq_of_lt (by omega)] + · simp only [Int.not_lt] at hw' + have h2 : 2 * 1 = 2 ^ 1 := by rw [Nat.mul_one, Nat.pow_one] + rw [h2, Nat.pow_lt_pow_iff_right (a := 2) (by omega)] at hw' + omega + @[simp] theorem getLsbD_one : (1#w).getLsbD i = (decide (0 < w) && decide (i = 0)) := by simp only [getLsbD, toNat_ofNat, Nat.testBit_mod_two_pow] by_cases h : i = 0 @@ -3682,6 +3697,67 @@ theorem udiv_twoPow_eq_of_lt {w : Nat} {x : BitVec w} {k : Nat} (hk : k < w) : x have : 2^k < 2^w := Nat.pow_lt_pow_of_lt (by decide) hk simp [bv_toNat, Nat.shiftRight_eq_div_pow, Nat.mod_eq_of_lt this] +theorem toInt_twoPow {w i : Nat} : + (BitVec.twoPow w i).toInt = if w ≤ i then (0 : Int) else (if i + 1 = w then -(1 <<< i:Int) else (1 <<< i)) := by + simp only [BitVec.twoPow, BitVec.toInt] + rcases w with _|w' + · simp + · by_cases h : w' + 1 ≤ i + · simp [h]; norm_cast; omega + · simp only [toNat_shiftLeft, toNat_ofNat, Nat.zero_lt_succ, Nat.one_mod_two_pow, Int.ofNat_emod, h, + ↓reduceIte, Nat.add_right_cancel_iff] + have hy : (2 ^ i % 2 ^ (w' + 1)) = 2 ^ i := by rw [Nat.mod_eq_of_lt (by rw [Nat.pow_lt_pow_iff_right (by omega)]; omega)] + have hj : 2 * 2 ^ i = 2 ^ (i + 1) := by rw [Nat.pow_add, Nat.mul_comm] + norm_cast + simp only [Nat.shiftLeft_eq, Nat.one_mul, hy, hj] + by_cases i + 1 = (w' + 1) + · simp only [show i = w' by omega, Nat.lt_irrefl, ↓reduceIte]; omega + · simp only [show 2 ^ (i + 1) < 2 ^ (w' + 1) by rw [Nat.pow_lt_pow_iff_right (by omega)]; omega, ↓reduceIte] + omega + +theorem toInt_twoPow_of_eq {w i : Nat} (h : i + 1 = w) : + (BitVec.twoPow w i).toInt = -(2 ^ i) := by + simp only [toInt_twoPow, show ¬(w ≤ i) by omega, ↓reduceIte, h, Nat.shiftLeft_eq, Nat.one_mul] + norm_cast + +theorem toInt_mul_toInt_lt {x y : BitVec w} : x.toInt * y.toInt ≤ 2 ^ (w * 2 - 2) := by + rcases w with _|w + · simp [of_length_zero] + · have xlt := toInt_lt (x := x); have xle := le_toInt (x := x) + have ylt := toInt_lt (x := y); have yle := le_toInt (x := y) + have h : 2 ^ ((w + 1) * 2 - 2) = 2 ^ ((w + 1) - 1) * 2 ^ ((w + 1) - 1) := by + rw [← Nat.pow_add, ←Nat.mul_two, Nat.mul_comm (m := 2) (n := ((w + 1) - 1)), Nat.mul_sub_one, Nat.mul_comm] + rw_mod_cast [h] + rw [← Nat.two_pow_pred_mul_two (by omega), Int.natCast_mul] at xlt ylt xle yle + exact Int.mul_le_mul_self (by omega) (by omega) (by omega) (by omega) + +theorem le_toInt_mul_toInt {x y : BitVec w} : - (2 ^ (w * 2 - 2)) ≤ x.toInt * y.toInt := by + rcases w with _|w + · simp [of_length_zero] + · have xlt := toInt_lt (x := x); have xle := le_toInt (x := x) + have ylt := toInt_lt (x := y); have yle := le_toInt (x := y) + have h : 2 ^ ((w + 1) * 2 - 2) = 2 ^ ((w + 1) - 1) * 2 ^ ((w + 1) - 1) := by + rw [← Nat.pow_add, ←Nat.mul_two, Nat.mul_comm (m := 2) (n := ((w + 1) - 1)), Nat.mul_sub_one, Nat.mul_comm] + rw_mod_cast [h] + rw [← Nat.two_pow_pred_mul_two (by omega), Int.natCast_mul] at xlt ylt xle yle + exact Int.neg_mul_self_le_mul (by omega) (by omega) (by omega) (by omega) + +@[simp] +theorem toInt_twoPow_sub_one : (BitVec.twoPow w (w - 1) - 1#w).toInt = 2 ^ (w - 1) - 1 := by + rcases w with _|_|w + · decide + · decide + · have : 1 < 2 ^ (w + 1 + 1) := Nat.one_lt_two_pow (by omega) + rw_mod_cast [BitVec.twoPow, BitVec.toInt_sub, BitVec.toInt_shiftLeft, BitVec.toNat_ofNat, + Int.bmod_sub_bmod_congr, BitVec.toInt_one (by omega), Nat.shiftLeft_eq, + Nat.mod_eq_of_lt (by omega), Int.bmod_eq_iff_of_lt_of_lt] + simp only [Nat.add_one_sub_one, Nat.one_mul] + · have : 0 < (2 ^ (w + 1 + 1 - 1) - 1) * 2 := by simp; omega + norm_cast + omega + · rw [← Nat.two_pow_pred_add_two_pow_pred (w := w + 1 + 1) (by omega)] + omega + /- ### cons -/ @[simp] theorem true_cons_zero : cons true 0#w = twoPow (w + 1) w := by @@ -3922,6 +3998,7 @@ theorem getLsbD_intMax (w : Nat) : (intMax w).getLsbD i = decide (i + 1 < w) := · rw [Nat.sub_add_cancel (Nat.two_pow_pos (w - 1)), Nat.two_pow_pred_mod_two_pow (by omega)] + /-! ### Non-overflow theorems -/ /-- If `x.toNat + y.toNat < 2^w`, then the addition `(x + y)` does not overflow. -/ @@ -3959,6 +4036,10 @@ theorem toNat_mul_of_lt {w} {x y : BitVec w} (h : x.toNat * y.toNat < 2^w) : (x * y).toNat = x.toNat * y.toNat := by rw [BitVec.toNat_mul, Nat.mod_eq_of_lt h] +theorem toNat_mul_toNat_lt {x y : BitVec w} : x.toNat * y.toNat < 2 ^ (w * 2) := by + have := BitVec.isLt x; have := BitVec.isLt y + simp only [Nat.mul_two, Nat.pow_add] + exact Nat.mul_lt_mul_of_le_of_lt (by omega) (by omega) (by omega) /-- `x ≤ y + z` if and only if `x - z ≤ y` diff --git a/src/Init/Data/Int/DivModLemmas.lean b/src/Init/Data/Int/DivModLemmas.lean index 64102471c7f4..1703ebf9d01f 100644 --- a/src/Init/Data/Int/DivModLemmas.lean +++ b/src/Init/Data/Int/DivModLemmas.lean @@ -481,6 +481,9 @@ theorem lt_mul_ediv_self_add {x k : Int} (h : 0 < k) : x < k * (x / k) + k := @[simp] theorem add_emod_self_left {a b : Int} : (a + b) % a = b % a := by rw [Int.add_comm, Int.add_emod_self] +theorem Int.emod_eq_add_self_emod {a b : Int} : a % b = (a + b) % b := + Int.add_emod_self.symm + theorem neg_emod {a b : Int} : -a % b = (b - a) % b := by rw [← add_emod_self_left]; rfl @@ -820,6 +823,10 @@ theorem ediv_eq_ediv_of_mul_eq_mul {a b c d : Int} Int.ediv_eq_of_eq_mul_right H3 <| by rw [← Int.mul_ediv_assoc _ H2]; exact (Int.ediv_eq_of_eq_mul_left H4 H5.symm).symm +theorem mul_le_mul_neg {a b c d : Int} + (hac : a ≤ c) (hbd : d ≤ b) (hb : 0 ≤ b) (hc : c ≤ 0) : a * b ≤ c * d := + Int.le_trans (Int.mul_le_mul_of_nonneg_right hac hb) (Int.mul_le_mul_of_nonpos_left hc hbd) + /-! ### tdiv -/ @[simp] protected theorem tdiv_one : ∀ a : Int, a.tdiv 1 = a diff --git a/src/Init/Data/Int/LemmasAux.lean b/src/Init/Data/Int/LemmasAux.lean index 756b1cc6676e..527f3068042e 100644 --- a/src/Init/Data/Int/LemmasAux.lean +++ b/src/Init/Data/Int/LemmasAux.lean @@ -45,4 +45,32 @@ theorem bmod_neg_iff {m : Nat} {x : Int} (h2 : -m ≤ x) (h1 : x < m) : · rw [Int.emod_eq_of_lt xpos (by omega)]; omega · rw [Int.add_emod_self.symm, Int.emod_eq_of_lt (by omega) (by omega)]; omega +theorem bmod_eq_iff_of_lt_of_lt {x : Int} {y : Nat} (hge : -y ≤ x * 2) (hlt : x * 2 < y) : + x.bmod y = x := by + simp only [Int.bmod_def] + by_cases 0 ≤ x + · rw [Int.emod_eq_of_lt (by omega) (by omega)]; omega + · rw [Int.emod_eq_add_self_emod, Int.emod_eq_of_lt (by omega) (by omega)]; omega + + +theorem mul_le_mul_self {x y : Int} {s : Nat} (lbx : -s ≤ x) (ubx : x < s) (lby : -s ≤ y) (uby : y < s) : + x * y ≤ s * s := by + have := Nat.mul_pos (n := s) (m := s) (by omega) (by omega) + by_cases hx : 0 < x <;> by_cases hy : 0 < y + · exact Int.mul_le_mul (by omega) (by omega) (by omega) (by omega) + · have : x * y ≤ 0 := Int.mul_nonpos_of_nonneg_of_nonpos (by omega) (by omega); omega + · rw [Int.mul_comm] + have : y * x ≤ 0 := Int.mul_nonpos_of_nonneg_of_nonpos (by omega) (by omega); omega + · have : -x * -y ≤ s * s := Int.mul_le_mul (by omega) (by omega) (by omega) (by omega) + simp_all + +theorem neg_mul_self_le_mul {x y : Int} {s : Nat} (lbx : -s ≤ x) (ubx : x < s) (lby : -s ≤ y) (uby : y < s) : + -(s * s) ≤ x * y := by + have := Nat.mul_pos (n := s) (m := s) (by omega) (by omega) + by_cases 0 ≤ x <;> by_cases 0 ≤ y + · have : 0 ≤ x * y := Int.mul_nonneg (by omega) (by omega); omega + · rw [← Int.neg_mul, Int.mul_comm (a := x)]; exact Int.mul_le_mul_neg (by omega) (by omega) (by omega) (by omega) + · rw [← Int.neg_mul]; exact Int.mul_le_mul_neg (by omega) (by omega) (by omega) (by omega) + · have : 0 < x * y := Int.mul_pos_of_neg_of_neg (by omega) (by omega) ;omega + end Int diff --git a/src/Init/Data/Int/Pow.lean b/src/Init/Data/Int/Pow.lean index 233849788b86..820ff3f2f29a 100644 --- a/src/Init/Data/Int/Pow.lean +++ b/src/Init/Data/Int/Pow.lean @@ -56,4 +56,11 @@ protected theorem two_pow_pred_sub_two_pow' {w : Nat} (h : 0 < w) : rw [← Nat.two_pow_pred_add_two_pow_pred h] simp [h] +theorem pow_lt_pow {a : Int} {b c : Nat} (ha : (1 : Nat) < a) (hbc : b < c): + a ^ b < a ^ c := by + rw [← Int.toNat_of_nonneg (a := a) (by omega), ← Int.natCast_pow, ← Int.natCast_pow] + have := Nat.pow_lt_pow_of_lt (a := a.toNat) (m := c) (n := b) + simp only [Int.ofNat_lt] + omega + end Int diff --git a/src/Init/Data/Nat/Lemmas.lean b/src/Init/Data/Nat/Lemmas.lean index 50c161fb8a2f..b6e57c5c82d2 100644 --- a/src/Init/Data/Nat/Lemmas.lean +++ b/src/Init/Data/Nat/Lemmas.lean @@ -671,6 +671,9 @@ theorem mul_mod (a b n : Nat) : a * b % n = (a % n) * (b % n) % n := by Nat.mul_assoc, Nat.mul_assoc, ← Nat.mul_add n, add_mul_mod_self_left, Nat.mul_comm _ (n * (b / n)), Nat.mul_assoc, add_mul_mod_self_left] +theorem mul_mod_mod (a b c : Nat) : (a * (b % c)) % c = a * b % c := by + rw [mul_mod, mod_mod, ← mul_mod] + @[simp] theorem mod_add_mod (m n k : Nat) : (m % n + k) % n = (m + k) % n := by have := (add_mul_mod_self_left (m % n + k) n (m / n)).symm rwa [Nat.add_right_comm, mod_add_div] at this From 7509cb60d4929db13ffcd0dd824291c8709b6936 Mon Sep 17 00:00:00 2001 From: luisacicolini Date: Thu, 6 Feb 2025 11:44:04 +0000 Subject: [PATCH 09/19] chore: undo unwanted change --- src/Init/Data/BitVec/Bitblast.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Init/Data/BitVec/Bitblast.lean b/src/Init/Data/BitVec/Bitblast.lean index 774db99384ce..d4b7153b5e9f 100644 --- a/src/Init/Data/BitVec/Bitblast.lean +++ b/src/Init/Data/BitVec/Bitblast.lean @@ -1231,7 +1231,7 @@ theorem shiftRight_eq_ushiftRightRec (x : BitVec w₁) (y : BitVec w₂) : · simp [of_length_zero] · simp [ushiftRightRec_eq] -/-! ### Overflow -/ +/-! ### Overflow definitions -/ /-- Unsigned addition overflows iff the final carry bit of the addition circuit is `true`. -/ theorem uaddOverflow_eq {w : Nat} (x y : BitVec w) : From cc7128ffeee09b84a68dd990308da79dcd482a81 Mon Sep 17 00:00:00 2001 From: luisacicolini Date: Thu, 6 Feb 2025 11:44:36 +0000 Subject: [PATCH 10/19] chore: undo unwanted change --- src/Init/Data/BitVec/Lemmas.lean | 1 - 1 file changed, 1 deletion(-) diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean index 3ea5ca5feee4..42ed2fdd5d81 100644 --- a/src/Init/Data/BitVec/Lemmas.lean +++ b/src/Init/Data/BitVec/Lemmas.lean @@ -3998,7 +3998,6 @@ theorem getLsbD_intMax (w : Nat) : (intMax w).getLsbD i = decide (i + 1 < w) := · rw [Nat.sub_add_cancel (Nat.two_pow_pos (w - 1)), Nat.two_pow_pred_mod_two_pow (by omega)] - /-! ### Non-overflow theorems -/ /-- If `x.toNat + y.toNat < 2^w`, then the addition `(x + y)` does not overflow. -/ From 199f7cc993bb7c3c64b8fe7de2436c442b28ccf0 Mon Sep 17 00:00:00 2001 From: luisacicolini Date: Thu, 6 Feb 2025 11:44:51 +0000 Subject: [PATCH 11/19] chore: undo unwanted change --- src/Init/Data/BitVec/Lemmas.lean | 1 - 1 file changed, 1 deletion(-) diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean index 42ed2fdd5d81..1b73f04608c3 100644 --- a/src/Init/Data/BitVec/Lemmas.lean +++ b/src/Init/Data/BitVec/Lemmas.lean @@ -4292,7 +4292,6 @@ instance instDecidableExistsBitVec : | 0, _, _ => inferInstance | _ + 1, _, _ => inferInstance - /-! ### Deprecations -/ set_option linter.missingDocs false From 1ebc9b43a406f4291bc42ecf5dfa7aedbc076419 Mon Sep 17 00:00:00 2001 From: luisacicolini Date: Thu, 6 Feb 2025 11:45:02 +0000 Subject: [PATCH 12/19] chore: undo unwanted change --- src/Init/Data/Int/LemmasAux.lean | 1 - 1 file changed, 1 deletion(-) diff --git a/src/Init/Data/Int/LemmasAux.lean b/src/Init/Data/Int/LemmasAux.lean index 527f3068042e..2e5c5a3338a2 100644 --- a/src/Init/Data/Int/LemmasAux.lean +++ b/src/Init/Data/Int/LemmasAux.lean @@ -52,7 +52,6 @@ theorem bmod_eq_iff_of_lt_of_lt {x : Int} {y : Nat} (hge : -y ≤ x * 2) (hlt : · rw [Int.emod_eq_of_lt (by omega) (by omega)]; omega · rw [Int.emod_eq_add_self_emod, Int.emod_eq_of_lt (by omega) (by omega)]; omega - theorem mul_le_mul_self {x y : Int} {s : Nat} (lbx : -s ≤ x) (ubx : x < s) (lby : -s ≤ y) (uby : y < s) : x * y ≤ s * s := by have := Nat.mul_pos (n := s) (m := s) (by omega) (by omega) From fcce13fc5da7e39ac4cbf82d34809f72686d2f09 Mon Sep 17 00:00:00 2001 From: luisacicolini Date: Thu, 6 Feb 2025 13:56:26 +0000 Subject: [PATCH 13/19] chore: more cleaning --- src/Init/Data/Int/LemmasAux.lean | 12 ++++++------ src/Std/Tactic/BVDecide/Normalize/BitVec.lean | 2 -- tests/lean/run/bv_decide_rewriter.lean | 1 - 3 files changed, 6 insertions(+), 9 deletions(-) diff --git a/src/Init/Data/Int/LemmasAux.lean b/src/Init/Data/Int/LemmasAux.lean index 2e5c5a3338a2..95e2d74b3846 100644 --- a/src/Init/Data/Int/LemmasAux.lean +++ b/src/Init/Data/Int/LemmasAux.lean @@ -48,8 +48,8 @@ theorem bmod_neg_iff {m : Nat} {x : Int} (h2 : -m ≤ x) (h1 : x < m) : theorem bmod_eq_iff_of_lt_of_lt {x : Int} {y : Nat} (hge : -y ≤ x * 2) (hlt : x * 2 < y) : x.bmod y = x := by simp only [Int.bmod_def] - by_cases 0 ≤ x - · rw [Int.emod_eq_of_lt (by omega) (by omega)]; omega + rcases x + · rw [Int.emod_eq_of_lt (by simp only [ofNat_eq_coe]; omega) (by omega)]; omega · rw [Int.emod_eq_add_self_emod, Int.emod_eq_of_lt (by omega) (by omega)]; omega theorem mul_le_mul_self {x y : Int} {s : Nat} (lbx : -s ≤ x) (ubx : x < s) (lby : -s ≤ y) (uby : y < s) : @@ -58,10 +58,10 @@ theorem mul_le_mul_self {x y : Int} {s : Nat} (lbx : -s ≤ x) (ubx : x < s) (lb by_cases hx : 0 < x <;> by_cases hy : 0 < y · exact Int.mul_le_mul (by omega) (by omega) (by omega) (by omega) · have : x * y ≤ 0 := Int.mul_nonpos_of_nonneg_of_nonpos (by omega) (by omega); omega - · rw [Int.mul_comm] - have : y * x ≤ 0 := Int.mul_nonpos_of_nonneg_of_nonpos (by omega) (by omega); omega + · have : x * y ≤ 0 := Int.mul_nonpos_of_nonpos_of_nonneg (by omega) (by omega); omega · have : -x * -y ≤ s * s := Int.mul_le_mul (by omega) (by omega) (by omega) (by omega) - simp_all + simp only [gt_iff_lt, Int.mul_neg, Int.neg_mul, Int.neg_neg] at this + omega theorem neg_mul_self_le_mul {x y : Int} {s : Nat} (lbx : -s ≤ x) (ubx : x < s) (lby : -s ≤ y) (uby : y < s) : -(s * s) ≤ x * y := by @@ -70,6 +70,6 @@ theorem neg_mul_self_le_mul {x y : Int} {s : Nat} (lbx : -s ≤ x) (ubx : x < s) · have : 0 ≤ x * y := Int.mul_nonneg (by omega) (by omega); omega · rw [← Int.neg_mul, Int.mul_comm (a := x)]; exact Int.mul_le_mul_neg (by omega) (by omega) (by omega) (by omega) · rw [← Int.neg_mul]; exact Int.mul_le_mul_neg (by omega) (by omega) (by omega) (by omega) - · have : 0 < x * y := Int.mul_pos_of_neg_of_neg (by omega) (by omega) ;omega + · have : 0 < x * y := Int.mul_pos_of_neg_of_neg (by omega) (by omega); omega end Int diff --git a/src/Std/Tactic/BVDecide/Normalize/BitVec.lean b/src/Std/Tactic/BVDecide/Normalize/BitVec.lean index 52b166a9f449..55adf4e78e51 100644 --- a/src/Std/Tactic/BVDecide/Normalize/BitVec.lean +++ b/src/Std/Tactic/BVDecide/Normalize/BitVec.lean @@ -330,14 +330,12 @@ attribute [bv_normalize] BitVec.umod_zero attribute [bv_normalize] BitVec.umod_one attribute [bv_normalize] BitVec.umod_eq_and - attribute [bv_normalize] BitVec.umulOverflow_eq attribute [bv_normalize] BitVec.smulOverflow_eq attribute [bv_normalize] BitVec.saddOverflow_eq attribute [bv_normalize] BitVec.uaddOverflow_eq - /-- `x / (BitVec.ofNat n)` where `n = 2^k` is the same as shifting `x` right by `k`. -/ theorem BitVec.udiv_ofNat_eq_of_lt (w : Nat) (x : BitVec w) (n : Nat) (k : Nat) (hk : 2 ^ k = n) (hlt : k < w) : x / (BitVec.ofNat w n) = x >>> k := by diff --git a/tests/lean/run/bv_decide_rewriter.lean b/tests/lean/run/bv_decide_rewriter.lean index 27fa3164f1d5..da8e2f445b72 100644 --- a/tests/lean/run/bv_decide_rewriter.lean +++ b/tests/lean/run/bv_decide_rewriter.lean @@ -89,7 +89,6 @@ example (x y : BitVec 16) : BitVec.saddOverflow x y = (x.msb = y.msb ∧ ¬(x + example (x y : BitVec w) : BitVec.uaddOverflow x y = (x.setWidth (w + 1) + y.setWidth (w + 1)).msb := by bv_normalize example (x y : BitVec w) : BitVec.saddOverflow x y = (x.msb = y.msb ∧ ¬(x + y).msb = x.msb) := by bv_normalize - -- not_neg example {x : BitVec 16} : ~~~(-x) = x + (-1#16) := by bv_normalize example {x : BitVec 16} : ~~~(~~~x + 1#16) = x + (-1#16) := by bv_normalize From 89a87da466e1890dcb88d73b9293ab197677f04c Mon Sep 17 00:00:00 2001 From: luisacicolini Date: Thu, 6 Feb 2025 14:08:28 +0000 Subject: [PATCH 14/19] chore: undo unwanted change --- tests/lean/run/bv_decide_rewriter.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/tests/lean/run/bv_decide_rewriter.lean b/tests/lean/run/bv_decide_rewriter.lean index da8e2f445b72..27fa3164f1d5 100644 --- a/tests/lean/run/bv_decide_rewriter.lean +++ b/tests/lean/run/bv_decide_rewriter.lean @@ -89,6 +89,7 @@ example (x y : BitVec 16) : BitVec.saddOverflow x y = (x.msb = y.msb ∧ ¬(x + example (x y : BitVec w) : BitVec.uaddOverflow x y = (x.setWidth (w + 1) + y.setWidth (w + 1)).msb := by bv_normalize example (x y : BitVec w) : BitVec.saddOverflow x y = (x.msb = y.msb ∧ ¬(x + y).msb = x.msb) := by bv_normalize + -- not_neg example {x : BitVec 16} : ~~~(-x) = x + (-1#16) := by bv_normalize example {x : BitVec 16} : ~~~(~~~x + 1#16) = x + (-1#16) := by bv_normalize From 155971c6072ff8fd1f8cd87160446ea784cfa0c9 Mon Sep 17 00:00:00 2001 From: Siddharth Bhat Date: Thu, 6 Feb 2025 14:36:55 +0000 Subject: [PATCH 15/19] chore: shorter proof of toInt_one_of_lt --- src/Init/Data/BitVec/Lemmas.lean | 23 +++++++++-------------- 1 file changed, 9 insertions(+), 14 deletions(-) diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean index 1b73f04608c3..a51488b90380 100644 --- a/src/Init/Data/BitVec/Lemmas.lean +++ b/src/Init/Data/BitVec/Lemmas.lean @@ -302,19 +302,6 @@ theorem getLsbD_ofNat (n : Nat) (x : Nat) (i : Nat) : @[simp] theorem getMsbD_zero : (0#w).getMsbD i = false := by simp [getMsbD] -@[simp] theorem toInt_one {w : Nat} (h : 1 < w ) : (1#w).toInt = 1 := by - have : 1 < 2 ^ w := Nat.one_lt_two_pow (by omega) - unfold BitVec.toInt - simp only [BitVec.toNat_ofNat, Int.ofNat_emod] - rw [Nat.mod_eq_of_lt (by omega)] - by_cases hw' : 2 * 1 < 2 ^ w - · simp only [Nat.mul_one, hw', ↓reduceIte, Int.Nat.cast_ofNat_Int] - norm_cast - rw [Nat.mod_eq_of_lt (by omega)] - · simp only [Int.not_lt] at hw' - have h2 : 2 * 1 = 2 ^ 1 := by rw [Nat.mul_one, Nat.pow_one] - rw [h2, Nat.pow_lt_pow_iff_right (a := 2) (by omega)] at hw' - omega @[simp] theorem getLsbD_one : (1#w).getLsbD i = (decide (0 < w) && decide (i = 0)) := by simp only [getLsbD, toNat_ofNat, Nat.testBit_mod_two_pow] @@ -512,6 +499,14 @@ theorem toInt_eq_toNat_bmod (x : BitVec n) : x.toInt = Int.bmod x.toNat (2^n) := rw [Int.bmod_neg] <;> simp only [←Int.ofNat_emod, toNat_mod_cancel] omega +@[simp] theorem toInt_one_of_lt {w : Nat} (h : 1 < w) : (1#w).toInt = 1 := by + rw [toInt_eq_msb_cond] + simp only [msb_one, show w ≠ 1 by omega, decide_false, Bool.false_eq_true, ↓reduceIte, + toNat_ofNat, Int.ofNat_emod, Int.Nat.cast_ofNat_Int] + norm_cast + apply Nat.mod_eq_of_lt + apply Nat.one_lt_two_pow (by omega) + /-- Prove equality of bitvectors in terms of nat operations. -/ theorem eq_of_toInt_eq {x y : BitVec n} : x.toInt = y.toInt → x = y := by intro eq @@ -3749,7 +3744,7 @@ theorem toInt_twoPow_sub_one : (BitVec.twoPow w (w - 1) - 1#w).toInt = 2 ^ (w - · decide · have : 1 < 2 ^ (w + 1 + 1) := Nat.one_lt_two_pow (by omega) rw_mod_cast [BitVec.twoPow, BitVec.toInt_sub, BitVec.toInt_shiftLeft, BitVec.toNat_ofNat, - Int.bmod_sub_bmod_congr, BitVec.toInt_one (by omega), Nat.shiftLeft_eq, + Int.bmod_sub_bmod_congr, toInt_one_of_lt (by omega), Nat.shiftLeft_eq, Nat.mod_eq_of_lt (by omega), Int.bmod_eq_iff_of_lt_of_lt] simp only [Nat.add_one_sub_one, Nat.one_mul] · have : 0 < (2 ^ (w + 1 + 1 - 1) - 1) * 2 := by simp; omega From 67d5900e5445ef8de1e608771ed4d0860d90d652 Mon Sep 17 00:00:00 2001 From: luisacicolini Date: Mon, 10 Feb 2025 09:30:51 +0000 Subject: [PATCH 16/19] chore: fix theorem name --- src/Init/Data/BitVec/Bitblast.lean | 2 +- src/Init/Data/BitVec/Lemmas.lean | 2 +- src/Init/Data/Int/LemmasAux.lean | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/src/Init/Data/BitVec/Bitblast.lean b/src/Init/Data/BitVec/Bitblast.lean index d4b7153b5e9f..9264d1488f32 100644 --- a/src/Init/Data/BitVec/Bitblast.lean +++ b/src/Init/Data/BitVec/Bitblast.lean @@ -1279,7 +1279,7 @@ theorem smulOverflow_eq {w : Nat} (x y : BitVec w) : have hub : x.toInt * y.toInt * 2 < ((2 ^ ((w + 1) * 2 - 1): Nat) * 2) := Int.mul_lt_mul_of_pos_right (by norm_cast at *; omega) (by omega) rw [BitVec.toInt_signExtend_of_lt (by omega), BitVec.toInt_signExtend_of_lt (by omega), BitVec.toInt_signExtend_of_lt (by omega), BitVec.toInt_signExtend_of_lt (by omega), BitVec.toInt_twoPow_of_eq (by omega), ←Nat.two_pow_pred_add_two_pow_pred (by omega)] - simp only [← Nat.mul_two, Int.bmod_eq_iff_of_lt_of_lt hlb hub, BitVec.toInt_twoPow_sub_one, or_eq_true, decide_eq_true_eq, _root_.eq_iff_iff, and_eq_true] + simp only [← Nat.mul_two, Int.bmod_eq_of_le_of_lt hlb hub, BitVec.toInt_twoPow_sub_one, or_eq_true, decide_eq_true_eq, _root_.eq_iff_iff, and_eq_true] omega /- ### umod -/ diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean index a51488b90380..50558cce891f 100644 --- a/src/Init/Data/BitVec/Lemmas.lean +++ b/src/Init/Data/BitVec/Lemmas.lean @@ -3745,7 +3745,7 @@ theorem toInt_twoPow_sub_one : (BitVec.twoPow w (w - 1) - 1#w).toInt = 2 ^ (w - · have : 1 < 2 ^ (w + 1 + 1) := Nat.one_lt_two_pow (by omega) rw_mod_cast [BitVec.twoPow, BitVec.toInt_sub, BitVec.toInt_shiftLeft, BitVec.toNat_ofNat, Int.bmod_sub_bmod_congr, toInt_one_of_lt (by omega), Nat.shiftLeft_eq, - Nat.mod_eq_of_lt (by omega), Int.bmod_eq_iff_of_lt_of_lt] + Nat.mod_eq_of_lt (by omega), Int.bmod_eq_of_le_of_lt] simp only [Nat.add_one_sub_one, Nat.one_mul] · have : 0 < (2 ^ (w + 1 + 1 - 1) - 1) * 2 := by simp; omega norm_cast diff --git a/src/Init/Data/Int/LemmasAux.lean b/src/Init/Data/Int/LemmasAux.lean index 95e2d74b3846..03d6bc51f554 100644 --- a/src/Init/Data/Int/LemmasAux.lean +++ b/src/Init/Data/Int/LemmasAux.lean @@ -45,7 +45,7 @@ theorem bmod_neg_iff {m : Nat} {x : Int} (h2 : -m ≤ x) (h1 : x < m) : · rw [Int.emod_eq_of_lt xpos (by omega)]; omega · rw [Int.add_emod_self.symm, Int.emod_eq_of_lt (by omega) (by omega)]; omega -theorem bmod_eq_iff_of_lt_of_lt {x : Int} {y : Nat} (hge : -y ≤ x * 2) (hlt : x * 2 < y) : +theorem bmod_eq_of_le_of_lt {x : Int} {y : Nat} (hge : -y ≤ x * 2) (hlt : x * 2 < y) : x.bmod y = x := by simp only [Int.bmod_def] rcases x From 24e9bc92578c91ae9cb66754d27381671139757a Mon Sep 17 00:00:00 2001 From: luisacicolini Date: Mon, 10 Feb 2025 09:31:36 +0000 Subject: [PATCH 17/19] chore: fix theorem name --- src/Init/Data/Int/LemmasAux.lean | 14 +++++++++++++- 1 file changed, 13 insertions(+), 1 deletion(-) diff --git a/src/Init/Data/Int/LemmasAux.lean b/src/Init/Data/Int/LemmasAux.lean index 03d6bc51f554..02c0193ed4d4 100644 --- a/src/Init/Data/Int/LemmasAux.lean +++ b/src/Init/Data/Int/LemmasAux.lean @@ -52,7 +52,19 @@ theorem bmod_eq_of_le_of_lt {x : Int} {y : Nat} (hge : -y ≤ x * 2) (hlt : x * · rw [Int.emod_eq_of_lt (by simp only [ofNat_eq_coe]; omega) (by omega)]; omega · rw [Int.emod_eq_add_self_emod, Int.emod_eq_of_lt (by omega) (by omega)]; omega -theorem mul_le_mul_self {x y : Int} {s : Nat} (lbx : -s ≤ x) (ubx : x < s) (lby : -s ≤ y) (uby : y < s) : +theorem mul_le_mul_self {x y : Int} {s : Nat} (lbx : -s ≤ x) (ubx : x ≤ s) (lby : -s ≤ y) (uby : y < s) : + x * y ≤ s * s := by + have := Nat.mul_pos (n := s) (m := s) (by omega) (by omega) + by_cases hx : 0 < x <;> by_cases hy : 0 < y + · exact Int.mul_le_mul (by omega) (by omega) (by omega) (by omega) + · have : x * y ≤ 0 := Int.mul_nonpos_of_nonneg_of_nonpos (by omega) (by omega); omega + · have : x * y ≤ 0 := Int.mul_nonpos_of_nonpos_of_nonneg (by omega) (by omega); omega + · have : -x * -y ≤ s * s := Int.mul_le_mul (by omega) (by omega) (by omega) (by omega) + simp only [gt_iff_lt, Int.mul_neg, Int.neg_mul, Int.neg_neg] at this + omega + + +theorem mul_le_mul_self' {x y : Int} {s : Nat} (lbx : -s ≤ x) (ubx : x < s) (lby : -s ≤ y) (uby : y < s) : x * y ≤ s * s := by have := Nat.mul_pos (n := s) (m := s) (by omega) (by omega) by_cases hx : 0 < x <;> by_cases hy : 0 < y From 87b1a873ae804c96995dc201debdb655749616f2 Mon Sep 17 00:00:00 2001 From: luisacicolini Date: Mon, 10 Feb 2025 10:36:13 +0000 Subject: [PATCH 18/19] chore: simplify mul_le_mul_self --- src/Init/Data/BitVec/Lemmas.lean | 2 +- src/Init/Data/Int/LemmasAux.lean | 31 ++++++++++--------------------- 2 files changed, 11 insertions(+), 22 deletions(-) diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean index 50558cce891f..08517a885409 100644 --- a/src/Init/Data/BitVec/Lemmas.lean +++ b/src/Init/Data/BitVec/Lemmas.lean @@ -3724,7 +3724,7 @@ theorem toInt_mul_toInt_lt {x y : BitVec w} : x.toInt * y.toInt ≤ 2 ^ (w * 2 - rw [← Nat.pow_add, ←Nat.mul_two, Nat.mul_comm (m := 2) (n := ((w + 1) - 1)), Nat.mul_sub_one, Nat.mul_comm] rw_mod_cast [h] rw [← Nat.two_pow_pred_mul_two (by omega), Int.natCast_mul] at xlt ylt xle yle - exact Int.mul_le_mul_self (by omega) (by omega) (by omega) (by omega) + exact Int.mul_le_mul_self (by omega) (by omega) theorem le_toInt_mul_toInt {x y : BitVec w} : - (2 ^ (w * 2 - 2)) ≤ x.toInt * y.toInt := by rcases w with _|w diff --git a/src/Init/Data/Int/LemmasAux.lean b/src/Init/Data/Int/LemmasAux.lean index 02c0193ed4d4..a55a22617363 100644 --- a/src/Init/Data/Int/LemmasAux.lean +++ b/src/Init/Data/Int/LemmasAux.lean @@ -52,28 +52,17 @@ theorem bmod_eq_of_le_of_lt {x : Int} {y : Nat} (hge : -y ≤ x * 2) (hlt : x * · rw [Int.emod_eq_of_lt (by simp only [ofNat_eq_coe]; omega) (by omega)]; omega · rw [Int.emod_eq_add_self_emod, Int.emod_eq_of_lt (by omega) (by omega)]; omega -theorem mul_le_mul_self {x y : Int} {s : Nat} (lbx : -s ≤ x) (ubx : x ≤ s) (lby : -s ≤ y) (uby : y < s) : +theorem mul_le_mul_self {x y : Int} {s : Nat} (hx : x.natAbs ≤ s) (hy : y.natAbs ≤ s) : x * y ≤ s * s := by - have := Nat.mul_pos (n := s) (m := s) (by omega) (by omega) - by_cases hx : 0 < x <;> by_cases hy : 0 < y - · exact Int.mul_le_mul (by omega) (by omega) (by omega) (by omega) - · have : x * y ≤ 0 := Int.mul_nonpos_of_nonneg_of_nonpos (by omega) (by omega); omega - · have : x * y ≤ 0 := Int.mul_nonpos_of_nonpos_of_nonneg (by omega) (by omega); omega - · have : -x * -y ≤ s * s := Int.mul_le_mul (by omega) (by omega) (by omega) (by omega) - simp only [gt_iff_lt, Int.mul_neg, Int.neg_mul, Int.neg_neg] at this - omega - - -theorem mul_le_mul_self' {x y : Int} {s : Nat} (lbx : -s ≤ x) (ubx : x < s) (lby : -s ≤ y) (uby : y < s) : - x * y ≤ s * s := by - have := Nat.mul_pos (n := s) (m := s) (by omega) (by omega) - by_cases hx : 0 < x <;> by_cases hy : 0 < y - · exact Int.mul_le_mul (by omega) (by omega) (by omega) (by omega) - · have : x * y ≤ 0 := Int.mul_nonpos_of_nonneg_of_nonpos (by omega) (by omega); omega - · have : x * y ≤ 0 := Int.mul_nonpos_of_nonpos_of_nonneg (by omega) (by omega); omega - · have : -x * -y ≤ s * s := Int.mul_le_mul (by omega) (by omega) (by omega) (by omega) - simp only [gt_iff_lt, Int.mul_neg, Int.neg_mul, Int.neg_neg] at this - omega + rcases s with _|s + · simp [show x = 0 by omega] + · have := Nat.mul_pos (n := (s + 1)) (m := (s + 1)) (by omega) (by omega) + by_cases hx : 0 < x <;> by_cases hy : 0 < y + · exact Int.mul_le_mul (by omega) (by omega) (by omega) (by omega) + · have : x * y ≤ 0 := Int.mul_nonpos_of_nonneg_of_nonpos (by omega) (by omega); omega + · have : x * y ≤ 0 := Int.mul_nonpos_of_nonpos_of_nonneg (by omega) (by omega); omega + · have : -x * -y ≤ (s + 1) * (s + 1) := Int.mul_le_mul (by omega) (by omega) (by omega) (by omega) + simp_all theorem neg_mul_self_le_mul {x y : Int} {s : Nat} (lbx : -s ≤ x) (ubx : x < s) (lby : -s ≤ y) (uby : y < s) : -(s * s) ≤ x * y := by From 94a68d45584ffd70b6154012732564df083adfaa Mon Sep 17 00:00:00 2001 From: luisacicolini Date: Tue, 11 Feb 2025 08:41:18 +0000 Subject: [PATCH 19/19] chore: smul correct def --- src/Init/Data/BitVec/Bitblast.lean | 44 ++++++++++++------- src/Init/Data/BitVec/Lemmas.lean | 1 + src/Std/Tactic/BVDecide/Normalize/BitVec.lean | 7 ++- tests/lean/run/bv_decide_rewriter.lean | 5 +++ 4 files changed, 39 insertions(+), 18 deletions(-) diff --git a/src/Init/Data/BitVec/Bitblast.lean b/src/Init/Data/BitVec/Bitblast.lean index 9264d1488f32..655e41b3f39e 100644 --- a/src/Init/Data/BitVec/Bitblast.lean +++ b/src/Init/Data/BitVec/Bitblast.lean @@ -1263,24 +1263,36 @@ theorem umulOverflow_eq {w : Nat} (x y : BitVec w) : have := Nat.pow_lt_pow_of_lt (a := 2) (n := (w' + 1)) (m := (w' + 1) * 2) omega +#print umulOverflow_eq + theorem smulOverflow_eq {w : Nat} (x y : BitVec w) : smulOverflow x y - = (w ≠ 0) || (((BitVec.intMin w).signExtend (w * 2)).sle (x.signExtend (w * 2) * y.signExtend (w * 2)) && - (x.signExtend (w * 2) * y.signExtend (w * 2)).sle ((BitVec.intMax w).signExtend (w * 2))) := by - simp only [smulOverflow] - rcases w with _|w - · decide +revert - · simp only [Bool.false_or, BitVec.intMin, BitVec.intMax, BitVec.sle, BitVec.toInt_mul, - decide_eq_true_eq, BitVec.ofNat_eq_ofNat] - have := Int.pow_lt_pow (a := 2) (b := ((w + 1) * 2 - 2)) (c := ((w + 1) * 2 - 1)) - have := @BitVec.le_toInt_mul_toInt (w + 1) x y - have hlb : -((2 ^ ((w + 1) * 2 - 1) : Nat) * 2) ≤ x.toInt * y.toInt * 2 := by push_cast; omega - have := @BitVec.toInt_mul_toInt_lt (w + 1) x y - have hub : x.toInt * y.toInt * 2 < ((2 ^ ((w + 1) * 2 - 1): Nat) * 2) := Int.mul_lt_mul_of_pos_right (by norm_cast at *; omega) (by omega) - rw [BitVec.toInt_signExtend_of_lt (by omega), BitVec.toInt_signExtend_of_lt (by omega), - BitVec.toInt_signExtend_of_lt (by omega), BitVec.toInt_signExtend_of_lt (by omega), BitVec.toInt_twoPow_of_eq (by omega), ←Nat.two_pow_pred_add_two_pow_pred (by omega)] - simp only [← Nat.mul_two, Int.bmod_eq_of_le_of_lt hlb hub, BitVec.toInt_twoPow_sub_one, or_eq_true, decide_eq_true_eq, _root_.eq_iff_iff, and_eq_true] - omega + = ((w ≠ 0) && + ((signExtend (w * 2) (intMin w)).sle (signExtend (w * 2) x * signExtend (w * 2) y) && + (signExtend (w * 2) x * signExtend (w * 2) y).sle (signExtend (w * 2) (intMax w)))) := by sorry + -- simp only [smulOverflow] + -- rcases w with _|w + -- · simp [of_length_zero, toInt_zero] + -- · simp [Bool.false_or, BitVec.intMin, BitVec.intMax, BitVec.sle, BitVec.toInt_mul, decide_eq_true_eq, BitVec.ofNat_eq_ofNat] + -- have h1 := Int.pow_lt_pow (a := 2) (b := ((w + 1) * 2 - 2)) (c := ((w + 1) * 2 - 1)) + -- have h2 := @BitVec.le_toInt_mul_toInt (w + 1) x y + -- have hlb : -((2 ^ ((w + 1) * 2 - 1) : Nat) * 2) ≤ x.toInt * y.toInt * 2 := by push_cast; omega + -- have h3 := @BitVec.toInt_mul_toInt_lt (w + 1) x y + -- have hub : x.toInt * y.toInt * 2 < ((2 ^ ((w + 1) * 2 - 1): Nat) * 2) := Int.mul_lt_mul_of_pos_right (by norm_cast at *; omega) (by omega) + -- rw [BitVec.toInt_signExtend_of_lt (by omega), BitVec.toInt_signExtend_of_lt (by omega), + -- BitVec.toInt_signExtend_of_lt (by omega), BitVec.toInt_signExtend_of_lt (by omega), BitVec.toInt_twoPow_of_eq (by omega), ←Nat.two_pow_pred_add_two_pow_pred (by omega)] + -- simp only [zero_lt_succ, Nat.mul_pos_iff_of_pos_left, Nat.two_pow_pred_add_two_pow_pred, + -- toInt_sub] + -- rw [← decide_or, ← decide_and] + -- congr 1 + -- simp only [Int.bmod_le] + + + -- simp_all only [Int.Nat.cast_ofNat_Int, ← Nat.mul_two, zero_lt_succ, Nat.mul_pos_iff_of_pos_left, + -- Nat.pow_pred_mul, toInt_sub] + -- sorry + +#print smulOverflow_eq /- ### umod -/ diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean index 08517a885409..0e5790633830 100644 --- a/src/Init/Data/BitVec/Lemmas.lean +++ b/src/Init/Data/BitVec/Lemmas.lean @@ -3964,6 +3964,7 @@ theorem msb_intMin {w : Nat} : (intMin w).msb = decide (0 < w) := by /-! ### intMax -/ + /-- The bitvector of width `w` that has the largest value when interpreted as an integer. -/ def intMax (w : Nat) := (twoPow w (w - 1)) - 1 diff --git a/src/Std/Tactic/BVDecide/Normalize/BitVec.lean b/src/Std/Tactic/BVDecide/Normalize/BitVec.lean index 55adf4e78e51..4cdce5f01f6d 100644 --- a/src/Std/Tactic/BVDecide/Normalize/BitVec.lean +++ b/src/Std/Tactic/BVDecide/Normalize/BitVec.lean @@ -169,6 +169,9 @@ end Constant attribute [bv_normalize] BitVec.zero_and attribute [bv_normalize] BitVec.and_zero +attribute [bv_normalize] BitVec.intMax +attribute [bv_normalize] BitVec.intMin + -- Used in simproc because of - normalization theorem BitVec.ones_and (a : BitVec w) : (-1#w) &&& a = a := by ext @@ -330,11 +333,11 @@ attribute [bv_normalize] BitVec.umod_zero attribute [bv_normalize] BitVec.umod_one attribute [bv_normalize] BitVec.umod_eq_and +attribute [bv_normalize] BitVec.saddOverflow_eq +attribute [bv_normalize] BitVec.uaddOverflow_eq attribute [bv_normalize] BitVec.umulOverflow_eq attribute [bv_normalize] BitVec.smulOverflow_eq -attribute [bv_normalize] BitVec.saddOverflow_eq -attribute [bv_normalize] BitVec.uaddOverflow_eq /-- `x / (BitVec.ofNat n)` where `n = 2^k` is the same as shifting `x` right by `k`. -/ theorem BitVec.udiv_ofNat_eq_of_lt (w : Nat) (x : BitVec w) (n : Nat) (k : Nat) (hk : 2 ^ k = n) (hlt : k < w) : diff --git a/tests/lean/run/bv_decide_rewriter.lean b/tests/lean/run/bv_decide_rewriter.lean index 27fa3164f1d5..eb0520a89ccd 100644 --- a/tests/lean/run/bv_decide_rewriter.lean +++ b/tests/lean/run/bv_decide_rewriter.lean @@ -88,6 +88,11 @@ example (x y : BitVec 16) : BitVec.uaddOverflow x y = (x.setWidth (17) + y.setWi example (x y : BitVec 16) : BitVec.saddOverflow x y = (x.msb = y.msb ∧ ¬(x + y).msb = x.msb) := by bv_normalize example (x y : BitVec w) : BitVec.uaddOverflow x y = (x.setWidth (w + 1) + y.setWidth (w + 1)).msb := by bv_normalize example (x y : BitVec w) : BitVec.saddOverflow x y = (x.msb = y.msb ∧ ¬(x + y).msb = x.msb) := by bv_normalize +example (x y : BitVec 16) : BitVec.umulOverflow x y = (BitVec.twoPow 32 16 ≤ x.zeroExtend (32) * y.zeroExtend (32)) := by bv_normalize +example (x y : BitVec 16) : BitVec.smulOverflow x y = ((BitVec.intMin 16).signExtend (32)).sle (x.signExtend (32) * y.signExtend (32)) && (x.signExtend (32) * y.signExtend (32)).sle ((BitVec.intMax w).signExtend (32)) := by rw [BitVec.smulOverflow_eq]; bv_normalize +example (x y : BitVec w) : BitVec.umulOverflow x y = (0 < w && BitVec.twoPow (w * 2) w ≤ x.zeroExtend (w * 2) * y.zeroExtend (w * 2)) := by bv_normalize +-- example (x y : BitVec w) : BitVec.smulOverflow x y = (w ≠ 0) || (((BitVec.intMin w).signExtend (w * 2)).sle (x.signExtend (w * 2) * y.signExtend (w * 2)) && +-- (x.signExtend (w * 2) * y.signExtend (w * 2)).sle ((BitVec.intMax w).signExtend (w * 2))) := by bv_normalize -- not_neg