From ecd0fc6ce7f17e5311849502f7e6aa2d9817a6a8 Mon Sep 17 00:00:00 2001 From: Tobias Grosser Date: Sat, 26 Oct 2024 15:37:01 -0700 Subject: [PATCH] feat: BitVec.[udiv_twoPow|sdiv_twoPow] --- src/Init/Data/BitVec/Lemmas.lean | 133 +++++++++++++++++++++++++++++-- src/Init/Data/Nat/Lemmas.lean | 25 ++++++ src/Init/Data/Nat/Mod.lean | 11 +++ 3 files changed, 163 insertions(+), 6 deletions(-) diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean index 9f35e7b4a381..b33906bf9930 100644 --- a/src/Init/Data/BitVec/Lemmas.lean +++ b/src/Init/Data/BitVec/Lemmas.lean @@ -2152,8 +2152,11 @@ instance : Std.LawfulCommIdentity (fun (x y : BitVec w) => x * y) (1#w) where @[simp] theorem BitVec.mul_zero {x : BitVec w} : x * 0#w = 0#w := by - apply eq_of_toNat_eq - simp [toNat_mul] + simp [bv_toNat] + +@[simp] +theorem BitVec.zero_mul {x : BitVec w} : 0#w * x = 0#w := by + simp [bv_toNat] theorem BitVec.mul_add {x y z : BitVec w} : x * (y + z) = x * y + x * z := by @@ -2640,6 +2643,8 @@ theorem getElem_rotateRight {x : BitVec w} {r i : Nat} (h : i < w) : /- ## twoPow -/ +#check Nat.two_pow_pred_mod_two_pow + @[simp, bv_toNat] theorem toNat_twoPow (w : Nat) (i : Nat) : (twoPow w i).toNat = 2^i % 2^w := by rcases w with rfl | w @@ -2681,11 +2686,10 @@ theorem getMsbD_twoPow {i j w: Nat} : @[simp] theorem msb_twoPow {i w: Nat} : - (twoPow w i).msb = (decide (i < w) && decide (i = w - 1)) := by - simp only [BitVec.msb, getMsbD_eq_getLsbD, Nat.sub_zero, getLsbD_twoPow, + (BitVec.twoPow w i).msb = decide (i + 1 = w) := by + simp only [BitVec.msb, BitVec.getMsbD_eq_getLsbD, Nat.sub_zero, BitVec.getLsbD_twoPow, Bool.and_iff_right_iff_imp, Bool.and_eq_true, decide_eq_true_eq, and_imp] - intros - omega + by_cases h : i + 1 = w <;> simp [h] <;> omega theorem and_twoPow (x : BitVec w) (i : Nat) : x &&& (twoPow w i) = if x.getLsbD i then twoPow w i else 0#w := by @@ -3035,6 +3039,123 @@ instance instDecidableExistsBitVec : have := instDecidableExistsBitVec n inferInstance +theorem div_twoPow_div_twoPow_eq_mul {n m : Nat} (x : BitVec w) : + x / (BitVec.twoPow w n) / (BitVec.twoPow w m) = + x / ((BitVec.twoPow w n) * (BitVec.twoPow w m)) := by + simp only [BitVec.toNat_eq, BitVec.toNat_udiv, BitVec.toNat_twoPow, BitVec.toNat_mul, + Nat.mul_mod_mod, Nat.mod_mul_mod] + by_cases hzz : x = 0 + · subst hzz + simp + · by_cases h : n + m < w + · + have hl : 2^n * 2^m < 2^w := by + rw [← Nat.pow_add] + have asdd := (@Nat.pow_lt_pow_iff_right 2 (n + m) w (by omega)).mpr h + apply asdd + simp [Nat.mod_eq_of_lt hl] + have := @Nat.mul_lt_mul_of_le_of_lt + have := @Nat.mul_lt_mul_right (2 ^ n) (2 ^ m) (2 ^ w) (by apply Nat.two_pow_pos) + have := @Nat.lt_of_mul_lt (2^n) (2^m) (2^w) (by apply Nat.two_pow_pos) h + rw [Nat.mul_comm] at hl + have := @Nat.lt_of_mul_lt (2^m) (2^n) (2^w) (by apply Nat.two_pow_pos) h + have : 2 ^ m < 2 ^ w := by omega + simp [Nat.mod_eq_of_lt, *] + rw [Nat.div_div_eq_div_mul] + · + rw [←Nat.pow_add] + rw [Nat.two_pow_mod_two_pow_iff (by omega)] + rw [Nat.two_pow_mod_two_pow_iff (by omega)] + rw [Nat.two_pow_mod_two_pow_iff (by omega)] + simp [h] + by_cases h₄ : n < w + · by_cases h₅ : m < w + · simp [h₄, h₅] + simp at h + rw [Nat.div_div_eq_div_mul] + rw [←Nat.pow_add] + rw [Nat.div_eq_zero_iff] + have xzero := BitVec.isLt x + simp [bv_toNat] at hzz + have := @Nat.pow_pos 2 w (by omega) + have : 2 ^ w ≤ 2 ^ (n + m) := by + apply Nat.pow_le_pow_of_le (by omega) h + omega + have := @Nat.pow_pos 2 (n + m) (by omega) + omega + · simp [h₄, h₅] + · by_cases h₅ : m < w + · simp [h₄, h₅] + · simp [h₄, h₅] + +theorem udiv_twoPow {n : Nat} {x : BitVec w} : + x / (BitVec.twoPow w n) = x >>> n := by + simp only [BitVec.toNat_eq, BitVec.toNat_ushiftRight, Nat.shiftRight_eq_div_pow, + BitVec.toNat_udiv, BitVec.toNat_twoPow] + by_cases h : n < w + · rw [Nat.mod_eq_of_lt ((Nat.pow_lt_pow_iff_right (by omega)).mpr h)] + · by_cases hh : x.toNat = 0 + · simp [hh] + · have : 2 ^ w ≤ 2 ^ n := (Nat.pow_le_pow_iff_right (by omega)).mpr (by omega) + rw [(@Nat.div_eq_zero_iff (2 ^ n) x.toNat (by omega)).mpr (by omega), + Nat.mod_eq_zero_of_dvd, Nat.div_zero] + apply Nat.pow_dvd_pow 2 (by omega) + +theorem neg_twoPow' {i w: Nat} : + (BitVec.twoPow w i).neg = (BitVec.twoPow w i) := by + simp [bv_toNat] + rw [Nat.two_pow_mod_two_pow_iff (by omega)] + by_cases h : i < w + · simp [h] + · simp [h] + + + + + + sorry + + +theorem sdiv_twoPow {n : Nat} {x : BitVec w} : + x.sdiv (BitVec.twoPow w n) = x.sshiftRight n := by + by_cases h : x.msb + · + simp only [BitVec.sdiv_eq, msb_twoPow, BitVec.udiv_eq] + by_cases hh : n + 1 = w + · + simp [hh, h] + + sorry + · + simp [hh, h] + rw [BitVec.sshiftRight_eq_of_msb_true h] + simp [bv_toNat] + rw [Nat.two_pow_mod_two_pow_iff (by omega)] + have al : n < w := by sorry + simp [al] + + + simp [hh] + sorry + · + simp only [BitVec.sdiv_eq, msb_twoPow, BitVec.udiv_eq] + by_cases hh : n + 1 = w + · simp [hh, h] + simp at h + rw [BitVec.sshiftRight_eq_of_msb_false h] + simp only [toNat_eq, toNat_neg, toNat_udiv, toNat_twoPow, toNat_ushiftRight] + rw [Nat.shiftRight_eq_div_pow] + + + + + sorry + · simp only [h, hh, decide_False] + simp only [Bool.not_eq_true] at h + rw [BitVec.sshiftRight_eq_of_msb_false h] + rw [udiv_twoPow] + + /-! ### Deprecations -/ set_option linter.missingDocs false diff --git a/src/Init/Data/Nat/Lemmas.lean b/src/Init/Data/Nat/Lemmas.lean index 0aa6a9ae9e72..0fd972cc580c 100644 --- a/src/Init/Data/Nat/Lemmas.lean +++ b/src/Init/Data/Nat/Lemmas.lean @@ -549,6 +549,12 @@ protected theorem mul_left_cancel_iff {n : Nat} (p : 0 < n) {m k : Nat} : n * m protected theorem mul_right_cancel_iff {m : Nat} (p : 0 < m) {n k : Nat} : n * m = k * m ↔ n = k := ⟨Nat.mul_right_cancel p, fun | rfl => rfl⟩ +protected theorem mul_left_inj (ha : a ≠ 0) : b * a = c * a ↔ b = c := + Nat.mul_right_cancel_iff (Nat.pos_iff_ne_zero.2 ha) + +protected theorem mul_right_inj (ha : a ≠ 0) : a * b = a * c ↔ b = c := + Nat.mul_left_cancel_iff (Nat.pos_iff_ne_zero.2 ha) + protected theorem ne_zero_of_mul_ne_zero_right (h : n * m ≠ 0) : m ≠ 0 := (Nat.mul_ne_zero_iff.1 h).2 @@ -664,6 +670,9 @@ theorem mul_mod (a b n : Nat) : a * b % n = (a % n) * (b % n) % n := by @[simp] theorem add_mod_mod (m n k : Nat) : (m + n % k) % k = (m + n) % k := by rw [Nat.add_comm, mod_add_mod, Nat.add_comm] +@[simp] theorem mul_mod_mod (a b c : Nat) : (a * (b % c)) % c = a * b % c := by + rw [mul_mod, mod_mod, ← mul_mod] + theorem add_mod (a b n : Nat) : (a + b) % n = ((a % n) + (b % n)) % n := by rw [add_mod_mod, mod_add_mod] @@ -894,6 +903,11 @@ protected theorem div_eq_iff_eq_mul_left {a b c : Nat} (H : 0 < b) (H' : b ∣ a a / b = c ↔ a = c * b := by rw [Nat.mul_comm]; exact Nat.div_eq_iff_eq_mul_right H H' +protected theorem div_eq_zero_iff (hb : 0 < b) : a / b = 0 ↔ a < b where + mp h := by rw [← mod_add_div a b, h, Nat.mul_zero, Nat.add_zero]; exact mod_lt _ hb + mpr h := by rw [← Nat.mul_right_inj (Nat.ne_of_gt hb), ← Nat.add_left_cancel_iff, mod_add_div, + mod_eq_of_lt h, Nat.mul_zero, Nat.add_zero] + theorem pow_dvd_pow_iff_pow_le_pow {k l : Nat} : ∀ {x : Nat}, 0 < x → (x ^ k ∣ x ^ l ↔ x ^ k ≤ x ^ l) | x + 1, w => by @@ -923,6 +937,17 @@ protected theorem pow_dvd_pow {m n : Nat} (a : Nat) (h : m ≤ n) : a ^ m ∣ a rw [Nat.pow_add] apply Nat.dvd_mul_right +protected theorem two_pow_mod_two_pow_iff {b m n : Nat} (h : 1 < b): + (b ^ n % b ^ m) = if n < m then b ^ n else 0 := by + by_cases h : n < m + · simp only [h, ↓reduceIte] + apply Nat.mod_eq_of_lt + apply Nat.pow_lt_pow_of_lt (by omega) h + · simp only [h, ↓reduceIte] + simp only [Nat.not_lt] at h + apply Nat.mod_eq_zero_of_dvd + apply Nat.pow_dvd_pow b (by omega) + protected theorem pow_sub_mul_pow (a : Nat) {m n : Nat} (h : m ≤ n) : a ^ (n - m) * a ^ m = a ^ n := by rw [← Nat.pow_add, Nat.sub_add_cancel h] diff --git a/src/Init/Data/Nat/Mod.lean b/src/Init/Data/Nat/Mod.lean index 2ef6691913aa..3ced86c318dc 100644 --- a/src/Init/Data/Nat/Mod.lean +++ b/src/Init/Data/Nat/Mod.lean @@ -21,6 +21,17 @@ which should probably be moved to their own file. namespace Nat +protected theorem lt_of_mul_lt {a b c : Nat} (h : 0 < b) (h₂ : a * b < c) : a < c := by + induction a generalizing c + case zero => + simp only [Nat.zero_mul] at h₂ + simp [h₂] + case succ i ih => + simp only [Nat.add_mul, Nat.one_mul] at h₂ + apply Nat.add_lt_of_lt_sub + apply ih + omega + @[simp] protected theorem mul_lt_mul_left (a0 : 0 < a) : a * b < a * c ↔ b < c := by induction a with | zero => simp_all