feat: add BitVec.[toNat|toInt|toFin|getLsbD|getMsbD|getElem|msb]_fill (leanprover#6177)

This PR implements `BitVec.*_fill`.

We also add `toInt_allOnes` and `toFin_allOnes` as the former is needed
here. This completes the allOnes API.

Author: tobiasgrosser

src/Init/Data/BitVec/Lemmas.lean

@@ -785,6 +785,19 @@ theorem extractLsb'_eq_extractLsb {w : Nat} (x : BitVec w) (start len : Nat) (h
   unfold allOnes
   simp
 
+@[simp] theorem toInt_allOnes : (allOnes w).toInt = if 0 < w then -1 else 0 := by
+  norm_cast
+  by_cases h : w = 0
+  · subst h
+    simp
+  · have : 1 < 2 ^ w := by simp [h]
+    simp [BitVec.toInt]
+    omega
+
+@[simp] theorem toFin_allOnes : (allOnes w).toFin = Fin.ofNat' (2^w) (2^w - 1) := by
+  ext
+  simp
+
 @[simp] theorem getLsbD_allOnes : (allOnes v).getLsbD i = decide (i < v) := by
   simp [allOnes]
 
@@ -2382,6 +2395,54 @@ theorem not_neg (x : BitVec w) : ~~~(-x) = x + -1#w := by
         show (_ - x.toNat) % _ = _ by rw [Nat.mod_eq_of_lt (by omega)]]
       omega
 
+/-! ### fill -/
+
+@[simp]
+theorem getLsbD_fill {w i : Nat} {v : Bool} :
+    (fill w v).getLsbD i = (v && decide (i < w)) := by
+  by_cases h : v
+  <;> simp [h, BitVec.fill, BitVec.negOne_eq_allOnes]
+
+@[simp]
+theorem getMsbD_fill {w i : Nat} {v : Bool} :
+    (fill w v).getMsbD i = (v && decide (i < w)) := by
+  by_cases h : v
+  <;> simp [h, BitVec.fill, BitVec.negOne_eq_allOnes]
+
+@[simp]
+theorem getElem_fill {w i : Nat} {v : Bool} (h : i < w) :
+    (fill w v)[i] = v := by
+  by_cases h : v
+  <;> simp [h, BitVec.fill, BitVec.negOne_eq_allOnes]
+
+@[simp]
+theorem msb_fill {w : Nat} {v : Bool} :
+    (fill w v).msb = (v && decide (0 < w)) := by
+  simp [BitVec.msb]
+
+theorem fill_eq {w : Nat} {v : Bool} : fill w v = if v = true then allOnes w else 0#w := by
+  by_cases h : v <;> (simp only [h] ; ext ; simp)
+
+@[simp]
+theorem fill_true {w : Nat} : fill w true = allOnes w := by
+  simp [fill_eq]
+
+@[simp]
+theorem fill_false {w : Nat} : fill w false = 0#w := by
+  simp [fill_eq]
+
+@[simp] theorem fill_toNat {w : Nat} {v : Bool} :
+    (fill w v).toNat = if v = true then 2^w - 1 else 0 := by
+  by_cases h : v <;> simp [h]
+
+@[simp] theorem fill_toInt {w : Nat} {v : Bool} :
+    (fill w v).toInt = if v = true && 0 < w then -1 else 0 := by
+  by_cases h : v <;> simp [h]
+
+@[simp] theorem fill_toFin {w : Nat} {v : Bool} :
+    (fill w v).toFin = if v = true then (allOnes w).toFin else Fin.ofNat' (2 ^ w) 0 := by
+  by_cases h : v <;> simp [h]
+
 /-! ### mul -/
 
 theorem mul_def {n} {x y : BitVec n} : x * y = (ofFin <| x.toFin * y.toFin) := by rfl