From b6ed97bb3dad824d3c1fc82dbf290ef0505c42d0 Mon Sep 17 00:00:00 2001 From: Siddharth Date: Thu, 22 Feb 2024 00:07:14 +0000 Subject: [PATCH] feat: setup simp lemmas: 'msb -> getLsb -> decide ...' (#3436) This is a follow up to 'https://github.com/leanprover/std4/pull/645', where the simp lemmas were requested: https://github.com/leanprover/std4/pull/645#issuecomment-1944862251 --- Note that @semorrison asked to use `(Fin.last _)` to index. Now that we use a `Nat` to index `msb` , the pattern `(Fin.last _)` would not have the width be automatically inferred. Therefore, I've changed the definitions to use `Nat` for indexing. --------- Co-authored-by: Siddharth Bhat Mala Co-authored-by: Scott Morrison --- src/Init/Data/BitVec/Lemmas.lean | 17 ++++++++++++++--- 1 file changed, 14 insertions(+), 3 deletions(-) diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean index 2297326385..8552ff0ecf 100644 --- a/src/Init/Data/BitVec/Lemmas.lean +++ b/src/Init/Data/BitVec/Lemmas.lean @@ -117,9 +117,16 @@ private theorem lt_two_pow_of_le {x m n : Nat} (lt : x < 2 ^ m) (le : m ≤ n) : /-! ### msb -/ -theorem msb_eq_decide (x : BitVec (Nat.succ w)) : BitVec.msb x = decide (2 ^ w ≤ x.toNat) := by - simp only [BitVec.msb, getMsb, Nat.zero_lt_succ, - decide_True, getLsb, Nat.testBit, Nat.succ_sub_succ_eq_sub, +theorem msb_eq_getLsb_last (x : BitVec w) : + x.msb = x.getLsb (w - 1) := by + simp [BitVec.msb, getMsb, getLsb] + rcases w with rfl | w + · simp [BitVec.eq_nil x] + · simp + +@[simp] theorem getLsb_last (x : BitVec (w + 1)) : + x.getLsb w = decide (2 ^ w ≤ x.toNat) := by + simp only [Nat.zero_lt_succ, decide_True, getLsb, Nat.testBit, Nat.succ_sub_succ_eq_sub, Nat.sub_zero, Nat.and_one_is_mod, Bool.true_and, Nat.shiftRight_eq_div_pow] rcases (Nat.lt_or_ge (BitVec.toNat x) (2 ^ w)) with h | h · simp [Nat.div_eq_of_lt h, h] @@ -129,6 +136,10 @@ theorem msb_eq_decide (x : BitVec (Nat.succ w)) : BitVec.msb x = decide (2 ^ w · have : BitVec.toNat x < 2^w + 2^w := by simpa [Nat.pow_succ, Nat.mul_two] using x.isLt omega +@[simp] +theorem msb_eq_decide (x : BitVec (w + 1)) : BitVec.msb x = decide (2 ^ w ≤ x.toNat) := by + simp [msb_eq_getLsb_last] + /-! ### cast -/ @[simp] theorem toNat_cast (h : w = v) (x : BitVec w) : (cast h x).toNat = x.toNat := rfl