From a7308e5530fec9ae06cf3dccc75db34eaa2a02c7 Mon Sep 17 00:00:00 2001 From: luisacicolini Date: Sat, 26 Oct 2024 14:01:11 +0100 Subject: [PATCH 1/2] msb-getmsbd-twopow --- src/Init/Data/BitVec/Lemmas.lean | 15 +++++++++++++++ 1 file changed, 15 insertions(+) diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean index f1e8bcd67f96..75a3cfb29579 100644 --- a/src/Init/Data/BitVec/Lemmas.lean +++ b/src/Init/Data/BitVec/Lemmas.lean @@ -2704,6 +2704,21 @@ theorem shiftLeft_eq_mul_twoPow (x : BitVec w) (n : Nat) : ext i simp [getLsbD_shiftLeft, Fin.is_lt, decide_True, Bool.true_and, mul_twoPow_eq_shiftLeft] +@[simp] +theorem getMsbD_twoPow {i j w: Nat} : + (twoPow w i).getMsbD j = (decide (i < w) && decide (j = w - i - 1)) := by + simp only [getMsbD_eq_getLsbD, getLsbD_twoPow] + by_cases h₀ : i < w <;> by_cases h₁ : j < w <;> + simp [h₀, h₁] <;> omega + +@[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, + Bool.and_iff_right_iff_imp, Bool.and_eq_true, decide_eq_true_eq, and_imp] + intros + omega + /- ### cons -/ @[simp] theorem true_cons_zero : cons true 0#w = twoPow (w + 1) w := by From 9df17ff8ae686e71658ecc97f8a8ff6147144d3f Mon Sep 17 00:00:00 2001 From: luisacicolini Date: Sat, 26 Oct 2024 17:12:17 +0100 Subject: [PATCH 2/2] moved theorems closer to getelem --- src/Init/Data/BitVec/Lemmas.lean | 30 +++++++++++++++--------------- 1 file changed, 15 insertions(+), 15 deletions(-) diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean index 75a3cfb29579..9f35e7b4a381 100644 --- a/src/Init/Data/BitVec/Lemmas.lean +++ b/src/Init/Data/BitVec/Lemmas.lean @@ -2672,6 +2672,21 @@ theorem getElem_twoPow {i j : Nat} (h : j < w) : (twoPow w i)[j] = decide (j = i simp [eq_comm] omega +@[simp] +theorem getMsbD_twoPow {i j w: Nat} : + (twoPow w i).getMsbD j = (decide (i < w) && decide (j = w - i - 1)) := by + simp only [getMsbD_eq_getLsbD, getLsbD_twoPow] + by_cases h₀ : i < w <;> by_cases h₁ : j < w <;> + simp [h₀, h₁] <;> omega + +@[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, + Bool.and_iff_right_iff_imp, Bool.and_eq_true, decide_eq_true_eq, and_imp] + intros + 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 ext j @@ -2704,21 +2719,6 @@ theorem shiftLeft_eq_mul_twoPow (x : BitVec w) (n : Nat) : ext i simp [getLsbD_shiftLeft, Fin.is_lt, decide_True, Bool.true_and, mul_twoPow_eq_shiftLeft] -@[simp] -theorem getMsbD_twoPow {i j w: Nat} : - (twoPow w i).getMsbD j = (decide (i < w) && decide (j = w - i - 1)) := by - simp only [getMsbD_eq_getLsbD, getLsbD_twoPow] - by_cases h₀ : i < w <;> by_cases h₁ : j < w <;> - simp [h₀, h₁] <;> omega - -@[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, - Bool.and_iff_right_iff_imp, Bool.and_eq_true, decide_eq_true_eq, and_imp] - intros - omega - /- ### cons -/ @[simp] theorem true_cons_zero : cons true 0#w = twoPow (w + 1) w := by