From eb1d9eedf7bbd733fea1deeec58beea978a0a066 Mon Sep 17 00:00:00 2001
From: luisacicolini <lc985@cam.ac.uk>
Date: Tue, 21 Jan 2025 10:24:29 +0000
Subject: [PATCH 01/21] feat: getMsbD_replicate

---
 src/Init/Data/BitVec/Lemmas.lean | 103 ++++++++++++++++++++++++++++++-
 1 file changed, 101 insertions(+), 2 deletions(-)

diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean
index 19fbf08d4603..b2e6ae7246aa 100644
--- a/src/Init/Data/BitVec/Lemmas.lean
+++ b/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₃

From 3227ec0500e539f792344457ed0aea3e6bdca211 Mon Sep 17 00:00:00 2001
From: luisacicolini <lc985@cam.ac.uk>
Date: Tue, 21 Jan 2025 10:29:16 +0000
Subject: [PATCH 02/21] chore: getMsbD_rotateLeft_of_lt undo change

---
 src/Init/Data/BitVec/Lemmas.lean | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean
index b2e6ae7246aa..15ad2d6f94ae 100644
--- a/src/Init/Data/BitVec/Lemmas.lean
+++ b/src/Init/Data/BitVec/Lemmas.lean
@@ -3080,9 +3080,8 @@ theorem getMsbD_rotateLeft_of_lt {n w : Nat} {x : BitVec w} (hi : r < w):
         have h₂ : (r + n) < 2 * (w + 1) := by omega
         rw [Nat.mod_eq_sub_of_le_of_lt (n := 1)]
         congr 1
-        · omega
-        · omega
-        · omega
+        rw [← Nat.sub_mul_eq_mod_of_lt_of_le (n := 1) (by omega) (by omega), Nat.mul_one]
+        omega
       · simp [h₁]
 
 theorem getMsbD_rotateLeft {r n w : Nat} {x : BitVec w} :

From 8f708f3285713ebb71ec3c4bb803f37c3bd132e8 Mon Sep 17 00:00:00 2001
From: luisacicolini <lc985@cam.ac.uk>
Date: Tue, 21 Jan 2025 10:30:02 +0000
Subject: [PATCH 03/21] chore: remove append_assoc_left

---
 src/Init/Data/BitVec/Lemmas.lean | 21 ---------------------
 1 file changed, 21 deletions(-)

diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean
index 15ad2d6f94ae..5a96f843729c 100644
--- a/src/Init/Data/BitVec/Lemmas.lean
+++ b/src/Init/Data/BitVec/Lemmas.lean
@@ -3433,27 +3433,6 @@ 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]

From 96233b354eb9287eeda24df299d872aea330da4e Mon Sep 17 00:00:00 2001
From: luisacicolini <lc985@cam.ac.uk>
Date: Tue, 21 Jan 2025 10:31:26 +0000
Subject: [PATCH 04/21] chore: restart proof with replicate

---
 src/Init/Data/BitVec/Lemmas.lean | 36 ++------------------------------
 1 file changed, 2 insertions(+), 34 deletions(-)

diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean
index 5a96f843729c..f50d310600ad 100644
--- a/src/Init/Data/BitVec/Lemmas.lean
+++ b/src/Init/Data/BitVec/Lemmas.lean
@@ -3413,19 +3413,8 @@ theorem replicate_succ {x : BitVec w} :
 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)
+  rw [← getLsbD_reverse]
+  rw [reverse_replicate, getLsbD_replicate, getLsbD_reverse]
 
 @[simp]
 theorem getElem_replicate {n w : Nat} (x : BitVec w) (h : i < w * n) :
@@ -3437,27 +3426,6 @@ theorem getElem_replicate {n w : Nat} (x : BitVec w) (h : i < w * n) :
 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 =

From b62806e3803962e663964aa9e97c2979e8dd597f Mon Sep 17 00:00:00 2001
From: luisacicolini <lc985@cam.ac.uk>
Date: Tue, 21 Jan 2025 11:19:03 +0000
Subject: [PATCH 05/21] chore: fix getMsbD_rotateLeft_of_lt proof

---
 src/Init/Data/BitVec/Lemmas.lean | 9 ++++-----
 1 file changed, 4 insertions(+), 5 deletions(-)

diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean
index f50d310600ad..38fb3eda6c2c 100644
--- a/src/Init/Data/BitVec/Lemmas.lean
+++ b/src/Init/Data/BitVec/Lemmas.lean
@@ -3078,9 +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.mod_eq_sub_of_le_of_lt (n := 1)]
+        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₁]
 
@@ -3412,9 +3411,9 @@ theorem replicate_succ {x : BitVec w} :
 @[simp]
 theorem getLsbD_replicate {n w : Nat} (x : BitVec w) :
     (x.replicate n).getLsbD i =
-    (decide (i < w * n) && x.getLsbD (i % w)) := by
-  rw [← getLsbD_reverse]
-  rw [reverse_replicate, getLsbD_replicate, getLsbD_reverse]
+    (decide (i < w * n) && x.getLsbD (i % w)) := by sorry
+  -- rw [← getLsbD_reverse]
+  -- rw [reverse_replicate, getLsbD_replicate, getLsbD_reverse]
 
 @[simp]
 theorem getElem_replicate {n w : Nat} (x : BitVec w) (h : i < w * n) :

From 648cd67525f7cf5b444e894d17fc15d8b4f907e6 Mon Sep 17 00:00:00 2001
From: luisacicolini <lc985@cam.ac.uk>
Date: Tue, 21 Jan 2025 11:21:25 +0000
Subject: [PATCH 06/21] chore: reordeering

---
 src/Init/Data/BitVec/Lemmas.lean | 174 +++++++++++++++----------------
 1 file changed, 87 insertions(+), 87 deletions(-)

diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean
index 38fb3eda6c2c..1cff00448c06 100644
--- a/src/Init/Data/BitVec/Lemmas.lean
+++ b/src/Init/Data/BitVec/Lemmas.lean
@@ -3360,6 +3360,91 @@ theorem udiv_twoPow_eq_of_lt {w : Nat} {x : BitVec w} {k : Nat} (hk : k < w) : x
   ext
   simp [getLsbD_concat]
 
+/-! ### Reverse -/
+
+theorem getLsbD_reverse {i : Nat} {x : BitVec w} :
+    (x.reverse).getLsbD i = x.getMsbD i := by
+  induction w generalizing i
+  case zero => simp
+  case succ n ih =>
+    simp only [reverse, truncate_eq_setWidth, getLsbD_concat]
+    rcases i with rfl | i
+    · rfl
+    · simp only [Nat.add_one_ne_zero, ↓reduceIte, Nat.add_one_sub_one, ih]
+      rw [getMsbD_setWidth]
+      simp only [show n - (n + 1) = 0 by omega, Nat.zero_le, decide_true, Bool.true_and]
+      congr; omega
+
+theorem getMsbD_reverse {i : Nat} {x : BitVec w} :
+    (x.reverse).getMsbD i = x.getLsbD i := by
+  simp only [getMsbD_eq_getLsbD, getLsbD_reverse]
+  by_cases hi : i < w
+  · simp only [hi, decide_true, show w - 1 - i < w by omega, Bool.true_and]
+    congr; omega
+  · simp [hi, show i ≥ w by omega]
+
+theorem msb_reverse {x : BitVec w} :
+    (x.reverse).msb = x.getLsbD 0 :=
+  by rw [BitVec.msb, getMsbD_reverse]
+
+theorem reverse_append {x : BitVec w} {y : BitVec v} :
+    (x ++ y).reverse = (y.reverse ++ x.reverse).cast (by omega) := by
+  ext i h
+  simp only [getLsbD_append, getLsbD_reverse]
+  by_cases hi : i < v
+  · by_cases hw : w ≤ i
+    · simp [getMsbD_append, getLsbD_cast, getLsbD_append, getLsbD_reverse, hw]
+    · simp [getMsbD_append, getLsbD_cast, getLsbD_append, getLsbD_reverse, hw, show i < w by omega]
+  · by_cases hw : w ≤ i
+    · simp [getMsbD_append, getLsbD_cast, getLsbD_append, hw, show ¬ i < w by omega, getLsbD_reverse]
+    · simp [getMsbD_append, getLsbD_cast, getLsbD_append, hw, show i < w by omega, getLsbD_reverse]
+
+@[simp]
+theorem reverse_cast {w v : Nat} (h : w = v) (x : BitVec w) :
+    (x.cast h).reverse = x.reverse.cast h := by
+  subst h; simp
+
+@[simp]
+theorem replicate_succ {x : BitVec w} :
+    x.replicate (n + 1) =
+    (x ++ replicate n x).cast (by rw [Nat.mul_succ]; omega) := by
+  simp [replicate]
+
+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₃
+  case zero => simp
+  case succ n ih =>
+    specialize @ih (setWidth n x₁)
+    rw [← cons_msb_setWidth x₁, cons_append_append, ih, cons_append]
+    ext j h
+    simp [getLsbD_cons, show n + w₂ + w₃ = n + (w₂ + w₃) by omega]
+
+theorem replicate_append_self {x : BitVec w} :
+    x ++ x.replicate n = (x.replicate n ++ x).cast (by omega) := by
+  induction n with
+  | zero => simp
+  | succ n ih =>
+    rw [replicate_succ]
+    conv => lhs; rw [ih]
+    simp only [cast_cast, cast_eq]
+    rw [← cast_append_left]
+    · rw [append_assoc]; congr
+    · rw [Nat.add_comm, Nat.mul_add, Nat.mul_one]; omega
+
+theorem replicate_succ' {x : BitVec w} :
+    x.replicate (n + 1) =
+    (replicate n x ++ x).cast (by rw [Nat.mul_succ]) := by
+  simp [replicate_append_self]
+
+theorem reverse_replicate {n : Nat} {x : BitVec w} :
+    (x.replicate n).reverse = (x.reverse).replicate n := by
+  induction n with
+  | zero => rfl
+  | succ n ih =>
+    conv => lhs; simp only [replicate_succ']
+    simp [reverse_append, ih]
+
 /- ### setWidth, setWidth, and bitwise operations -/
 
 /--
@@ -3402,17 +3487,11 @@ theorem and_one_eq_setWidth_ofBool_getLsbD {x : BitVec w} :
 theorem replicate_zero {x : BitVec w} : x.replicate 0 = 0#0 := by
   simp [replicate]
 
-@[simp]
-theorem replicate_succ {x : BitVec w} :
-    x.replicate (n + 1) =
-    (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 sorry
-  -- rw [← getLsbD_reverse]
+    (decide (i < w * n) && x.getLsbD (i % w)) := by
+  rw [← getLsbD_reverse]
   -- rw [reverse_replicate, getLsbD_replicate, getLsbD_reverse]
 
 @[simp]
@@ -3476,33 +3555,6 @@ theorem msb_replicate {n w : Nat} (x : BitVec w) :
   · 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₃
-  case zero => simp
-  case succ n ih =>
-    specialize @ih (setWidth n x₁)
-    rw [← cons_msb_setWidth x₁, cons_append_append, ih, cons_append]
-    ext j h
-    simp [getLsbD_cons, show n + w₂ + w₃ = n + (w₂ + w₃) by omega]
-
-theorem replicate_append_self {x : BitVec w} :
-    x ++ x.replicate n = (x.replicate n ++ x).cast (by omega) := by
-  induction n with
-  | zero => simp
-  | succ n ih =>
-    rw [replicate_succ]
-    conv => lhs; rw [ih]
-    simp only [cast_cast, cast_eq]
-    rw [← cast_append_left]
-    · rw [append_assoc]; congr
-    · rw [Nat.add_comm, Nat.mul_add, Nat.mul_one]; omega
-
-theorem replicate_succ' {x : BitVec w} :
-    x.replicate (n + 1) =
-    (replicate n x ++ x).cast (by rw [Nat.mul_succ]) := by
-  simp [replicate_append_self]
-
 /-! ### intMin -/
 
 /-- The bitvector of width `w` that has the smallest value when interpreted as an integer. -/
@@ -3788,58 +3840,6 @@ theorem toInt_abs_eq_natAbs_of_ne_intMin {x : BitVec w} (hx : x ≠ intMin w) :
     x.abs.toInt = x.toInt.natAbs := by
   simp [toInt_abs_eq_natAbs, hx]
 
-/-! ### Reverse -/
-
-theorem getLsbD_reverse {i : Nat} {x : BitVec w} :
-    (x.reverse).getLsbD i = x.getMsbD i := by
-  induction w generalizing i
-  case zero => simp
-  case succ n ih =>
-    simp only [reverse, truncate_eq_setWidth, getLsbD_concat]
-    rcases i with rfl | i
-    · rfl
-    · simp only [Nat.add_one_ne_zero, ↓reduceIte, Nat.add_one_sub_one, ih]
-      rw [getMsbD_setWidth]
-      simp only [show n - (n + 1) = 0 by omega, Nat.zero_le, decide_true, Bool.true_and]
-      congr; omega
-
-theorem getMsbD_reverse {i : Nat} {x : BitVec w} :
-    (x.reverse).getMsbD i = x.getLsbD i := by
-  simp only [getMsbD_eq_getLsbD, getLsbD_reverse]
-  by_cases hi : i < w
-  · simp only [hi, decide_true, show w - 1 - i < w by omega, Bool.true_and]
-    congr; omega
-  · simp [hi, show i ≥ w by omega]
-
-theorem msb_reverse {x : BitVec w} :
-    (x.reverse).msb = x.getLsbD 0 :=
-  by rw [BitVec.msb, getMsbD_reverse]
-
-theorem reverse_append {x : BitVec w} {y : BitVec v} :
-    (x ++ y).reverse = (y.reverse ++ x.reverse).cast (by omega) := by
-  ext i h
-  simp only [getLsbD_append, getLsbD_reverse]
-  by_cases hi : i < v
-  · by_cases hw : w ≤ i
-    · simp [getMsbD_append, getLsbD_cast, getLsbD_append, getLsbD_reverse, hw]
-    · simp [getMsbD_append, getLsbD_cast, getLsbD_append, getLsbD_reverse, hw, show i < w by omega]
-  · by_cases hw : w ≤ i
-    · simp [getMsbD_append, getLsbD_cast, getLsbD_append, hw, show ¬ i < w by omega, getLsbD_reverse]
-    · simp [getMsbD_append, getLsbD_cast, getLsbD_append, hw, show i < w by omega, getLsbD_reverse]
-
-@[simp]
-theorem reverse_cast {w v : Nat} (h : w = v) (x : BitVec w) :
-    (x.cast h).reverse = x.reverse.cast h := by
-  subst h; simp
-
-theorem reverse_replicate {n : Nat} {x : BitVec w} :
-    (x.replicate n).reverse = (x.reverse).replicate n := by
-  induction n with
-  | zero => rfl
-  | succ n ih =>
-    conv => lhs; simp only [replicate_succ']
-    simp [reverse_append, ih]
-
 /-! ### Decidable quantifiers -/
 
 theorem forall_zero_iff {P : BitVec 0 → Prop} :

From 6e74763225bf62454aa655e58c571a6c38587a8e Mon Sep 17 00:00:00 2001
From: luisacicolini <lc985@cam.ac.uk>
Date: Tue, 21 Jan 2025 11:28:07 +0000
Subject: [PATCH 07/21] chore: fix proofs

---
 src/Init/Data/BitVec/Lemmas.lean | 51 +++++++++-----------------------
 1 file changed, 14 insertions(+), 37 deletions(-)

diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean
index 1cff00448c06..879d7b204a54 100644
--- a/src/Init/Data/BitVec/Lemmas.lean
+++ b/src/Init/Data/BitVec/Lemmas.lean
@@ -3491,8 +3491,19 @@ theorem replicate_zero {x : BitVec w} : x.replicate 0 = 0#0 := by
 theorem getLsbD_replicate {n w : Nat} (x : BitVec w) :
     (x.replicate n).getLsbD i =
     (decide (i < w * n) && x.getLsbD (i % w)) := by
-  rw [← getLsbD_reverse]
-  -- rw [reverse_replicate, getLsbD_replicate, getLsbD_reverse]
+  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) :
@@ -3508,41 +3519,7 @@ theorem replicate_one {w : Nat} {x : BitVec w} (h : w = w * 1 := by omega) :
 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]
+  rw [← getLsbD_reverse, reverse_replicate, getLsbD_replicate, getLsbD_reverse]
 
 @[simp]
 theorem msb_replicate {n w : Nat} (x : BitVec w) :

From 3fd39c318b1a932be1a59735bdda4c86b2cc7074 Mon Sep 17 00:00:00 2001
From: luisacicolini <lc985@cam.ac.uk>
Date: Tue, 21 Jan 2025 11:33:28 +0000
Subject: [PATCH 08/21] chore: msb_replicare better proof

---
 src/Init/Data/BitVec/Lemmas.lean | 8 ++------
 1 file changed, 2 insertions(+), 6 deletions(-)

diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean
index 879d7b204a54..15d01466f32b 100644
--- a/src/Init/Data/BitVec/Lemmas.lean
+++ b/src/Init/Data/BitVec/Lemmas.lean
@@ -3525,12 +3525,8 @@ theorem getMsbD_replicate {n w : Nat} (x : BitVec w) :
 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]
+  simp [BitVec.msb]
+  cases n <;> cases w <;> simp
 
 /-! ### intMin -/
 

From 167062cd06fd2cf5f9fb69edd2a3094c162a0814 Mon Sep 17 00:00:00 2001
From: luisacicolini <lc985@cam.ac.uk>
Date: Tue, 21 Jan 2025 11:45:21 +0000
Subject: [PATCH 09/21] chore: simple order

---
 src/Init/Data/BitVec/Lemmas.lean | 240 +++++++++++++++----------------
 1 file changed, 120 insertions(+), 120 deletions(-)

diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean
index 15d01466f32b..a2a644dec9a0 100644
--- a/src/Init/Data/BitVec/Lemmas.lean
+++ b/src/Init/Data/BitVec/Lemmas.lean
@@ -3360,91 +3360,6 @@ theorem udiv_twoPow_eq_of_lt {w : Nat} {x : BitVec w} {k : Nat} (hk : k < w) : x
   ext
   simp [getLsbD_concat]
 
-/-! ### Reverse -/
-
-theorem getLsbD_reverse {i : Nat} {x : BitVec w} :
-    (x.reverse).getLsbD i = x.getMsbD i := by
-  induction w generalizing i
-  case zero => simp
-  case succ n ih =>
-    simp only [reverse, truncate_eq_setWidth, getLsbD_concat]
-    rcases i with rfl | i
-    · rfl
-    · simp only [Nat.add_one_ne_zero, ↓reduceIte, Nat.add_one_sub_one, ih]
-      rw [getMsbD_setWidth]
-      simp only [show n - (n + 1) = 0 by omega, Nat.zero_le, decide_true, Bool.true_and]
-      congr; omega
-
-theorem getMsbD_reverse {i : Nat} {x : BitVec w} :
-    (x.reverse).getMsbD i = x.getLsbD i := by
-  simp only [getMsbD_eq_getLsbD, getLsbD_reverse]
-  by_cases hi : i < w
-  · simp only [hi, decide_true, show w - 1 - i < w by omega, Bool.true_and]
-    congr; omega
-  · simp [hi, show i ≥ w by omega]
-
-theorem msb_reverse {x : BitVec w} :
-    (x.reverse).msb = x.getLsbD 0 :=
-  by rw [BitVec.msb, getMsbD_reverse]
-
-theorem reverse_append {x : BitVec w} {y : BitVec v} :
-    (x ++ y).reverse = (y.reverse ++ x.reverse).cast (by omega) := by
-  ext i h
-  simp only [getLsbD_append, getLsbD_reverse]
-  by_cases hi : i < v
-  · by_cases hw : w ≤ i
-    · simp [getMsbD_append, getLsbD_cast, getLsbD_append, getLsbD_reverse, hw]
-    · simp [getMsbD_append, getLsbD_cast, getLsbD_append, getLsbD_reverse, hw, show i < w by omega]
-  · by_cases hw : w ≤ i
-    · simp [getMsbD_append, getLsbD_cast, getLsbD_append, hw, show ¬ i < w by omega, getLsbD_reverse]
-    · simp [getMsbD_append, getLsbD_cast, getLsbD_append, hw, show i < w by omega, getLsbD_reverse]
-
-@[simp]
-theorem reverse_cast {w v : Nat} (h : w = v) (x : BitVec w) :
-    (x.cast h).reverse = x.reverse.cast h := by
-  subst h; simp
-
-@[simp]
-theorem replicate_succ {x : BitVec w} :
-    x.replicate (n + 1) =
-    (x ++ replicate n x).cast (by rw [Nat.mul_succ]; omega) := by
-  simp [replicate]
-
-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₃
-  case zero => simp
-  case succ n ih =>
-    specialize @ih (setWidth n x₁)
-    rw [← cons_msb_setWidth x₁, cons_append_append, ih, cons_append]
-    ext j h
-    simp [getLsbD_cons, show n + w₂ + w₃ = n + (w₂ + w₃) by omega]
-
-theorem replicate_append_self {x : BitVec w} :
-    x ++ x.replicate n = (x.replicate n ++ x).cast (by omega) := by
-  induction n with
-  | zero => simp
-  | succ n ih =>
-    rw [replicate_succ]
-    conv => lhs; rw [ih]
-    simp only [cast_cast, cast_eq]
-    rw [← cast_append_left]
-    · rw [append_assoc]; congr
-    · rw [Nat.add_comm, Nat.mul_add, Nat.mul_one]; omega
-
-theorem replicate_succ' {x : BitVec w} :
-    x.replicate (n + 1) =
-    (replicate n x ++ x).cast (by rw [Nat.mul_succ]) := by
-  simp [replicate_append_self]
-
-theorem reverse_replicate {n : Nat} {x : BitVec w} :
-    (x.replicate n).reverse = (x.reverse).replicate n := by
-  induction n with
-  | zero => rfl
-  | succ n ih =>
-    conv => lhs; simp only [replicate_succ']
-    simp [reverse_append, ih]
-
 /- ### setWidth, setWidth, and bitwise operations -/
 
 /--
@@ -3488,45 +3403,37 @@ theorem replicate_zero {x : BitVec w} : x.replicate 0 = 0#0 := 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
+theorem replicate_succ {x : BitVec w} :
+    x.replicate (n + 1) =
+    (x ++ replicate n x).cast (by rw [Nat.mul_succ]; omega) := by
+  simp [replicate]
+
+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₃
   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]
+    specialize @ih (setWidth n x₁)
+    rw [← cons_msb_setWidth x₁, cons_append_append, ih, cons_append]
+    ext j h
+    simp [getLsbD_cons, show n + w₂ + w₃ = n + (w₂ + w₃) by 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
-  rw [← getLsbD_reverse, reverse_replicate, getLsbD_replicate, getLsbD_reverse]
+theorem replicate_append_self {x : BitVec w} :
+    x ++ x.replicate n = (x.replicate n ++ x).cast (by omega) := by
+  induction n with
+  | zero => simp
+  | succ n ih =>
+    rw [replicate_succ]
+    conv => lhs; rw [ih]
+    simp only [cast_cast, cast_eq]
+    rw [← cast_append_left]
+    · rw [append_assoc]; congr
+    · rw [Nat.add_comm, Nat.mul_add, Nat.mul_one]; omega
 
-@[simp]
-theorem msb_replicate {n w : Nat} (x : BitVec w) :
-    (x.replicate n).msb =
-    (decide (0 < n) && x.msb) := by
-  simp [BitVec.msb]
-  cases n <;> cases w <;> simp
+theorem replicate_succ' {x : BitVec w} :
+    x.replicate (n + 1) =
+    (replicate n x ++ x).cast (by rw [Nat.mul_succ]) := by
+  simp [replicate_append_self]
 
 /-! ### intMin -/
 
@@ -3813,6 +3720,99 @@ theorem toInt_abs_eq_natAbs_of_ne_intMin {x : BitVec w} (hx : x ≠ intMin w) :
     x.abs.toInt = x.toInt.natAbs := by
   simp [toInt_abs_eq_natAbs, hx]
 
+/-! ### Reverse -/
+
+theorem getLsbD_reverse {i : Nat} {x : BitVec w} :
+    (x.reverse).getLsbD i = x.getMsbD i := by
+  induction w generalizing i
+  case zero => simp
+  case succ n ih =>
+    simp only [reverse, truncate_eq_setWidth, getLsbD_concat]
+    rcases i with rfl | i
+    · rfl
+    · simp only [Nat.add_one_ne_zero, ↓reduceIte, Nat.add_one_sub_one, ih]
+      rw [getMsbD_setWidth]
+      simp only [show n - (n + 1) = 0 by omega, Nat.zero_le, decide_true, Bool.true_and]
+      congr; omega
+
+theorem getMsbD_reverse {i : Nat} {x : BitVec w} :
+    (x.reverse).getMsbD i = x.getLsbD i := by
+  simp only [getMsbD_eq_getLsbD, getLsbD_reverse]
+  by_cases hi : i < w
+  · simp only [hi, decide_true, show w - 1 - i < w by omega, Bool.true_and]
+    congr; omega
+  · simp [hi, show i ≥ w by omega]
+
+theorem msb_reverse {x : BitVec w} :
+    (x.reverse).msb = x.getLsbD 0 :=
+  by rw [BitVec.msb, getMsbD_reverse]
+
+theorem reverse_append {x : BitVec w} {y : BitVec v} :
+    (x ++ y).reverse = (y.reverse ++ x.reverse).cast (by omega) := by
+  ext i h
+  simp only [getLsbD_append, getLsbD_reverse]
+  by_cases hi : i < v
+  · by_cases hw : w ≤ i
+    · simp [getMsbD_append, getLsbD_cast, getLsbD_append, getLsbD_reverse, hw]
+    · simp [getMsbD_append, getLsbD_cast, getLsbD_append, getLsbD_reverse, hw, show i < w by omega]
+  · by_cases hw : w ≤ i
+    · simp [getMsbD_append, getLsbD_cast, getLsbD_append, hw, show ¬ i < w by omega, getLsbD_reverse]
+    · simp [getMsbD_append, getLsbD_cast, getLsbD_append, hw, show i < w by omega, getLsbD_reverse]
+
+@[simp]
+theorem reverse_cast {w v : Nat} (h : w = v) (x : BitVec w) :
+    (x.cast h).reverse = x.reverse.cast h := by
+  subst h; simp
+
+theorem reverse_replicate {n : Nat} {x : BitVec w} :
+    (x.replicate n).reverse = (x.reverse).replicate n := by
+  induction n with
+  | zero => rfl
+  | succ n ih =>
+    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} :

From 1ad467ba30e1f8e50739dd8fd685f21301c2a38c Mon Sep 17 00:00:00 2001
From: luisacicolini <lc985@cam.ac.uk>
Date: Tue, 21 Jan 2025 11:51:26 +0000
Subject: [PATCH 10/21] chore: fix simp only

---
 src/Init/Data/BitVec/Lemmas.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean
index a2a644dec9a0..1268127aafa5 100644
--- a/src/Init/Data/BitVec/Lemmas.lean
+++ b/src/Init/Data/BitVec/Lemmas.lean
@@ -3810,7 +3810,7 @@ theorem getMsbD_replicate {n w : Nat} (x : BitVec w) :
 theorem msb_replicate {n w : Nat} (x : BitVec w) :
     (x.replicate n).msb =
     (decide (0 < n) && x.msb) := by
-  simp [BitVec.msb, getMsbD_replicate]
+  simp only [BitVec.msb, getMsbD_replicate, Nat.zero_mod]
   cases n <;> cases w <;> simp
 
 /-! ### Decidable quantifiers -/

From 72ea87b32ebc497adb6ca7d9b206a0e27fd7ca1d Mon Sep 17 00:00:00 2001
From: luisacicolini <lc985@cam.ac.uk>
Date: Tue, 21 Jan 2025 11:53:35 +0000
Subject: [PATCH 11/21] chore: format

---
 src/Init/Data/BitVec/Lemmas.lean | 14 ++++++--------
 1 file changed, 6 insertions(+), 8 deletions(-)

diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean
index 1268127aafa5..8bfedbd54a4b 100644
--- a/src/Init/Data/BitVec/Lemmas.lean
+++ b/src/Init/Data/BitVec/Lemmas.lean
@@ -3773,9 +3773,8 @@ theorem reverse_replicate {n : Nat} {x : BitVec w} :
     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
+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 =>
@@ -3791,7 +3790,7 @@ theorem getLsbD_replicate {n w : Nat} (x : BitVec w) :
       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) :
+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
@@ -3801,13 +3800,12 @@ 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
+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) :
+theorem msb_replicate {n w : Nat} {x : BitVec w} :
     (x.replicate n).msb =
     (decide (0 < n) && x.msb) := by
   simp only [BitVec.msb, getMsbD_replicate, Nat.zero_mod]

From 4bd9cfb0fb4eb90d264e16f16e0eb6677d28002e Mon Sep 17 00:00:00 2001
From: luisacicolini <lc985@cam.ac.uk>
Date: Tue, 21 Jan 2025 11:58:58 +0000
Subject: [PATCH 12/21] chore: remove mul_one

---
 src/Init/Data/BitVec/Lemmas.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean
index 8bfedbd54a4b..bf19faf84e7f 100644
--- a/src/Init/Data/BitVec/Lemmas.lean
+++ b/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 (i := (r + n)) (w := (w + 1)) (n := 1) (by omega) (by omega)]
         omega
       · simp [h₁]
 

From 0c73020cef263dba2602078ac3475f110093bfdb Mon Sep 17 00:00:00 2001
From: luisacicolini <lc985@cam.ac.uk>
Date: Tue, 21 Jan 2025 12:57:54 +0000
Subject: [PATCH 13/21] chore: remove useless var spec

---
 src/Init/Data/BitVec/Lemmas.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean
index bf19faf84e7f..618b1cf0270e 100644
--- a/src/Init/Data/BitVec/Lemmas.lean
+++ b/src/Init/Data/BitVec/Lemmas.lean
@@ -3079,7 +3079,7 @@ theorem getMsbD_rotateLeft_of_lt {n w : Nat} {x : BitVec w} (hi : r < w):
       · simp only [h₁, decide_true, Bool.true_and]
         have h₂ : (r + n) < 2 * (w + 1) := by omega
         congr 1
-        rw [← Nat.sub_mul_eq_mod_of_lt_of_le (i := (r + n)) (w := (w + 1)) (n := 1) (by omega) (by omega)]
+        rw [← Nat.sub_mul_eq_mod_of_lt_of_le (n := 1) (by omega) (by omega)]
         omega
       · simp [h₁]
 

From f794c9e8b97cd7ebca0fd42b50714f04e7b0c31b Mon Sep 17 00:00:00 2001
From: Luisa Cicolini <48860705+luisacicolini@users.noreply.github.com>
Date: Tue, 21 Jan 2025 14:45:41 +0000
Subject: [PATCH 14/21] chore: format of proof

Co-authored-by: Alex Keizer <alex@keizer.dev>
---
 src/Init/Data/BitVec/Lemmas.lean | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean
index 618b1cf0270e..e4d07c5cf9db 100644
--- a/src/Init/Data/BitVec/Lemmas.lean
+++ b/src/Init/Data/BitVec/Lemmas.lean
@@ -3797,7 +3797,8 @@ theorem getElem_replicate {n w : Nat} {x : BitVec w} (h : i < w * n) :
 
 @[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]
+    (x.replicate 1) = x.cast h := by 
+  simp [replicate, h]
 
 @[simp]
 theorem getMsbD_replicate {n w : Nat} {x : BitVec w} :

From 4481757206564c6a4788a2ebf941a1a633d3abcd Mon Sep 17 00:00:00 2001
From: Luisa Cicolini <48860705+luisacicolini@users.noreply.github.com>
Date: Tue, 21 Jan 2025 14:46:14 +0000
Subject: [PATCH 15/21] chore: replace omega with proper theorem

Co-authored-by: Alex Keizer <alex@keizer.dev>
---
 src/Init/Data/BitVec/Lemmas.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean
index e4d07c5cf9db..1c9d902f6375 100644
--- a/src/Init/Data/BitVec/Lemmas.lean
+++ b/src/Init/Data/BitVec/Lemmas.lean
@@ -3796,7 +3796,7 @@ theorem getElem_replicate {n w : Nat} {x : BitVec w} (h : i < w * n) :
   by_cases h' : w = 0 <;> simp [h'] <;> omega
 
 @[simp]
-theorem replicate_one {w : Nat} {x : BitVec w} (h : w = w * 1 := by omega) :
+theorem replicate_one {w : Nat} {x : BitVec w} (h : w = w * 1 := Nat.mul_one _) :
     (x.replicate 1) = x.cast h := by 
   simp [replicate, h]
 

From ded2cce606ac626dbb86c167b467cbfbe7629c15 Mon Sep 17 00:00:00 2001
From: luisacicolini <lc985@cam.ac.uk>
Date: Tue, 21 Jan 2025 15:51:30 +0000
Subject: [PATCH 16/21] chore: fix msb_replicate format

---
 src/Init/Data/BitVec/Lemmas.lean | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean
index 1c9d902f6375..47b86643cdd6 100644
--- a/src/Init/Data/BitVec/Lemmas.lean
+++ b/src/Init/Data/BitVec/Lemmas.lean
@@ -3807,8 +3807,7 @@ theorem getMsbD_replicate {n w : Nat} {x : BitVec w} :
 
 @[simp]
 theorem msb_replicate {n w : Nat} {x : BitVec w} :
-    (x.replicate n).msb =
-    (decide (0 < n) && x.msb) := by
+    (x.replicate n).msb = (decide (0 < n) && x.msb) := by
   simp only [BitVec.msb, getMsbD_replicate, Nat.zero_mod]
   cases n <;> cases w <;> simp
 

From cfd46394dade279b7a9cefa93f3b2e463d6f1c53 Mon Sep 17 00:00:00 2001
From: luisacicolini <lc985@cam.ac.uk>
Date: Tue, 21 Jan 2025 15:52:30 +0000
Subject: [PATCH 17/21] chore: fix ypothesis

---
 src/Init/Data/BitVec/Lemmas.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean
index 47b86643cdd6..1692a206c072 100644
--- a/src/Init/Data/BitVec/Lemmas.lean
+++ b/src/Init/Data/BitVec/Lemmas.lean
@@ -3796,8 +3796,8 @@ theorem getElem_replicate {n w : Nat} {x : BitVec w} (h : i < w * n) :
   by_cases h' : w = 0 <;> simp [h'] <;> omega
 
 @[simp]
-theorem replicate_one {w : Nat} {x : BitVec w} (h : w = w * 1 := Nat.mul_one _) :
-    (x.replicate 1) = x.cast h := by 
+theorem replicate_one {w : Nat} {x : BitVec w} (h : w = w * 1 := by rw [Nat.mul_one]) :
+    (x.replicate 1) = x.cast h := by
   simp [replicate, h]
 
 @[simp]

From 19c426db02ff7b898826c21fbb663a329b3edb11 Mon Sep 17 00:00:00 2001
From: luisacicolini <lc985@cam.ac.uk>
Date: Tue, 21 Jan 2025 15:53:16 +0000
Subject: [PATCH 18/21] chore: restore unneeded change

---
 src/Init/Data/BitVec/Lemmas.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean
index 1692a206c072..05f8ccc44f59 100644
--- a/src/Init/Data/BitVec/Lemmas.lean
+++ b/src/Init/Data/BitVec/Lemmas.lean
@@ -3079,7 +3079,7 @@ theorem getMsbD_rotateLeft_of_lt {n w : Nat} {x : BitVec w} (hi : r < w):
       · simp only [h₁, decide_true, Bool.true_and]
         have h₂ : (r + n) < 2 * (w + 1) := by omega
         congr 1
-        rw [← Nat.sub_mul_eq_mod_of_lt_of_le (n := 1) (by omega) (by omega)]
+        rw [← Nat.sub_mul_eq_mod_of_lt_of_le (n := 1) (by omega) (by omega), Nat.mul_one]
         omega
       · simp [h₁]
 

From 80c622ae6d489275e95392bfd8b928c01da20fa8 Mon Sep 17 00:00:00 2001
From: luisacicolini <lc985@cam.ac.uk>
Date: Tue, 21 Jan 2025 16:28:59 +0000
Subject: [PATCH 19/21] chore: nonretm simp

---
 src/Init/Data/BitVec/Lemmas.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean
index 05f8ccc44f59..c9ac8f84acc7 100644
--- a/src/Init/Data/BitVec/Lemmas.lean
+++ b/src/Init/Data/BitVec/Lemmas.lean
@@ -3783,7 +3783,7 @@ theorem getLsbD_replicate {n w : Nat} {x : BitVec w} :
     · simp only [hi, decide_true, Bool.true_and]
       by_cases hi' : i < w * n
       · simp [hi', ih]
-      · simp [hi', decide_false]
+      · simp only [hi', ↓reduceIte]
         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]

From 751f74f13aa45c23b76337c0bab83bb441e6c731 Mon Sep 17 00:00:00 2001
From: luisacicolini <lc985@cam.ac.uk>
Date: Tue, 21 Jan 2025 16:29:51 +0000
Subject: [PATCH 20/21] chore: cases instead of by_cases

---
 src/Init/Data/BitVec/Lemmas.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean
index c9ac8f84acc7..f7ecf22f42eb 100644
--- a/src/Init/Data/BitVec/Lemmas.lean
+++ b/src/Init/Data/BitVec/Lemmas.lean
@@ -3793,7 +3793,7 @@ theorem getLsbD_replicate {n w : Nat} {x : BitVec w} :
 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
+  cases w <;> simp <;> omega
 
 @[simp]
 theorem replicate_one {w : Nat} {x : BitVec w} (h : w = w * 1 := by rw [Nat.mul_one]) :

From f8f584fe1e7e691c3584d99e039c99a7bcd4dbe5 Mon Sep 17 00:00:00 2001
From: luisacicolini <lc985@cam.ac.uk>
Date: Tue, 21 Jan 2025 16:31:07 +0000
Subject: [PATCH 21/21] chore: simpler getElem proof

---
 src/Init/Data/BitVec/Lemmas.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean
index f7ecf22f42eb..8178e7c53342 100644
--- a/src/Init/Data/BitVec/Lemmas.lean
+++ b/src/Init/Data/BitVec/Lemmas.lean
@@ -3793,7 +3793,7 @@ theorem getLsbD_replicate {n w : Nat} {x : BitVec w} :
 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]
-  cases w <;> simp <;> omega
+  cases w <;> simp; omega
 
 @[simp]
 theorem replicate_one {w : Nat} {x : BitVec w} (h : w = w * 1 := by rw [Nat.mul_one]) :