From 246e351f66ddbaf0ec8913b3302305e68a98f8d3 Mon Sep 17 00:00:00 2001 From: Tobias Grosser Date: Sun, 27 Oct 2024 05:18:36 -0700 Subject: [PATCH] more wip --- src/Init/Data/BitVec/Lemmas.lean | 307 +++++++++++++++++++++++++++---- 1 file changed, 274 insertions(+), 33 deletions(-) diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean index b33906bf9930..b7e8ceb3c36e 100644 --- a/src/Init/Data/BitVec/Lemmas.lean +++ b/src/Init/Data/BitVec/Lemmas.lean @@ -3101,61 +3101,302 @@ theorem udiv_twoPow {n : Nat} {x : BitVec w} : 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 +theorem aaas (x y : BitVec w) : -(x / -y) = x / y := by simp [bv_toNat] + by_cases h : y = 0 + · subst h + simp + · rw [Nat.mod_eq_of_lt (a := 2 ^ w - y.toNat)] + · rw [Nat.mul_div_mul_left] + + sorry + · have := isLt y + simp only [ofNat_eq_ofNat, toNat_eq, toNat_ofNat, Nat.zero_mod] at h + omega + +theorem twoPow_large (h : i ≥ w): (twoPow w i) = 0#w := by + simp only [toNat_eq, toNat_twoPow, toNat_ofNat, Nat.zero_mod] rw [Nat.two_pow_mod_two_pow_iff (by omega)] - by_cases h : i < w - · simp [h] - · simp [h] + simp [h] + omega +theorem twoPow_neg_large : (-(twoPow (w+1) (w))) = twoPow (w+1) w := by + simp [toNat_eq, toNat_twoPow, toNat_ofNat, Nat.zero_mod] + rw [Nat.two_pow_mod_two_pow_iff (by omega)] + have h : ¬ (w + 1 < w) := by omega + simp [h] + have le := @Nat.two_pow_sub_two_pow_pred (w+1) (by omega) + simp at le + apply le +def testaa : Bool := Id.run do + for xv in [0, 1, 2, 3, 4, 5, 6, 7, 8] do + for w in [1, 2, 3, 4] do + for n in [0, 1, 2, 3, 4, 5] do + let x := BitVec.ofNat w xv + if x.sdiv (BitVec.twoPow w n) ≠ (if n +1 < w then x.sshiftRight n else if n + 1 = w then 1#w else 0#w) then + return False + return True +#eval testaa +#eval (8#4).sdiv (8#4) +theorem udiv_eq_one {x y : BitVec w} : x / y = 1#w := by + simp [bv_toNat] + rw [Nat.div_] sorry +theorem sdiv_twoPow' {n : Nat} {x : BitVec w} (hmsb : x.msb = false) (hn : ¬ (n + 1 = w)) : + x.sdiv (BitVec.twoPow w n) = x.sshiftRight n := by + simp only [BitVec.sdiv_eq, msb_twoPow, BitVec.udiv_eq] + simp only [hmsb, hn, decide_False] + rw [BitVec.sshiftRight_eq_of_msb_false hmsb] + rw [udiv_twoPow] -theorem sdiv_twoPow {n : Nat} {x : BitVec w} : +/- +0x0#4 +-/ +#eval (7#4).sshiftRight 3 +/- +0x8#4 +-/ +#eval (twoPow 4 3) +/- +0x0#4 +-/ +#eval (7#4).sdiv (twoPow 4 3) + +theorem ushiftRight_eq_zero {x : BitVec w} {n : Nat} (h : n ≥ w) : + x >>> n = 0#w := by + simp [bv_toNat] + rw [Nat.shiftRight_eq_div_pow] + rw [Nat.div_eq] + have rt := isLt x + have re := @Nat.pow_le_pow_of_le 2 w n (by omega) (by omega) + by_cases h₂ : 0 < 2 ^ n ∧ 2 ^ n ≤ x.toNat + · omega + · simp [h₂] + +theorem ushiftRight_eq_zero_of_msb_false {x : BitVec w} {n : Nat} (h : n + 1 = w) (h₂ : x.msb = false) : + x >>> n = 0#w := by + simp [bv_toNat] + rw [Nat.shiftRight_eq_div_pow] + rw [Nat.div_eq] + have rt := isLt x + have re := @Nat.pow_le_pow_of_le 2 w (n+1) (by omega) (by omega) + by_cases h₃ : 0 < 2 ^ n ∧ 2 ^ n ≤ x.toNat + · simp [h₃] + have sr := (@BitVec.msb_eq_false_iff_two_mul_lt w x).mp h₂ + omega + · simp [h₃] + + +theorem sdiv_twoPow₂ {n : Nat} {x : BitVec w} (hmsb : x.msb = false) (hn : n + 1 = 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] + simp only [BitVec.sdiv_eq, msb_twoPow, BitVec.udiv_eq] + simp only [hmsb, hn, decide_True] + rw [BitVec.sshiftRight_eq_of_msb_false hmsb] + symm at hn + subst hn + rw [twoPow_neg_large] + rw [udiv_twoPow] + rw [ushiftRight_eq_zero_of_msb_false] + simp + simp + simp [hmsb] + +theorem sdiv_twoPow_of_msb_true {n : Nat} {x : BitVec w} (h : x.msb = true) (h2 : n + 1 = w) (h3 : 2 ^ n = x.toNat) : + x.sdiv (BitVec.twoPow w n) = 1#w := by + by_cases hw : w = 0 + · subst hw + simp [twoPow] + · have re : 0 < w := by omega + simp [BitVec.sdiv] + simp [*, bv_toNat] + rw [Nat.div_self] + by_cases hy : x.toNat = 0 + · have lr := @Nat.pow_pos 2 n (by omega) + omega + · rw [Nat.mod_eq_of_lt] + omega + omega - sorry +theorem sdiv_twoPow_of_msb_true' {n : Nat} {x : BitVec w} (h : x.msb = true) (h2 : n + 1 = w) (h3 : 2 ^ n > x.toNat) : + x.sdiv (BitVec.twoPow w n) = 1#w := by + by_cases hw : w = 0 + · subst hw + simp [twoPow] + · have re : 0 < w := by omega + simp [BitVec.sdiv] + simp [*, bv_toNat] + have lr := @Nat.pow_pos 2 n (by omega) + have lr := @Nat.pow_pos 2 w (by omega) + symm at h2 + subst h2 + by_cases hy : x.toNat = 0 + · have le := (@BitVec.msb_eq_true_iff_two_mul_ge (n+1) x).mp h + rw [Nat.mul_comm] at le + rw [Nat.mul_two] at le + omega · - 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] + rw [Nat.mod_eq_of_lt (by omega)] + have tl := @Nat.two_pow_pred_mod_two_pow (n + 1) (by omega) + simp at tl + rw [tl] + have tl := @Nat.two_pow_sub_two_pow_pred (n + 1) (by omega) + simp at tl + rw [tl] + have tl := @Nat.two_pow_pred_mod_two_pow (n + 1) (by omega) + simp at tl + rw [tl] + rw [Nat.div_eq_zero_iff] + rw [Nat.div_eq] + simp [*] + + Omega + +theorem xxr {x : BitVec w} (h : x.msb = false) : - (x >>> 1) = (-x).sshiftRight 1 := by + ext + rw [getLsbD_sshiftRight] + rw [getLsbD_neg] + rw [getLsbD_ushiftRight] - 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] + induction w + case zero => + simp [BitVec.eq_nil x] + case succ i ih => + + + + sorry + +theorem sdiv_twoPow_msb {n : Nat} {x : BitVec w} (h : x.msb = true) (h2 : n +1 < w) : + x.sdiv (BitVec.twoPow w n) = x.sshiftRight n := by + simp [sdiv] + have rr : ¬ (n + 1 = w) := by omega + simp [*] + rw [udiv_twoPow] + induction n + · simp + case succ i ih => + have hr := @ih (by omega) (by omega) + rw [sshiftRight_add] + rw [← hr] + rw [shiftRight_add] + congr + rw [xxr] + have rr : (-x).msb = false := by + sorry + have rr2 : ((-x) >>> i).msb = false := by 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] + simp [rr2] +theorem sdiv_twoPow {n : Nat} {x : BitVec w} : + x.sdiv (BitVec.twoPow w n) = if x.msb = false ∨ n < w then x.sshiftRight n else 0#w := by + by_cases hhh : x.msb = false + · by_cases hr : n + 1 = w + · simp [hhh] + rw [sdiv_twoPow₂ hhh hr] + · simp [hhh] + rw [sdiv_twoPow' hhh hr] + · simp [hhh] + by_cases ha : n ≥ w + · simp [show ¬ (n < w) by omega] + rw [twoPow_large ha] + simp + · by_cases hrr : n + 1 < w + · + simp [show (n < w) by omega] + rw [sdiv_twoPow_msb] + simp at hhh + simp [hhh] + omega + · simp_all + have lr : w = n + 1 := by omega + subst lr + clear ha hrr + sorry + +theorem sdiv_twoPow''' {n : Nat} {x : BitVec w} : + x.sdiv (BitVec.twoPow w n) = if n + 1 < w then x.sshiftRight n else if n + 1 = w then 1#w else 0#w := by + by_cases hb : n + 1 = w + · simp [hb] + by_cases ha : n ≥ w + · sorry + · simp_all + have : w = n + 1 := by omega + subst this + rw [BitVec.sdiv] + by_cases hhh : x.msb + · simp [hhh, bv_toNat] + have := @Nat.two_pow_pred_mod_two_pow (n+1) (by omega) + simp at this + rw [this] + have := @Nat.two_pow_sub_two_pow_pred (n+1) (by omega) + simp at this + rw [this] + have := @Nat.two_pow_pred_mod_two_pow (n+1) (by omega) + simp at this + rw [this] + have el := (@BitVec.msb_eq_true_iff_two_mul_ge (n+1) x).mp hhh + rw [Nat.mul_comm] at el + rw [Nat.mul_two] at el + have lr := @Nat.two_pow_pred_add_two_pow_pred (n+1) (by omega) + simp at lr + symm at lr + rw [← Nat.mul_two] at lr + rw [← Nat.mul_two] at el + rw [lr] at el + simp at el + by_cases rt : 2 ^ n = x.toNat + · symm at rt + rw [rt] + have as := @Nat.two_pow_sub_two_pow_pred (n+1) (by omega) + simp at as + rw [as] + have aadd := @Nat.two_pow_pred_mod_two_pow (n+1) (by omega) + simp at aadd + rw [aadd] + rw [Nat.div_self] + apply Nat.pow_pos + omega + + · have ar : 2 ^ n < x.toNat := by omega + by_cases rl : x.toNat = 2^(n+1) + · + simp [rl] + · + rw [Nat.mod_eq_of_lt (by omega)] + rw [Nat.div_eq_zero_iff (by omega)] + have := @Nat.two_pow_pred_add_two_pow_pred (n+1) (by omega) + simp at this + rw [←this] + simp + omega + + · simp [hhh, bv_toNat] + have := @Nat.two_pow_pred_mod_two_pow (n+1) (by omega) + simp at this + rw [this] + have := @Nat.two_pow_sub_two_pow_pred (n+1) (by omega) + simp at this + rw [this] + have := @Nat.two_pow_pred_mod_two_pow (n+1) (by omega) + simp at this + rw [this] + rw [Nat.div_eq_zero_iff] + simp at hhh + · have el := (@BitVec.msb_eq_false_iff_two_mul_lt (n+1) x).mp hhh + omega + · apply Nat.two_pow_pos + /-! ### Deprecations -/ set_option linter.missingDocs false