From 17865394d476111aca367e42626d66970e92bc56 Mon Sep 17 00:00:00 2001 From: Tobias Grosser Date: Tue, 10 Dec 2024 08:46:24 +0000 Subject: [PATCH] feat: BitVec.[toInt|toFin|getMsbD]_ofBool (#6317) This PR completes the basic API for BitVec.ofBool. --------- Co-authored-by: Kim Morrison --- src/Init/Data/BitVec/Lemmas.lean | 13 +++++++++++-- 1 file changed, 11 insertions(+), 2 deletions(-) diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean index 00b12166b8..a5036d1367 100644 --- a/src/Init/Data/BitVec/Lemmas.lean +++ b/src/Init/Data/BitVec/Lemmas.lean @@ -241,8 +241,11 @@ theorem toFin_one : toFin (1 : BitVec w) = 1 := by @[simp] theorem toNat_ofBool (b : Bool) : (ofBool b).toNat = b.toNat := by cases b <;> rfl -@[simp] theorem msb_ofBool (b : Bool) : (ofBool b).msb = b := by - cases b <;> simp [BitVec.msb, getMsbD, getLsbD] +@[simp] theorem toInt_ofBool (b : Bool) : (ofBool b).toInt = -b.toInt := by + cases b <;> rfl + +@[simp] theorem toFin_ofBool (b : Bool) : (ofBool b).toFin = Fin.ofNat' 2 (b.toNat) := by + cases b <;> rfl theorem ofNat_one (n : Nat) : BitVec.ofNat 1 n = BitVec.ofBool (n % 2 = 1) := by rcases (Nat.mod_two_eq_zero_or_one n) with h | h <;> simp [h, BitVec.ofNat, Fin.ofNat'] @@ -366,6 +369,12 @@ theorem getElem_ofBool {b : Bool} {i : Nat} : (ofBool b)[0] = b := by ยท simp only [ofBool] by_cases hi : i = 0 <;> simp [hi] <;> omega +@[simp] theorem getMsbD_ofBool (b : Bool) : (ofBool b).getMsbD i = (decide (i = 0) && b) := by + cases b <;> simp [getMsbD] + +@[simp] theorem msb_ofBool (b : Bool) : (ofBool b).msb = b := by + cases b <;> simp [BitVec.msb] + /-! ### msb -/ @[simp] theorem msb_zero : (0#w).msb = false := by simp [BitVec.msb, getMsbD]