feat: add BitVec.(getMsbD, msb)_replicate, replicate_one

src/Init/Data/BitVec/Lemmas.lean

@@ -3078,8 +3078,8 @@ theorem getMsbD_rotateLeft_of_lt {n w : Nat} {x : BitVec w} (hi : r < w):
       by_cases h₁ : n < w + 1
       · simp only [h₁, decide_true, Bool.true_and]
         have h₂ : (r + n) < 2 * (w + 1) := by omega
+        rw [← Nat.sub_mul_eq_mod_of_lt_of_le (i := (r + n)) (w := (w + 1)) (n := 1) (by omega) (by omega)]
         congr 1
-        rw [← Nat.sub_mul_eq_mod_of_lt_of_le (n := 1) (by omega) (by omega), Nat.mul_one]
         omega
       · simp [h₁]
 
@@ -3408,30 +3408,6 @@ theorem replicate_succ {x : BitVec w} :
     (x ++ replicate n x).cast (by rw [Nat.mul_succ]; omega) := by
   simp [replicate]
 
-@[simp]
-theorem getLsbD_replicate {n w : Nat} (x : BitVec w) :
-    (x.replicate n).getLsbD i =
-    (decide (i < w * n) && x.getLsbD (i % w)) := by
-  induction n generalizing x
-  case zero => simp
-  case succ n ih =>
-    simp only [replicate_succ, getLsbD_cast, getLsbD_append]
-    by_cases hi : i < w * (n + 1)
-    · simp only [hi, decide_true, Bool.true_and]
-      by_cases hi' : i < w * n
-      · simp [hi', ih]
-      · simp [hi', decide_false]
-        rw [Nat.sub_mul_eq_mod_of_lt_of_le] <;> omega
-    · rw [Nat.mul_succ] at hi ⊢
-      simp only [show ¬i < w * n by omega, decide_false, cond_false, hi, Bool.false_and]
-      apply BitVec.getLsbD_ge (x := x) (i := i - w * n) (ge := by omega)
-
-@[simp]
-theorem getElem_replicate {n w : Nat} (x : BitVec w) (h : i < w * n) :
-    (x.replicate n)[i] = if h' : w = 0 then false else x[i % w]'(@Nat.mod_lt i w (by omega)) := by
-  simp only [← getLsbD_eq_getElem, getLsbD_replicate]
-  by_cases h' : w = 0 <;> simp [h'] <;> omega
-
 theorem append_assoc {x₁ : BitVec w₁} {x₂ : BitVec w₂} {x₃ : BitVec w₃} :
     (x₁ ++ x₂) ++ x₃ = (x₁ ++ (x₂ ++ x₃)).cast (by omega) := by
   induction w₁ generalizing x₂ x₃
@@ -3796,6 +3772,47 @@ theorem reverse_replicate {n : Nat} {x : BitVec w} :
     conv => lhs; simp only [replicate_succ']
     simp [reverse_append, ih]
 
+@[simp]
+theorem getLsbD_replicate {n w : Nat} (x : BitVec w) :
+    (x.replicate n).getLsbD i =
+    (decide (i < w * n) && x.getLsbD (i % w)) := by
+  induction n generalizing x
+  case zero => simp
+  case succ n ih =>
+    simp only [replicate_succ, getLsbD_cast, getLsbD_append]
+    by_cases hi : i < w * (n + 1)
+    · simp only [hi, decide_true, Bool.true_and]
+      by_cases hi' : i < w * n
+      · simp [hi', ih]
+      · simp [hi', decide_false]
+        rw [Nat.sub_mul_eq_mod_of_lt_of_le] <;> omega
+    · rw [Nat.mul_succ] at hi ⊢
+      simp only [show ¬i < w * n by omega, decide_false, cond_false, hi, Bool.false_and]
+      apply BitVec.getLsbD_ge (x := x) (i := i - w * n) (ge := by omega)
+
+@[simp]
+theorem getElem_replicate {n w : Nat} (x : BitVec w) (h : i < w * n) :
+    (x.replicate n)[i] = if h' : w = 0 then false else x[i % w]'(@Nat.mod_lt i w (by omega)) := by
+  simp only [← getLsbD_eq_getElem, getLsbD_replicate]
+  by_cases h' : w = 0 <;> simp [h'] <;> omega
+
+@[simp]
+theorem replicate_one {w : Nat} {x : BitVec w} (h : w = w * 1 := by omega) :
+    (x.replicate 1) = x.cast h := by simp [replicate, h]
+
+@[simp]
+theorem getMsbD_replicate {n w : Nat} (x : BitVec w) :
+    (x.replicate n).getMsbD i =
+    (decide (i < w * n) && x.getMsbD (i % w)) := by
+  rw [← getLsbD_reverse, reverse_replicate, getLsbD_replicate, getLsbD_reverse]
+
+@[simp]
+theorem msb_replicate {n w : Nat} (x : BitVec w) :
+    (x.replicate n).msb =
+    (decide (0 < n) && x.msb) := by
+  simp [BitVec.msb, getMsbD_replicate]
+  cases n <;> cases w <;> simp
+
 /-! ### Decidable quantifiers -/
 
 theorem forall_zero_iff {P : BitVec 0 → Prop} :