feat: add bv_decide normalization rules for ofBool (a.getLsbD i) and ofBool a[i] (#5375)

In LNSym we often use the pattern `ofBool (a.getLsbD i)` to pick out a
specific bit (`i`) from a bitvector (`a`).

By adding a rewrite to `extractLsb` to `bv_decide`s normalization set,
we can still automatically close goals that have this pattern. In the
process, I also added a simp-lemma about the value of a `Fin 1`.

src/Init/Data/BitVec/Basic.lean

@@ -174,8 +174,7 @@ theorem getElem_eq_testBit_toNat (x : BitVec w) (i : Nat) (h : i < w) :
   x[i] = x.toNat.testBit i := rfl
 
 theorem getLsbD_eq_getElem {x : BitVec w} {i : Nat} (h : i < w) :
-    x.getLsbD i = x[i] := by
-  simp [getLsbD, getElem_eq_testBit_toNat]
+    x.getLsbD i = x[i] := rfl
 
 end getElem
 

src/Init/Data/Fin/Lemmas.lean

@@ -68,6 +68,9 @@ theorem mk_val (i : Fin n) : (⟨i, i.isLt⟩ : Fin n) = i := Fin.eta ..
 @[simp] theorem modn_val (a : Fin n) (b : Nat) : (a.modn b).val = a.val % b :=
   rfl
 
+@[simp] theorem val_eq_zero (a : Fin 1) : a.val = 0 :=
+  Nat.eq_zero_of_le_zero <| Nat.le_of_lt_succ a.isLt
+
 theorem ite_val {n : Nat} {c : Prop} [Decidable c] {x : c → Fin n} (y : ¬c → Fin n) :
     (if h : c then x h else y h).val = if h : c then (x h).val else (y h).val := by
   by_cases c <;> simp [*]

src/Std/Tactic/BVDecide/Normalize/BitVec.lean

@@ -206,5 +206,17 @@ theorem BitVec.max_ult' (a : BitVec w) : (BitVec.ult (-1#w) a) = false := by
 
 attribute [bv_normalize] BitVec.replicate_zero_eq
 
+@[bv_normalize]
+theorem BitVec.ofBool_getLsbD (a : BitVec w) (i : Nat) :
+    BitVec.ofBool (a.getLsbD i) = a.extractLsb' i 1 := by
+  ext j
+  simp
+
+@[bv_normalize]
+theorem BitVec.ofBool_getElem (a : BitVec w) (i : Nat) (h : i < w) :
+    BitVec.ofBool a[i] = a.extractLsb' i 1 := by
+  rw [← BitVec.getLsbD_eq_getElem]
+  apply ofBool_getLsbD
+
 end Normalize
 end Std.Tactic.BVDecide

tests/lean/run/bv_extract.lean

@@ -13,3 +13,15 @@ theorem bv_extract_3 (h : x = 1#64) : extractLsb 63 32 x = 0#32 := by
 
 theorem bv_extract_4 (h : x = 1#64) : extractLsb 31 0 x = 1#32 := by
   bv_decide
+
+theorem bv_ofBool_1 (h : x = 1#64) : ofBool (x.getLsbD 0) = 1#1 := by
+  bv_decide
+
+theorem bv_ofBool_2 (h : x = 1#64) : ofBool (x.getLsbD 1) = 0#1 := by
+  bv_decide
+
+theorem bv_ofBool_3 (h : x = 1#64) : ofBool x[0] = 1#1 := by
+  bv_decide
+
+theorem bv_ofBool_4 (h : x = 1#64) : ofBool x[1] = 0#1 := by
+  bv_decide