feat: getMsbD_replicate

src/Init/Data/BitVec/Lemmas.lean

@@ -3078,9 +3078,11 @@ 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.mod_eq_sub_of_le_of_lt (n := 1)]
         congr 1
-        rw [← Nat.sub_mul_eq_mod_of_lt_of_le (n := 1) (by omega) (by omega), Nat.mul_one]
-        omega
+        · omega
+        · omega
+        · omega
       · simp [h₁]
 
 theorem getMsbD_rotateLeft {r n w : Nat} {x : BitVec w} :
@@ -3432,6 +3434,103 @@ theorem getElem_replicate {n w : Nat} (x : BitVec w) (h : i < w * n) :
   simp only [← getLsbD_eq_getElem, getLsbD_replicate]
   by_cases h' : w = 0 <;> simp [h'] <;> omega
 
+theorem append_assoc_left {a b c : Nat} (x : BitVec a) (y : BitVec b) (z : BitVec c) :
+    have : a + b + c = a + (b + c) := by rw [Nat.add_assoc]
+    (x ++ y) ++ z =  cast (by omega) (x ++ (y ++ z)) := by
+  ext k
+  simp only [getLsbD_cast, getLsbD_append]
+  by_cases h₀ : (↑k < c) <;> by_cases h₁ : (↑k < b + c)
+  · simp [h₀, h₁]
+  · simp [h₀, h₁]
+    omega
+  · simp [h₀, h₁]
+    by_cases h₂ : (↑k - c < b)
+    · simp [h₂]
+    · simp [h₂]
+      omega
+  · simp [h₀, h₁]
+    by_cases h₂ : (↑k - c < b)
+    · simp [h₂]
+      omega
+    · simp [h₂]
+      rw [Nat.sub_sub, Nat.add_comm (n := c)]
+
+@[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]
+
+theorem replicate_append_replicate_eq {w n : Nat} {x : BitVec w} (h : w * (n + m) = w * n + w * m := by omega) :
+    x.replicate n ++ x.replicate m = (x.replicate (n + m)).cast h := by
+  apply BitVec.eq_of_getLsbD_eq
+  simp only [getLsbD_cast, getLsbD_replicate, getLsbD_append, getLsbD_replicate]
+  intros i
+  by_cases h₀ : i < w * m <;> by_cases h₁ : i < w * (n + m)
+  · simp only [h₀, decide_true, Bool.true_and, cond_true, h₁]
+  · rw [Nat.mul_add] at h₁
+    simp only [h₀, decide_true, Bool.true_and, cond_true, Bool.iff_and_self, decide_eq_true_eq]
+    omega
+  · have h₂ : i ≥ w * m := by omega
+    simp only [h₀, decide_false, Bool.false_and, show i - w * m < w * n by omega, decide_true,
+      Bool.true_and, cond_false, h₁]
+    congr 1
+    rw [Nat.sub_mul_mod (by omega)]
+  · simp only [h₀, decide_false, Bool.false_and, cond_false, h₁, Bool.and_eq_false_imp,
+    decide_eq_true_eq]
+    omega
+
+
+
+@[simp]
+theorem getMsbD_replicate {n w : Nat} (x : BitVec w) :
+    (x.replicate n).getMsbD i =
+    (decide (i < w * n) && x.getMsbD (i % w)) := by
+  simp [getMsbD_eq_getLsbD]
+  by_cases h₀ : 0 < w
+  · by_cases h₁ : i < w * n <;> by_cases h₂ : n = 0
+    · simp [h₁, h₂]
+    · simp [h₁, h₂, show w * n - 1 - i < w * n by omega, Nat.mod_lt i h₀]
+      congr 1
+      induction n
+      case neg.e_i.zero => omega
+      case neg.e_i.succ n ih =>
+        simp_all [Nat.mul_add]
+        by_cases h₃ : i < w * n
+        · simp [show w * n + w - 1 -i = w + (w * n - 1 - i) by omega]
+          rw [ih (by omega)]
+          intros hcontra
+          subst hcontra
+          simp at h₃
+        · rw [Nat.mod_eq_of_lt]
+          · have := Nat.mod_add_div i w
+            have hiw : i / w = n := by
+              apply Nat.div_eq_of_lt_le
+              · rw [Nat.mul_comm]
+                omega
+              · rw [Nat.add_mul]
+                simp
+                rw [Nat.mul_comm]
+                omega
+            rw [hiw] at this
+            conv =>
+              lhs
+              rw [← this]
+            omega
+          · omega
+    · simp [h₁, h₂]
+    · simp [h₁, h₂]
+  · simp [show w = 0 by omega]
+
+@[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]
+  by_cases hn : 0 < n <;> by_cases hw : 0 < w
+  · simp [hn, hw]
+  · simp [show w = 0 by omega]
+  · simp [hn, hw]
+  · simp [show w = 0 by omega, show n = 0 by 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₃