diff --git a/src/Init/Data/BitVec/Bitblast.lean b/src/Init/Data/BitVec/Bitblast.lean index 8bb8517ad7..02e6ec3ab1 100644 --- a/src/Init/Data/BitVec/Bitblast.lean +++ b/src/Init/Data/BitVec/Bitblast.lean @@ -1752,6 +1752,116 @@ theorem toInt_srem (x y : BitVec w) : (x.srem y).toInt = x.toInt.tmod y.toInt := ((not_congr neg_eq_zero_iff).mpr hyz)] exact neg_le_intMin_of_msb_eq_true h' +@[simp] +theorem msb_intMin_umod_neg_of_msb_true {y : BitVec w} (hy : y.msb = true) : + (intMin w % -y).msb = false := by + by_cases hyintmin : y = intMin w + · simp [hyintmin] + · rw [msb_umod_of_msb_false_of_ne_zero (by simp [hyintmin, hy])] + simp [hy] + +@[simp] +theorem msb_neg_umod_neg_of_msb_true_of_msb_true {x y : BitVec w} (hx : x.msb = true) (hy : y.msb = true) : + (-x % -y).msb = false := by + by_cases hx' : x = intMin w + · simp only [hx', neg_intMin, msb_intMin_umod_neg_of_msb_true hy] + · simp [show (-x).msb = false by simp [hx, hx']] + +theorem toInt_dvd_toInt_iff {x y : BitVec w} : + y.toInt ∣ x.toInt ↔ (if x.msb then -x else x) % (if y.msb then -y else y) = 0#w := by + constructor + <;> by_cases hxmsb : x.msb <;> by_cases hymsb: y.msb + <;> intros h + <;> simp only [hxmsb, hymsb, reduceIte, false_eq_true, toNat_eq, toNat_umod, toNat_ofNat, + zero_mod, toInt_eq_neg_toNat_neg_of_msb_true, Int.dvd_neg, Int.neg_dvd, + toInt_eq_toNat_of_msb] at h + <;> simp only [hxmsb, hymsb, toInt_eq_neg_toNat_neg_of_msb_true, toInt_eq_toNat_of_msb, + Int.dvd_neg, Int.neg_dvd, toNat_eq, toNat_umod, reduceIte, toNat_ofNat, zero_mod] + <;> norm_cast + <;> norm_cast at h + <;> simp only [dvd_of_mod_eq_zero, h, dvd_iff_mod_eq_zero.mp, reduceIte] + +theorem toInt_dvd_toInt_iff_of_msb_true_msb_false {x y : BitVec w} (hx : x.msb = true) (hy : y.msb = false) : + y.toInt ∣ x.toInt ↔ (-x) % y = 0#w := by + simpa [hx, hy] using toInt_dvd_toInt_iff (x := x) (y := y) + +theorem toInt_dvd_toInt_iff_of_msb_false_msb_true {x y : BitVec w} (hx : x.msb = false) (hy : y.msb = true) : + y.toInt ∣ x.toInt ↔ x % (-y) = 0#w := by + simpa [hx, hy] using toInt_dvd_toInt_iff (x := x) (y := y) + +@[simp] +theorem neg_toInt_neg_umod_eq_of_msb_true_msb_true {x y : BitVec w} (hx : x.msb = true) (hy : y.msb = true) : + -(-(-x % -y)).toInt = (-x % -y).toNat := by + rw [neg_toInt_neg] + by_cases h : -x % -y = 0#w + · simp [h] + · rw [msb_neg_umod_neg_of_msb_true_of_msb_true hx hy] + +@[simp] +theorem toInt_umod_neg_add {x y : BitVec w} (hymsb : y.msb = true) (hxmsb : x.msb = false) (hdvd : ¬y.toInt ∣ x.toInt) : + (x % -y + y).toInt = x.toInt % y.toInt + y.toInt := by + rcases w with _|w ; simp [of_length_zero] + have hypos : 0 < y.toNat := toNat_pos_of_ne_zero (by simp [hymsb]) + have hxnonneg := toInt_nonneg_of_msb_false hxmsb + have hynonpos := toInt_neg_of_msb_true hymsb + have hylt : (-y).toNat ≤ 2 ^ (w) := toNat_neg_lt_of_msb y hymsb + have hmodlt := Nat.mod_lt x.toNat (y := (-y).toNat) + (by rw [toNat_neg, Nat.mod_eq_of_lt (by omega)]; omega) + simp only [hdvd, reduceIte, toInt_add, hxnonneg, show ¬0 ≤ y.toInt by omega] + rw [toInt_umod, toInt_eq_neg_toNat_neg_of_msb_true hymsb, Int.bmod_add_bmod, + Int.bmod_eq_of_le (by omega) (by omega), + toInt_eq_toNat_of_msb hxmsb, Int.emod_neg] + +@[simp] +theorem toInt_sub_neg_umod {x y : BitVec w} (hxmsb : x.msb = true) (hymsb : y.msb = false) (hdvd : ¬y.toInt ∣ x.toInt) : + (y - -x % y).toInt = x.toInt % y.toInt := by + rcases w with _|w + · simp [of_length_zero] + · have : y.toNat < 2 ^ w := toNat_lt_of_msb_false hymsb + by_cases hyzero : y = 0#(w+1) + · subst hyzero; simp + · simp only [toNat_eq, toNat_ofNat, zero_mod] at hyzero + have hypos : 0 < y.toNat := by omega + simp only [reduceIte, toInt_sub, toInt_eq_toNat_of_msb hymsb, toInt_umod, + Int.sub_bmod_bmod, toInt_eq_neg_toNat_neg_of_msb_true hxmsb, Int.neg_emod] + have hmodlt := Nat.mod_lt (x := (-x).toNat) (y := y.toNat) hypos + rw [Int.bmod_eq_of_le (by omega) (by omega)] + simp only [toInt_eq_toNat_of_msb hymsb, BitVec.toInt_eq_neg_toNat_neg_of_msb_true hxmsb, + Int.dvd_neg] at hdvd + simp only [hdvd, ↓reduceIte, Int.natAbs_cast] + +theorem toInt_smod {x y : BitVec w} : + (x.smod y).toInt = x.toInt.fmod y.toInt := by + rcases w with _|w + · decide +revert + · by_cases hyzero : y = 0#(w + 1) + · simp [hyzero] + · rw [smod_eq] + cases hxmsb : x.msb <;> cases hymsb : y.msb + <;> simp only [umod_eq] + · have : 0 < y.toNat := by simp [toNat_eq] at hyzero; omega + have : y.toNat < 2 ^ w := toNat_lt_of_msb_false hymsb + have : x.toNat % y.toNat < y.toNat := Nat.mod_lt x.toNat (by omega) + rw [toInt_umod, Int.fmod_eq_emod_of_nonneg x.toInt (toInt_nonneg_of_msb_false hymsb), + toInt_eq_toNat_of_msb hxmsb, toInt_eq_toNat_of_msb hymsb, + Int.bmod_eq_of_le_mul_two (by omega) (by omega)] + · have := toInt_dvd_toInt_iff_of_msb_false_msb_true hxmsb hymsb + by_cases hx_dvd_y : y.toInt ∣ x.toInt + · simp [show x % -y = 0#(w + 1) by simp_all, hx_dvd_y, Int.fmod_eq_zero_of_dvd] + · have hynonpos := toInt_neg_of_msb_true hymsb + simp only [show ¬x % -y = 0#(w + 1) by simp_all, ↓reduceIte, + toInt_umod_neg_add hymsb hxmsb hx_dvd_y, Int.fmod_eq_emod, show ¬0 ≤ y.toInt by omega, + hx_dvd_y, _root_.or_self] + · have hynonneg := toInt_nonneg_of_msb_false hymsb + rw [Int.fmod_eq_emod_of_nonneg x.toInt (b := y.toInt) (by omega)] + have hdvd := toInt_dvd_toInt_iff_of_msb_true_msb_false hxmsb hymsb + by_cases hx_dvd_y : y.toInt ∣ x.toInt + · simp [show -x % y = 0#(w + 1) by simp_all, hx_dvd_y, Int.emod_eq_zero_of_dvd] + · simp [show ¬-x % y = 0#(w + 1) by simp_all, toInt_sub_neg_umod hxmsb hymsb hx_dvd_y] + · rw [←Int.neg_inj, neg_toInt_neg_umod_eq_of_msb_true_msb_true hxmsb hymsb] + simp [BitVec.toInt_eq_neg_toNat_neg_of_msb_true, hxmsb, hymsb, + Int.fmod_eq_emod_of_nonneg _, show 0 ≤ (-y).toNat by omega] + /-! ### Lemmas that use bit blasting circuits -/ theorem add_sub_comm {x y : BitVec w} : x + y - z = x - z + y := by diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean index 88aa462677..5b167259e6 100644 --- a/src/Init/Data/BitVec/Lemmas.lean +++ b/src/Init/Data/BitVec/Lemmas.lean @@ -3995,6 +3995,15 @@ theorem pos_of_msb {x : BitVec w} (hx : x.msb = true) : 0#w < x := by rw [BitVec.not_lt, le_zero_iff] at h simp [h] at hx +@[simp] +theorem lt_of_msb_false_of_msb_true {x y : BitVec w} (hx : x.msb = false) (hy : y.msb = true) : + x < y := by + simp only [LT.lt] + have := toNat_ge_of_msb_true hy + have := toNat_lt_of_msb_false hx + simp + omega + /-! ### udiv -/ theorem udiv_def {x y : BitVec n} : x / y = BitVec.ofNat n (x.toNat / y.toNat) := by @@ -4176,6 +4185,14 @@ theorem toInt_umod_of_msb {x y : BitVec w} (h : x.msb = false) : (x % y).toInt = x.toInt % y.toNat := by simp [toInt_eq_msb_cond, h] +@[simp] +theorem msb_umod_of_msb_false_of_ne_zero {x y : BitVec w} (hmsb : y.msb = false) (h_ne_zero : y ≠ 0#w) : + (x % y).msb = false := by + simp only [msb_umod, Bool.and_eq_false_imp, Bool.or_eq_false_iff, beq_eq_false_iff_ne, + ne_eq, h_ne_zero] + intro h + simp [BitVec.le_of_lt, lt_of_msb_false_of_msb_true hmsb h] + /-! ### smtUDiv -/ theorem smtUDiv_eq (x y : BitVec w) : smtUDiv x y = if y = 0#w then allOnes w else x / y := by @@ -5410,6 +5427,27 @@ theorem neg_ofNat_eq_ofInt_neg {w : Nat} {x : Nat} : apply BitVec.eq_of_toInt_eq simp [BitVec.toInt_neg, BitVec.toInt_ofNat] +@[simp] +theorem neg_toInt_neg {x : BitVec w} (h : x.msb = false) : + -(-x).toInt = x.toNat := by + simp [toInt_neg_eq_of_msb h, toInt_eq_toNat_of_msb, h] + +theorem toNat_pos_of_ne_zero {x : BitVec w} (hx : x ≠ 0#w) : + 0 < x.toNat := by + simp [toNat_eq] at hx; omega + +theorem toNat_neg_lt_of_msb (x : BitVec w) (hmsb : x.msb = true) : + (-x).toNat ≤ 2^(w-1) := by + rcases w with _|w + · simp [BitVec.eq_nil x] + · by_cases hx : x = 0#(w + 1) + · simp [hx] + · have := BitVec.le_toNat_of_msb_true hmsb + have := toNat_pos_of_ne_zero hx + rw [toNat_neg, Nat.mod_eq_of_lt (by omega), ← Nat.two_pow_pred_add_two_pow_pred (by omega), + ← Nat.two_mul] + omega + /-! ### abs -/ theorem abs_eq (x : BitVec w) : x.abs = if x.msb then -x else x := rfl