From 6430f5cf8fcbbf919a697e8cfca796606c8bc7ed Mon Sep 17 00:00:00 2001
From: luisacicolini <lc985@cam.ac.uk>
Date: Thu, 23 Jan 2025 16:11:02 +0000
Subject: [PATCH 01/33] feat: dumbest statements I could think of

---
 src/Init/Data/BitVec/Lemmas.lean | 28 +++++++++++++++++++++++++++-
 1 file changed, 27 insertions(+), 1 deletion(-)

diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean
index 1881887062f2..45fdc4c97e1f 100644
--- a/src/Init/Data/BitVec/Lemmas.lean
+++ b/src/Init/Data/BitVec/Lemmas.lean
@@ -781,6 +781,20 @@ protected theorem extractLsb_ofNat (x n : Nat) (hi lo : Nat) :
     (extractLsb' start len x).getLsbD i = (i < len && x.getLsbD (start+i)) := by
   simp [getLsbD, Nat.lt_succ]
 
+@[simp] theorem getMsbD_extractLsb' (start len : Nat) (x : BitVec w) (i : Nat) :
+    (extractLsb' start len x).getMsbD i =
+    (decide (i < len) &&
+    (decide (len - 1 - i < len) &&
+    (decide (start + (len - 1 - i) < w) && x.getMsbD (w - 1 - (start + (len - 1 - i)))))) := by
+  rw [getMsbD_eq_getLsbD, getLsbD_extractLsb', getLsbD_eq_getMsbD]
+
+@[simp] theorem msb_extractLsb' (start len : Nat) (x : BitVec w) :
+    (extractLsb' start len x).msb =
+    (decide (0 < len) &&
+    (decide (len - 1 - 0 < len) &&
+    (decide (start + (len - 1 - 0) < w) && x.getMsbD (w - 1 - (start + (len - 1 - 0))))))  := by
+  rw [BitVec.msb, BitVec.getMsbD_extractLsb']
+
 @[simp] theorem getElem_extract {hi lo : Nat} {x : BitVec n} {i : Nat} (h : i < hi - lo + 1) :
     (extractLsb hi lo x)[i] = getLsbD x (lo+i) := by
   simp [getElem_eq_testBit_toNat, getLsbD, h]
@@ -789,6 +803,18 @@ protected theorem extractLsb_ofNat (x n : Nat) (hi lo : Nat) :
     getLsbD (extractLsb hi lo x) i = (i ≤ (hi-lo) && getLsbD x (lo+i)) := by
   simp [getLsbD, Nat.lt_succ]
 
+@[simp] theorem getMsbD_extract (hi lo : Nat) (x : BitVec n) (i : Nat) :
+    (extractLsb hi lo x).getMsbD i = (decide (i < hi - lo + 1) &&
+    (decide (hi - lo - i ≤ hi - lo) &&
+    (decide (lo + (hi - lo - i) < n) && x.getMsbD (n - 1 - (lo + (hi - lo - i)))))) := by
+  rw [getMsbD_eq_getLsbD, getLsbD_extract, getLsbD_eq_getMsbD, Nat.add_sub_cancel]
+
+@[simp] theorem msb_extract (hi lo : Nat) (x : BitVec n) :
+    (extractLsb hi lo x).msb = (decide (0 < hi - lo + 1) &&
+    (decide (hi - lo ≤ hi - lo) &&
+    (decide (lo + (hi - lo) < n) && x.getMsbD (n - 1 - (lo + (hi - lo)))))) := by
+  rw [BitVec.msb, BitVec.getMsbD_extract, Nat.sub_zero]
+
 theorem extractLsb'_eq_extractLsb {w : Nat} (x : BitVec w) (start len : Nat) (h : len > 0) :
     x.extractLsb' start len = (x.extractLsb (len - 1 + start) start).cast (by omega) := by
   apply eq_of_toNat_eq
@@ -3352,7 +3378,7 @@ theorem shiftLeft_eq_mul_twoPow (x : BitVec w) (n : Nat) :
   simp [getLsbD_shiftLeft, Fin.is_lt, decide_true, Bool.true_and, mul_twoPow_eq_shiftLeft]
 
 /-- 2^i * 2^j = 2^(i + j) with bitvectors as well -/
-theorem twoPow_mul_twoPow_eq {w : Nat} (i j : Nat) : twoPow w i * twoPow w j = twoPow w (i + j) := by 
+theorem twoPow_mul_twoPow_eq {w : Nat} (i j : Nat) : twoPow w i * twoPow w j = twoPow w (i + j) := by
   apply BitVec.eq_of_toNat_eq
   simp only [toNat_mul, toNat_twoPow]
   rw [← Nat.mul_mod, Nat.pow_add]

From 4f2605e1cb31477a7f4326739f449c80ac8b93b6 Mon Sep 17 00:00:00 2001
From: luisacicolini <lc985@cam.ac.uk>
Date: Thu, 23 Jan 2025 16:26:52 +0000
Subject: [PATCH 02/33] simplification

---
 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 45fdc4c97e1f..0d6db33c390e 100644
--- a/src/Init/Data/BitVec/Lemmas.lean
+++ b/src/Init/Data/BitVec/Lemmas.lean
@@ -811,9 +811,8 @@ protected theorem extractLsb_ofNat (x n : Nat) (hi lo : Nat) :
 
 @[simp] theorem msb_extract (hi lo : Nat) (x : BitVec n) :
     (extractLsb hi lo x).msb = (decide (0 < hi - lo + 1) &&
-    (decide (hi - lo ≤ hi - lo) &&
-    (decide (lo + (hi - lo) < n) && x.getMsbD (n - 1 - (lo + (hi - lo)))))) := by
-  rw [BitVec.msb, BitVec.getMsbD_extract, Nat.sub_zero]
+    (decide (lo + (hi - lo) < n) && x.getMsbD (n - 1 - (lo + (hi - lo))))) := by
+  simp [show hi - lo ≤ hi - lo by omega, BitVec.msb, BitVec.getMsbD_extract, Nat.sub_zero]
 
 theorem extractLsb'_eq_extractLsb {w : Nat} (x : BitVec w) (start len : Nat) (h : len > 0) :
     x.extractLsb' start len = (x.extractLsb (len - 1 + start) start).cast (by omega) := by

From 30d6f28777af1fe9eb3b77d0902e0fe71eda14a8 Mon Sep 17 00:00:00 2001
From: luisacicolini <lc985@cam.ac.uk>
Date: Fri, 24 Jan 2025 08:49:06 +0000
Subject: [PATCH 03/33] chore: simplify dumb statements

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

diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean
index 0d6db33c390e..0bb016dcf564 100644
--- a/src/Init/Data/BitVec/Lemmas.lean
+++ b/src/Init/Data/BitVec/Lemmas.lean
@@ -790,10 +790,9 @@ protected theorem extractLsb_ofNat (x n : Nat) (hi lo : Nat) :
 
 @[simp] theorem msb_extractLsb' (start len : Nat) (x : BitVec w) :
     (extractLsb' start len x).msb =
-    (decide (0 < len) &&
-    (decide (len - 1 - 0 < len) &&
-    (decide (start + (len - 1 - 0) < w) && x.getMsbD (w - 1 - (start + (len - 1 - 0))))))  := by
-  rw [BitVec.msb, BitVec.getMsbD_extractLsb']
+    (decide (0 < len) && (decide (start + (len - 1) < w)
+    && x.getMsbD (w - 1 - (start + (len - 1))))) := by
+  simp [BitVec.msb, BitVec.getMsbD_extractLsb', Nat.sub_zero, show (len - 1 < len) = (0 < len) by simp; omega]
 
 @[simp] theorem getElem_extract {hi lo : Nat} {x : BitVec n} {i : Nat} (h : i < hi - lo + 1) :
     (extractLsb hi lo x)[i] = getLsbD x (lo+i) := by

From 98c4afb6ef2d27ac80b93be4bf2ec6e98cd76dcb Mon Sep 17 00:00:00 2001
From: luisacicolini <lc985@cam.ac.uk>
Date: Fri, 24 Jan 2025 14:20:42 +0000
Subject: [PATCH 04/33] progress

---
 src/Init/Data/BitVec/Lemmas.lean | 17 ++++++++++-------
 1 file changed, 10 insertions(+), 7 deletions(-)

diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean
index 0bb016dcf564..1fa3031815e4 100644
--- a/src/Init/Data/BitVec/Lemmas.lean
+++ b/src/Init/Data/BitVec/Lemmas.lean
@@ -784,15 +784,17 @@ protected theorem extractLsb_ofNat (x n : Nat) (hi lo : Nat) :
 @[simp] theorem getMsbD_extractLsb' (start len : Nat) (x : BitVec w) (i : Nat) :
     (extractLsb' start len x).getMsbD i =
     (decide (i < len) &&
-    (decide (len - 1 - i < len) &&
-    (decide (start + (len - 1 - i) < w) && x.getMsbD (w - 1 - (start + (len - 1 - i)))))) := by
-  rw [getMsbD_eq_getLsbD, getLsbD_extractLsb', getLsbD_eq_getMsbD]
+    decide (start + (len - 1 - i) < w) && x.getMsbD (w - 1 - (start + (len - 1 - i)))) := by
+  rcases len with _|len'
+  · simp
+  · rw [getMsbD_eq_getLsbD, getLsbD_extractLsb', getLsbD_eq_getMsbD, Nat.sub_add_eq]
+    have := @Nat.sub_lt_add_one (a := len') (b := i)
+    simp only [Nat.add_one_sub_one, this, decide_true, Bool.true_and, Bool.and_assoc]
 
 @[simp] theorem msb_extractLsb' (start len : Nat) (x : BitVec w) :
     (extractLsb' start len x).msb =
-    (decide (0 < len) && (decide (start + (len - 1) < w)
-    && x.getMsbD (w - 1 - (start + (len - 1))))) := by
-  simp [BitVec.msb, BitVec.getMsbD_extractLsb', Nat.sub_zero, show (len - 1 < len) = (0 < len) by simp; omega]
+    (decide (0 < len) && (decide (start + (len - 1) < w) && x.getMsbD (w - 1 - (start + (len - 1))))) := by
+  simp [BitVec.msb, BitVec.getMsbD_extractLsb', Nat.sub_zero, show (len - 1 < len) = (0 < len) by simp; omega, Bool.and_assoc]
 
 @[simp] theorem getElem_extract {hi lo : Nat} {x : BitVec n} {i : Nat} (h : i < hi - lo + 1) :
     (extractLsb hi lo x)[i] = getLsbD x (lo+i) := by
@@ -803,7 +805,8 @@ protected theorem extractLsb_ofNat (x n : Nat) (hi lo : Nat) :
   simp [getLsbD, Nat.lt_succ]
 
 @[simp] theorem getMsbD_extract (hi lo : Nat) (x : BitVec n) (i : Nat) :
-    (extractLsb hi lo x).getMsbD i = (decide (i < hi - lo + 1) &&
+    (extractLsb hi lo x).getMsbD i =
+    (decide (i < hi - lo + 1) &&
     (decide (hi - lo - i ≤ hi - lo) &&
     (decide (lo + (hi - lo - i) < n) && x.getMsbD (n - 1 - (lo + (hi - lo - i)))))) := by
   rw [getMsbD_eq_getLsbD, getLsbD_extract, getLsbD_eq_getMsbD, Nat.add_sub_cancel]

From 20a6ca8998d4399a045af8687380d3d201bd2d3c Mon Sep 17 00:00:00 2001
From: luisacicolini <lc985@cam.ac.uk>
Date: Mon, 27 Jan 2025 11:59:21 +0000
Subject: [PATCH 05/33] chore: proofs done

---
 src/Init/Data/BitVec/Lemmas.lean | 35 ++++++++++++++++++++------------
 1 file changed, 22 insertions(+), 13 deletions(-)

diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean
index 1fa3031815e4..5b915ee8eaf8 100644
--- a/src/Init/Data/BitVec/Lemmas.lean
+++ b/src/Init/Data/BitVec/Lemmas.lean
@@ -781,20 +781,31 @@ protected theorem extractLsb_ofNat (x n : Nat) (hi lo : Nat) :
     (extractLsb' start len x).getLsbD i = (i < len && x.getLsbD (start+i)) := by
   simp [getLsbD, Nat.lt_succ]
 
-@[simp] theorem getMsbD_extractLsb' (start len : Nat) (x : BitVec w) (i : Nat) :
+@[simp] theorem getMsbD_extractLsb'_eq_getLsbD {start len : Nat} {x : BitVec w} {i : Nat} :
+    (extractLsb' start len x).getMsbD i =
+    (decide (i < len) && x.getLsbD (start + (len - 1 - i))) := by
+  rcases len with _|len'
+  · simp
+  · have h : len' + 1 - 1 - i < len' + 1 := by omega
+    rw [BitVec.getMsbD_eq_getLsbD, BitVec.getLsbD_extractLsb']
+    simp [h, show len' - i < len' + 1 by omega]
+
+@[simp] theorem getMsbD_extractLsb' {start len : Nat} {x : BitVec w} {i : Nat} :
     (extractLsb' start len x).getMsbD i =
     (decide (i < len) &&
-    decide (start + (len - 1 - i) < w) && x.getMsbD (w - 1 - (start + (len - 1 - i)))) := by
+    (decide (start + (len - 1 - i) < w) && x.getMsbD (w - 1 - (start + (len - 1 - i))))) := by
   rcases len with _|len'
   · simp
-  · rw [getMsbD_eq_getLsbD, getLsbD_extractLsb', getLsbD_eq_getMsbD, Nat.sub_add_eq]
-    have := @Nat.sub_lt_add_one (a := len') (b := i)
-    simp only [Nat.add_one_sub_one, this, decide_true, Bool.true_and, Bool.and_assoc]
+  · have h : (len' - i < len' + 1) := by omega
+    rw [getMsbD_eq_getLsbD, getLsbD_extractLsb', getLsbD_eq_getMsbD]
+    simp [h]
 
-@[simp] theorem msb_extractLsb' (start len : Nat) (x : BitVec w) :
+@[simp] theorem msb_extractLsb' {start len : Nat} {x : BitVec w} :
     (extractLsb' start len x).msb =
-    (decide (0 < len) && (decide (start + (len - 1) < w) && x.getMsbD (w - 1 - (start + (len - 1))))) := by
-  simp [BitVec.msb, BitVec.getMsbD_extractLsb', Nat.sub_zero, show (len - 1 < len) = (0 < len) by simp; omega, Bool.and_assoc]
+    (decide (0 < len) && x.getLsbD (start + len - 1)) := by
+  rcases len with _|len'
+  · simp [BitVec.extractLsb', BitVec.msb]
+  · simp [BitVec.msb, BitVec.getMsbD_extractLsb', ← Nat.add_assoc]
 
 @[simp] theorem getElem_extract {hi lo : Nat} {x : BitVec n} {i : Nat} (h : i < hi - lo + 1) :
     (extractLsb hi lo x)[i] = getLsbD x (lo+i) := by
@@ -804,12 +815,10 @@ protected theorem extractLsb_ofNat (x n : Nat) (hi lo : Nat) :
     getLsbD (extractLsb hi lo x) i = (i ≤ (hi-lo) && getLsbD x (lo+i)) := by
   simp [getLsbD, Nat.lt_succ]
 
-@[simp] theorem getMsbD_extract (hi lo : Nat) (x : BitVec n) (i : Nat) :
+@[simp] theorem getMsbD_extract (hi lo : Nat) (x : BitVec w) (i : Nat) :
     (extractLsb hi lo x).getMsbD i =
-    (decide (i < hi - lo + 1) &&
-    (decide (hi - lo - i ≤ hi - lo) &&
-    (decide (lo + (hi - lo - i) < n) && x.getMsbD (n - 1 - (lo + (hi - lo - i)))))) := by
-  rw [getMsbD_eq_getLsbD, getLsbD_extract, getLsbD_eq_getMsbD, Nat.add_sub_cancel]
+    (decide (i < hi - lo + 1) && (decide (lo + (hi - lo - i) < w) && x.getMsbD (w - 1 - (lo + (hi - lo - i))))) := by
+  rw [BitVec.extractLsb, BitVec.getMsbD_extractLsb', Nat.add_sub_cancel]
 
 @[simp] theorem msb_extract (hi lo : Nat) (x : BitVec n) :
     (extractLsb hi lo x).msb = (decide (0 < hi - lo + 1) &&

From 84fed64489be13ddba178aefe93db0a4292e273c Mon Sep 17 00:00:00 2001
From: luisacicolini <lc985@cam.ac.uk>
Date: Mon, 27 Jan 2025 12:02:45 +0000
Subject: [PATCH 06/33] chore: proofs done

---
 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 5b915ee8eaf8..89a947cb910c 100644
--- a/src/Init/Data/BitVec/Lemmas.lean
+++ b/src/Init/Data/BitVec/Lemmas.lean
@@ -815,12 +815,12 @@ protected theorem extractLsb_ofNat (x n : Nat) (hi lo : Nat) :
     getLsbD (extractLsb hi lo x) i = (i ≤ (hi-lo) && getLsbD x (lo+i)) := by
   simp [getLsbD, Nat.lt_succ]
 
-@[simp] theorem getMsbD_extract (hi lo : Nat) (x : BitVec w) (i : Nat) :
+@[simp] theorem getMsbD_extract {hi lo : Nat} {x : BitVec w} {i : Nat} :
     (extractLsb hi lo x).getMsbD i =
     (decide (i < hi - lo + 1) && (decide (lo + (hi - lo - i) < w) && x.getMsbD (w - 1 - (lo + (hi - lo - i))))) := by
   rw [BitVec.extractLsb, BitVec.getMsbD_extractLsb', Nat.add_sub_cancel]
 
-@[simp] theorem msb_extract (hi lo : Nat) (x : BitVec n) :
+@[simp] theorem msb_extract {hi lo : Nat} {x : BitVec n} :
     (extractLsb hi lo x).msb = (decide (0 < hi - lo + 1) &&
     (decide (lo + (hi - lo) < n) && x.getMsbD (n - 1 - (lo + (hi - lo))))) := by
   simp [show hi - lo ≤ hi - lo by omega, BitVec.msb, BitVec.getMsbD_extract, Nat.sub_zero]

From 0b9c3774b7d695fce80de6dd1b4dcee0f031e0ed Mon Sep 17 00:00:00 2001
From: Luisa Cicolini <48860705+luisacicolini@users.noreply.github.com>
Date: Wed, 29 Jan 2025 11:38:45 +0000
Subject: [PATCH 07/33] chore: update names

Co-authored-by: Siddharth <siddu.druid@gmail.com>
---
 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 89a947cb910c..227258101eaa 100644
--- a/src/Init/Data/BitVec/Lemmas.lean
+++ b/src/Init/Data/BitVec/Lemmas.lean
@@ -815,7 +815,7 @@ protected theorem extractLsb_ofNat (x n : Nat) (hi lo : Nat) :
     getLsbD (extractLsb hi lo x) i = (i ≤ (hi-lo) && getLsbD x (lo+i)) := by
   simp [getLsbD, Nat.lt_succ]
 
-@[simp] theorem getMsbD_extract {hi lo : Nat} {x : BitVec w} {i : Nat} :
+@[simp] theorem getMsbD_extractLsb {hi lo : Nat} {x : BitVec w} {i : Nat} :
     (extractLsb hi lo x).getMsbD i =
     (decide (i < hi - lo + 1) && (decide (lo + (hi - lo - i) < w) && x.getMsbD (w - 1 - (lo + (hi - lo - i))))) := by
   rw [BitVec.extractLsb, BitVec.getMsbD_extractLsb', Nat.add_sub_cancel]

From 58b6f1a3963b995d262c6d14b07f5b54ebe08c42 Mon Sep 17 00:00:00 2001
From: Luisa Cicolini <48860705+luisacicolini@users.noreply.github.com>
Date: Wed, 29 Jan 2025 11:38:55 +0000
Subject: [PATCH 08/33] chore: update names

Co-authored-by: Siddharth <siddu.druid@gmail.com>
---
 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 227258101eaa..954845c154ac 100644
--- a/src/Init/Data/BitVec/Lemmas.lean
+++ b/src/Init/Data/BitVec/Lemmas.lean
@@ -820,7 +820,7 @@ protected theorem extractLsb_ofNat (x n : Nat) (hi lo : Nat) :
     (decide (i < hi - lo + 1) && (decide (lo + (hi - lo - i) < w) && x.getMsbD (w - 1 - (lo + (hi - lo - i))))) := by
   rw [BitVec.extractLsb, BitVec.getMsbD_extractLsb', Nat.add_sub_cancel]
 
-@[simp] theorem msb_extract {hi lo : Nat} {x : BitVec n} :
+@[simp] theorem msb_extractLsb {hi lo : Nat} {x : BitVec n} :
     (extractLsb hi lo x).msb = (decide (0 < hi - lo + 1) &&
     (decide (lo + (hi - lo) < n) && x.getMsbD (n - 1 - (lo + (hi - lo))))) := by
   simp [show hi - lo ≤ hi - lo by omega, BitVec.msb, BitVec.getMsbD_extract, Nat.sub_zero]

From 619a901910a3e572f238c72c99e6493eb317a6f5 Mon Sep 17 00:00:00 2001
From: luisacicolini <lc985@cam.ac.uk>
Date: Wed, 29 Jan 2025 13:04:13 +0000
Subject: [PATCH 09/33] chore: simplify msb_extractLsb git push

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

diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean
index 954845c154ac..de29a0c0f042 100644
--- a/src/Init/Data/BitVec/Lemmas.lean
+++ b/src/Init/Data/BitVec/Lemmas.lean
@@ -781,31 +781,22 @@ protected theorem extractLsb_ofNat (x n : Nat) (hi lo : Nat) :
     (extractLsb' start len x).getLsbD i = (i < len && x.getLsbD (start+i)) := by
   simp [getLsbD, Nat.lt_succ]
 
-@[simp] theorem getMsbD_extractLsb'_eq_getLsbD {start len : Nat} {x : BitVec w} {i : Nat} :
-    (extractLsb' start len x).getMsbD i =
-    (decide (i < len) && x.getLsbD (start + (len - 1 - i))) := by
-  rcases len with _|len'
-  · simp
-  · have h : len' + 1 - 1 - i < len' + 1 := by omega
-    rw [BitVec.getMsbD_eq_getLsbD, BitVec.getLsbD_extractLsb']
-    simp [h, show len' - i < len' + 1 by omega]
-
 @[simp] theorem getMsbD_extractLsb' {start len : Nat} {x : BitVec w} {i : Nat} :
     (extractLsb' start len x).getMsbD i =
     (decide (i < len) &&
     (decide (start + (len - 1 - i) < w) && x.getMsbD (w - 1 - (start + (len - 1 - i))))) := by
-  rcases len with _|len'
+  rcases len with rfl | len
   · simp
-  · have h : (len' - i < len' + 1) := by omega
+  · have h : (len - i < len + 1) := by omega
     rw [getMsbD_eq_getLsbD, getLsbD_extractLsb', getLsbD_eq_getMsbD]
     simp [h]
 
 @[simp] theorem msb_extractLsb' {start len : Nat} {x : BitVec w} :
     (extractLsb' start len x).msb =
     (decide (0 < len) && x.getLsbD (start + len - 1)) := by
-  rcases len with _|len'
+  rcases len with rfl | len
   · simp [BitVec.extractLsb', BitVec.msb]
-  · simp [BitVec.msb, BitVec.getMsbD_extractLsb', ← Nat.add_assoc]
+  · simp [BitVec.msb, BitVec.getMsbD_eq_getLsbD, BitVec.getLsbD_extractLsb', ← Nat.add_assoc]
 
 @[simp] theorem getElem_extract {hi lo : Nat} {x : BitVec n} {i : Nat} (h : i < hi - lo + 1) :
     (extractLsb hi lo x)[i] = getLsbD x (lo+i) := by
@@ -823,7 +814,7 @@ protected theorem extractLsb_ofNat (x n : Nat) (hi lo : Nat) :
 @[simp] theorem msb_extractLsb {hi lo : Nat} {x : BitVec n} :
     (extractLsb hi lo x).msb = (decide (0 < hi - lo + 1) &&
     (decide (lo + (hi - lo) < n) && x.getMsbD (n - 1 - (lo + (hi - lo))))) := by
-  simp [show hi - lo ≤ hi - lo by omega, BitVec.msb, BitVec.getMsbD_extract, Nat.sub_zero]
+  simp [show hi - lo ≤ hi - lo by omega, BitVec.msb, BitVec.getMsbD_extractLsb, Nat.sub_zero]
 
 theorem extractLsb'_eq_extractLsb {w : Nat} (x : BitVec w) (start len : Nat) (h : len > 0) :
     x.extractLsb' start len = (x.extractLsb (len - 1 + start) start).cast (by omega) := by

From 83090773851a7bc3f8b1eec24e021b1a94dcc2c4 Mon Sep 17 00:00:00 2001
From: Luisa Cicolini <48860705+luisacicolini@users.noreply.github.com>
Date: Wed, 29 Jan 2025 13:06:31 +0000
Subject: [PATCH 10/33] chore: undo

---
 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 de29a0c0f042..8a33f2664ff4 100644
--- a/src/Init/Data/BitVec/Lemmas.lean
+++ b/src/Init/Data/BitVec/Lemmas.lean
@@ -3379,7 +3379,7 @@ theorem shiftLeft_eq_mul_twoPow (x : BitVec w) (n : Nat) :
   simp [getLsbD_shiftLeft, Fin.is_lt, decide_true, Bool.true_and, mul_twoPow_eq_shiftLeft]
 
 /-- 2^i * 2^j = 2^(i + j) with bitvectors as well -/
-theorem twoPow_mul_twoPow_eq {w : Nat} (i j : Nat) : twoPow w i * twoPow w j = twoPow w (i + j) := by
+theorem twoPow_mul_twoPow_eq {w : Nat} (i j : Nat) : twoPow w i * twoPow w j = twoPow w (i + j) := by 
   apply BitVec.eq_of_toNat_eq
   simp only [toNat_mul, toNat_twoPow]
   rw [← Nat.mul_mod, Nat.pow_add]

From da80f4dc5b504dccdcbf88e503979a3cd44ec332 Mon Sep 17 00:00:00 2001
From: luisacicolini <lc985@cam.ac.uk>
Date: Wed, 29 Jan 2025 14:23:33 +0000
Subject: [PATCH 11/33] chore: simplify msb_extractLsb

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

diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean
index 8a33f2664ff4..2875f812c9e9 100644
--- a/src/Init/Data/BitVec/Lemmas.lean
+++ b/src/Init/Data/BitVec/Lemmas.lean
@@ -811,10 +811,10 @@ protected theorem extractLsb_ofNat (x n : Nat) (hi lo : Nat) :
     (decide (i < hi - lo + 1) && (decide (lo + (hi - lo - i) < w) && x.getMsbD (w - 1 - (lo + (hi - lo - i))))) := by
   rw [BitVec.extractLsb, BitVec.getMsbD_extractLsb', Nat.add_sub_cancel]
 
-@[simp] theorem msb_extractLsb {hi lo : Nat} {x : BitVec n} :
-    (extractLsb hi lo x).msb = (decide (0 < hi - lo + 1) &&
-    (decide (lo + (hi - lo) < n) && x.getMsbD (n - 1 - (lo + (hi - lo))))) := by
-  simp [show hi - lo ≤ hi - lo by omega, BitVec.msb, BitVec.getMsbD_extractLsb, Nat.sub_zero]
+@[simp] theorem msb_extractLsb {hi lo : Nat} {x : BitVec w} :
+    (extractLsb hi lo x).msb =
+    (decide (lo + (hi - lo) < w) && x.getMsbD (w - 1 - (lo + (hi - lo)))) := by
+  simp [BitVec.msb, BitVec.getMsbD_extractLsb, show hi - lo ≤ hi - lo by omega]
 
 theorem extractLsb'_eq_extractLsb {w : Nat} (x : BitVec w) (start len : Nat) (h : len > 0) :
     x.extractLsb' start len = (x.extractLsb (len - 1 + start) start).cast (by omega) := by

From be7f0b8c52e1d6e55749a3ec0742b4b7a14057a9 Mon Sep 17 00:00:00 2001
From: Luisa Cicolini <48860705+luisacicolini@users.noreply.github.com>
Date: Thu, 30 Jan 2025 19:54:02 +0000
Subject: [PATCH 12/33] chore: format cases

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 2875f812c9e9..7790e22a14c2 100644
--- a/src/Init/Data/BitVec/Lemmas.lean
+++ b/src/Init/Data/BitVec/Lemmas.lean
@@ -794,7 +794,7 @@ protected theorem extractLsb_ofNat (x n : Nat) (hi lo : Nat) :
 @[simp] theorem msb_extractLsb' {start len : Nat} {x : BitVec w} :
     (extractLsb' start len x).msb =
     (decide (0 < len) && x.getLsbD (start + len - 1)) := by
-  rcases len with rfl | len
+  cases len
   · simp [BitVec.extractLsb', BitVec.msb]
   · simp [BitVec.msb, BitVec.getMsbD_eq_getLsbD, BitVec.getLsbD_extractLsb', ← Nat.add_assoc]
 

From ce00480c6d0025427ac0583203736602a8f2109f Mon Sep 17 00:00:00 2001
From: luisacicolini <lc985@cam.ac.uk>
Date: Thu, 30 Jan 2025 20:02:30 +0000
Subject: [PATCH 13/33] chore: format

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

diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean
index 7790e22a14c2..3f7890cea133 100644
--- a/src/Init/Data/BitVec/Lemmas.lean
+++ b/src/Init/Data/BitVec/Lemmas.lean
@@ -782,8 +782,8 @@ protected theorem extractLsb_ofNat (x n : Nat) (hi lo : Nat) :
   simp [getLsbD, Nat.lt_succ]
 
 @[simp] theorem getMsbD_extractLsb' {start len : Nat} {x : BitVec w} {i : Nat} :
-    (extractLsb' start len x).getMsbD i =
-    (decide (i < len) &&
+    (extractLsb' start len x).getMsbD i
+    = (decide (i < len) &&
     (decide (start + (len - 1 - i) < w) && x.getMsbD (w - 1 - (start + (len - 1 - i))))) := by
   rcases len with rfl | len
   · simp
@@ -792,8 +792,8 @@ protected theorem extractLsb_ofNat (x n : Nat) (hi lo : Nat) :
     simp [h]
 
 @[simp] theorem msb_extractLsb' {start len : Nat} {x : BitVec w} :
-    (extractLsb' start len x).msb =
-    (decide (0 < len) && x.getLsbD (start + len - 1)) := by
+    (extractLsb' start len x).msb
+    = (decide (0 < len) && x.getLsbD (start + len - 1)) := by
   cases len
   · simp [BitVec.extractLsb', BitVec.msb]
   · simp [BitVec.msb, BitVec.getMsbD_eq_getLsbD, BitVec.getLsbD_extractLsb', ← Nat.add_assoc]
@@ -807,13 +807,15 @@ protected theorem extractLsb_ofNat (x n : Nat) (hi lo : Nat) :
   simp [getLsbD, Nat.lt_succ]
 
 @[simp] theorem getMsbD_extractLsb {hi lo : Nat} {x : BitVec w} {i : Nat} :
-    (extractLsb hi lo x).getMsbD i =
-    (decide (i < hi - lo + 1) && (decide (lo + (hi - lo - i) < w) && x.getMsbD (w - 1 - (lo + (hi - lo - i))))) := by
+    (extractLsb hi lo x).getMsbD i
+    = (decide (i < hi - lo + 1)
+      && (decide (lo + (hi - lo - i) < w)
+      && x.getMsbD (w - 1 - (lo + (hi - lo - i))))) := by
   rw [BitVec.extractLsb, BitVec.getMsbD_extractLsb', Nat.add_sub_cancel]
 
 @[simp] theorem msb_extractLsb {hi lo : Nat} {x : BitVec w} :
-    (extractLsb hi lo x).msb =
-    (decide (lo + (hi - lo) < w) && x.getMsbD (w - 1 - (lo + (hi - lo)))) := by
+    (extractLsb hi lo x).msb
+    = (decide (lo + (hi - lo) < w) && x.getMsbD (w - 1 - (lo + (hi - lo)))) := by
   simp [BitVec.msb, BitVec.getMsbD_extractLsb, show hi - lo ≤ hi - lo by omega]
 
 theorem extractLsb'_eq_extractLsb {w : Nat} (x : BitVec w) (start len : Nat) (h : len > 0) :
@@ -3379,7 +3381,7 @@ theorem shiftLeft_eq_mul_twoPow (x : BitVec w) (n : Nat) :
   simp [getLsbD_shiftLeft, Fin.is_lt, decide_true, Bool.true_and, mul_twoPow_eq_shiftLeft]
 
 /-- 2^i * 2^j = 2^(i + j) with bitvectors as well -/
-theorem twoPow_mul_twoPow_eq {w : Nat} (i j : Nat) : twoPow w i * twoPow w j = twoPow w (i + j) := by 
+theorem twoPow_mul_twoPow_eq {w : Nat} (i j : Nat) : twoPow w i * twoPow w j = twoPow w (i + j) := by
   apply BitVec.eq_of_toNat_eq
   simp only [toNat_mul, toNat_twoPow]
   rw [← Nat.mul_mod, Nat.pow_add]

From 38fe8a82631c53de87dd03ac8921154b017d848e Mon Sep 17 00:00:00 2001
From: Siddharth <siddu.druid@gmail.com>
Date: Thu, 30 Jan 2025 22:51:48 +0000
Subject: [PATCH 14/33] Update src/Init/Data/BitVec/Lemmas.lean

---
 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 3f7890cea133..b472b2bb4f68 100644
--- a/src/Init/Data/BitVec/Lemmas.lean
+++ b/src/Init/Data/BitVec/Lemmas.lean
@@ -3381,7 +3381,7 @@ theorem shiftLeft_eq_mul_twoPow (x : BitVec w) (n : Nat) :
   simp [getLsbD_shiftLeft, Fin.is_lt, decide_true, Bool.true_and, mul_twoPow_eq_shiftLeft]
 
 /-- 2^i * 2^j = 2^(i + j) with bitvectors as well -/
-theorem twoPow_mul_twoPow_eq {w : Nat} (i j : Nat) : twoPow w i * twoPow w j = twoPow w (i + j) := by
+theorem twoPow_mul_twoPow_eq {w : Nat} (i j : Nat) : twoPow w i * twoPow w j = twoPow w (i + j) := by 
   apply BitVec.eq_of_toNat_eq
   simp only [toNat_mul, toNat_twoPow]
   rw [← Nat.mul_mod, Nat.pow_add]

From cb775b7e7659aebbd1df6f0c58f4fe4ccf2e5561 Mon Sep 17 00:00:00 2001
From: luisacicolini <lc985@cam.ac.uk>
Date: Mon, 3 Feb 2025 08:45:17 +0000
Subject: [PATCH 15/33] chore: fix comments

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

diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean
index b472b2bb4f68..753d634a7529 100644
--- a/src/Init/Data/BitVec/Lemmas.lean
+++ b/src/Init/Data/BitVec/Lemmas.lean
@@ -808,15 +808,15 @@ protected theorem extractLsb_ofNat (x n : Nat) (hi lo : Nat) :
 
 @[simp] theorem getMsbD_extractLsb {hi lo : Nat} {x : BitVec w} {i : Nat} :
     (extractLsb hi lo x).getMsbD i
-    = (decide (i < hi - lo + 1)
+    = (decide (i ≤  hi - lo)
       && (decide (lo + (hi - lo - i) < w)
       && x.getMsbD (w - 1 - (lo + (hi - lo - i))))) := by
-  rw [BitVec.extractLsb, BitVec.getMsbD_extractLsb', Nat.add_sub_cancel]
+  simp [BitVec.extractLsb, BitVec.getMsbD_extractLsb', Nat.add_sub_cancel, Nat.lt_add_one_iff (m := i) (n := (hi - lo))]
 
 @[simp] theorem msb_extractLsb {hi lo : Nat} {x : BitVec w} :
     (extractLsb hi lo x).msb
     = (decide (lo + (hi - lo) < w) && x.getMsbD (w - 1 - (lo + (hi - lo)))) := by
-  simp [BitVec.msb, BitVec.getMsbD_extractLsb, show hi - lo ≤ hi - lo by omega]
+  simp [BitVec.msb, BitVec.getMsbD_extractLsb]
 
 theorem extractLsb'_eq_extractLsb {w : Nat} (x : BitVec w) (start len : Nat) (h : len > 0) :
     x.extractLsb' start len = (x.extractLsb (len - 1 + start) start).cast (by omega) := by
@@ -3381,7 +3381,7 @@ theorem shiftLeft_eq_mul_twoPow (x : BitVec w) (n : Nat) :
   simp [getLsbD_shiftLeft, Fin.is_lt, decide_true, Bool.true_and, mul_twoPow_eq_shiftLeft]
 
 /-- 2^i * 2^j = 2^(i + j) with bitvectors as well -/
-theorem twoPow_mul_twoPow_eq {w : Nat} (i j : Nat) : twoPow w i * twoPow w j = twoPow w (i + j) := by 
+theorem twoPow_mul_twoPow_eq {w : Nat} (i j : Nat) : twoPow w i * twoPow w j = twoPow w (i + j) := by
   apply BitVec.eq_of_toNat_eq
   simp only [toNat_mul, toNat_twoPow]
   rw [← Nat.mul_mod, Nat.pow_add]

From 243d6af28a1dead00699d313e52e32889da29789 Mon Sep 17 00:00:00 2001
From: luisacicolini <lc985@cam.ac.uk>
Date: Mon, 3 Feb 2025 08:47:06 +0000
Subject: [PATCH 16/33] chore: remove unwanted chnge

---
 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 753d634a7529..e310f060da2f 100644
--- a/src/Init/Data/BitVec/Lemmas.lean
+++ b/src/Init/Data/BitVec/Lemmas.lean
@@ -3381,7 +3381,7 @@ theorem shiftLeft_eq_mul_twoPow (x : BitVec w) (n : Nat) :
   simp [getLsbD_shiftLeft, Fin.is_lt, decide_true, Bool.true_and, mul_twoPow_eq_shiftLeft]
 
 /-- 2^i * 2^j = 2^(i + j) with bitvectors as well -/
-theorem twoPow_mul_twoPow_eq {w : Nat} (i j : Nat) : twoPow w i * twoPow w j = twoPow w (i + j) := by
+theorem twoPow_mul_twoPow_eq {w : Nat} (i j : Nat) : twoPow w i * twoPow w j = twoPow w (i + j) := by 
   apply BitVec.eq_of_toNat_eq
   simp only [toNat_mul, toNat_twoPow]
   rw [← Nat.mul_mod, Nat.pow_add]

From 4c916687fe8b04d2a1acca5bb480bc57bb272e16 Mon Sep 17 00:00:00 2001
From: luisacicolini <lc985@cam.ac.uk>
Date: Mon, 3 Feb 2025 09:34:28 +0000
Subject: [PATCH 17/33] chore: new statements and new poroofs

---
 src/Init/Data/BitVec/Lemmas.lean | 20 +++++++++++++-------
 1 file changed, 13 insertions(+), 7 deletions(-)

diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean
index e310f060da2f..9a2c0c08aed1 100644
--- a/src/Init/Data/BitVec/Lemmas.lean
+++ b/src/Init/Data/BitVec/Lemmas.lean
@@ -806,17 +806,23 @@ protected theorem extractLsb_ofNat (x n : Nat) (hi lo : Nat) :
     getLsbD (extractLsb hi lo x) i = (i ≤ (hi-lo) && getLsbD x (lo+i)) := by
   simp [getLsbD, Nat.lt_succ]
 
+
 @[simp] theorem getMsbD_extractLsb {hi lo : Nat} {x : BitVec w} {i : Nat} :
     (extractLsb hi lo x).getMsbD i
-    = (decide (i ≤  hi - lo)
-      && (decide (lo + (hi - lo - i) < w)
-      && x.getMsbD (w - 1 - (lo + (hi - lo - i))))) := by
-  simp [BitVec.extractLsb, BitVec.getMsbD_extractLsb', Nat.add_sub_cancel, Nat.lt_add_one_iff (m := i) (n := (hi - lo))]
+    = if lo ≤ hi then decide (i ≤ hi - lo) && (decide (hi - i < w) && x.getMsbD (w - 1 - (hi - i)))
+    else decide (i = 0) && (decide (lo < w) && x.getMsbD (w - 1 - lo)) := by
+  by_cases hlo : lo ≤ hi
+  · simp only [hlo, ↓reduceIte]
+    by_cases hil : i ≤ hi - lo
+    · simp [hil, BitVec.extractLsb, BitVec.getMsbD_extractLsb', Nat.add_sub_cancel, Nat.lt_add_one_iff (m := i) (n := (hi - lo)), show lo + (hi - lo - i) = hi - i by omega]
+    · simp [hil, BitVec.extractLsb]; omega
+  · simp [hlo, BitVec.extractLsb, show hi - lo = 0 by omega, show lo + (hi - lo - i) = lo by omega]
 
 @[simp] theorem msb_extractLsb {hi lo : Nat} {x : BitVec w} :
     (extractLsb hi lo x).msb
-    = (decide (lo + (hi - lo) < w) && x.getMsbD (w - 1 - (lo + (hi - lo)))) := by
-  simp [BitVec.msb, BitVec.getMsbD_extractLsb]
+    = if lo ≤ hi then (decide (hi < w) && x.getMsbD (w - 1 - hi))
+    else (decide (lo < w) && x.getMsbD (w - 1 - lo)) := by
+  simp [BitVec.msb, BitVec.getMsbD_extractLsb, Nat.le_sub_iff_add_le' (k := lo) (n := 0) (m := hi)]
 
 theorem extractLsb'_eq_extractLsb {w : Nat} (x : BitVec w) (start len : Nat) (h : len > 0) :
     x.extractLsb' start len = (x.extractLsb (len - 1 + start) start).cast (by omega) := by
@@ -3381,7 +3387,7 @@ theorem shiftLeft_eq_mul_twoPow (x : BitVec w) (n : Nat) :
   simp [getLsbD_shiftLeft, Fin.is_lt, decide_true, Bool.true_and, mul_twoPow_eq_shiftLeft]
 
 /-- 2^i * 2^j = 2^(i + j) with bitvectors as well -/
-theorem twoPow_mul_twoPow_eq {w : Nat} (i j : Nat) : twoPow w i * twoPow w j = twoPow w (i + j) := by 
+theorem twoPow_mul_twoPow_eq {w : Nat} (i j : Nat) : twoPow w i * twoPow w j = twoPow w (i + j) := by
   apply BitVec.eq_of_toNat_eq
   simp only [toNat_mul, toNat_twoPow]
   rw [← Nat.mul_mod, Nat.pow_add]

From 5954098ff319d739ff31c1502346f65a44f473b6 Mon Sep 17 00:00:00 2001
From: luisacicolini <lc985@cam.ac.uk>
Date: Mon, 3 Feb 2025 09:37:01 +0000
Subject: [PATCH 18/33] chore: unwanted change fix

---
 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 9a2c0c08aed1..86ac11f87605 100644
--- a/src/Init/Data/BitVec/Lemmas.lean
+++ b/src/Init/Data/BitVec/Lemmas.lean
@@ -3387,7 +3387,7 @@ theorem shiftLeft_eq_mul_twoPow (x : BitVec w) (n : Nat) :
   simp [getLsbD_shiftLeft, Fin.is_lt, decide_true, Bool.true_and, mul_twoPow_eq_shiftLeft]
 
 /-- 2^i * 2^j = 2^(i + j) with bitvectors as well -/
-theorem twoPow_mul_twoPow_eq {w : Nat} (i j : Nat) : twoPow w i * twoPow w j = twoPow w (i + j) := by
+theorem twoPow_mul_twoPow_eq {w : Nat} (i j : Nat) : twoPow w i * twoPow w j = twoPow w (i + j) := by 
   apply BitVec.eq_of_toNat_eq
   simp only [toNat_mul, toNat_twoPow]
   rw [← Nat.mul_mod, Nat.pow_add]

From 912bdbe7fa5bab8a124b1304a74b7a6f0aa2b398 Mon Sep 17 00:00:00 2001
From: Luisa Cicolini <48860705+luisacicolini@users.noreply.github.com>
Date: Mon, 3 Feb 2025 10:04:30 +0000
Subject: [PATCH 19/33] chore: remove useless newline

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

diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean
index 86ac11f87605..897d9c27488f 100644
--- a/src/Init/Data/BitVec/Lemmas.lean
+++ b/src/Init/Data/BitVec/Lemmas.lean
@@ -806,7 +806,6 @@ protected theorem extractLsb_ofNat (x n : Nat) (hi lo : Nat) :
     getLsbD (extractLsb hi lo x) i = (i ≤ (hi-lo) && getLsbD x (lo+i)) := by
   simp [getLsbD, Nat.lt_succ]
 
-
 @[simp] theorem getMsbD_extractLsb {hi lo : Nat} {x : BitVec w} {i : Nat} :
     (extractLsb hi lo x).getMsbD i
     = if lo ≤ hi then decide (i ≤ hi - lo) && (decide (hi - i < w) && x.getMsbD (w - 1 - (hi - i)))

From 2b51a169e97f645f8b669788bb1c02c5a45733f7 Mon Sep 17 00:00:00 2001
From: luisacicolini <lc985@cam.ac.uk>
Date: Wed, 5 Feb 2025 08:22:42 +0000
Subject: [PATCH 20/33] chore: format getMsbD_extractLsb_prime

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

diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean
index 897d9c27488f..4d857880bf1e 100644
--- a/src/Init/Data/BitVec/Lemmas.lean
+++ b/src/Init/Data/BitVec/Lemmas.lean
@@ -782,9 +782,10 @@ protected theorem extractLsb_ofNat (x n : Nat) (hi lo : Nat) :
   simp [getLsbD, Nat.lt_succ]
 
 @[simp] theorem getMsbD_extractLsb' {start len : Nat} {x : BitVec w} {i : Nat} :
-    (extractLsb' start len x).getMsbD i
-    = (decide (i < len) &&
-    (decide (start + (len - 1 - i) < w) && x.getMsbD (w - 1 - (start + (len - 1 - i))))) := by
+    (extractLsb' start len x).getMsbD i =
+      (decide (i < len) &&
+      (decide (start + (len - 1 - i) < w) &&
+      x.getMsbD (w - 1 - (start + (len - 1 - i))))) := by
   rcases len with rfl | len
   · simp
   · have h : (len - i < len + 1) := by omega
@@ -3386,7 +3387,7 @@ theorem shiftLeft_eq_mul_twoPow (x : BitVec w) (n : Nat) :
   simp [getLsbD_shiftLeft, Fin.is_lt, decide_true, Bool.true_and, mul_twoPow_eq_shiftLeft]
 
 /-- 2^i * 2^j = 2^(i + j) with bitvectors as well -/
-theorem twoPow_mul_twoPow_eq {w : Nat} (i j : Nat) : twoPow w i * twoPow w j = twoPow w (i + j) := by 
+theorem twoPow_mul_twoPow_eq {w : Nat} (i j : Nat) : twoPow w i * twoPow w j = twoPow w (i + j) := by
   apply BitVec.eq_of_toNat_eq
   simp only [toNat_mul, toNat_twoPow]
   rw [← Nat.mul_mod, Nat.pow_add]

From f3d2463fa34075e0d549394c1c871e74d143eee3 Mon Sep 17 00:00:00 2001
From: luisacicolini <lc985@cam.ac.uk>
Date: Wed, 5 Feb 2025 08:45:09 +0000
Subject: [PATCH 21/33] chore: verbose comment

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

diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean
index 4d857880bf1e..82a039a6724f 100644
--- a/src/Init/Data/BitVec/Lemmas.lean
+++ b/src/Init/Data/BitVec/Lemmas.lean
@@ -781,6 +781,15 @@ protected theorem extractLsb_ofNat (x n : Nat) (hi lo : Nat) :
     (extractLsb' start len x).getLsbD i = (i < len && x.getLsbD (start+i)) := by
   simp [getLsbD, Nat.lt_succ]
 
+/-!
+  We extract a BitVec x' with length `len` from BitVec x, starting from the element at position `start`
+  let x                       = 8 7 6 5 4 3 2 1 0
+  let x' = x.extractLsb' 3 4  =     6 5 4 3
+  with `start = 3` and `len = 4`
+  we have `x'.getMsbD i = x[start + (len - 1 - i)] = x.getLsbD (start + (len - 1 - i))`
+  and rewrite `x.getLsbD (start + (len - 1 - i))` as `getMsbD`, which requires checking
+  `start + (len - 1 - i) < w` and yields `x.getMsbD (w - 1 - (start + (len - 1 - i)))`
+-/
 @[simp] theorem getMsbD_extractLsb' {start len : Nat} {x : BitVec w} {i : Nat} :
     (extractLsb' start len x).getMsbD i =
       (decide (i < len) &&

From 11e3bafc46dc74f7e8fe8d2336752fafb75679ab Mon Sep 17 00:00:00 2001
From: luisacicolini <lc985@cam.ac.uk>
Date: Wed, 5 Feb 2025 09:33:13 +0000
Subject: [PATCH 22/33] chore: fix getMsbD_extractLsb proof

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

diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean
index 82a039a6724f..3a6792470900 100644
--- a/src/Init/Data/BitVec/Lemmas.lean
+++ b/src/Init/Data/BitVec/Lemmas.lean
@@ -816,21 +816,31 @@ protected theorem extractLsb_ofNat (x n : Nat) (hi lo : Nat) :
     getLsbD (extractLsb hi lo x) i = (i ≤ (hi-lo) && getLsbD x (lo+i)) := by
   simp [getLsbD, Nat.lt_succ]
 
+@[boolToPropSimps] theorem and_eq_decide (a b : Bool) : (a && b) = decide (a = true ∧ b = true) := by simp [Bool.decide_and]
+
+attribute [boolToPropSimps] decide_eq_true_iff
+
+@[simp] theorem getLsbD_extractLsb (hi lo : Nat) (x : BitVec n) (i : Nat) :
+    getLsbD (extractLsb hi lo x) i = (decide (i < hi - lo + 1) && x.getLsbD (lo + i)) := by
+  rw [extractLsb]
+  rw [getLsbD_extractLsb']
+
 @[simp] theorem getMsbD_extractLsb {hi lo : Nat} {x : BitVec w} {i : Nat} :
-    (extractLsb hi lo x).getMsbD i
-    = if lo ≤ hi then decide (i ≤ hi - lo) && (decide (hi - i < w) && x.getMsbD (w - 1 - (hi - i)))
-    else decide (i = 0) && (decide (lo < w) && x.getMsbD (w - 1 - lo)) := by
-  by_cases hlo : lo ≤ hi
-  · simp only [hlo, ↓reduceIte]
-    by_cases hil : i ≤ hi - lo
-    · simp [hil, BitVec.extractLsb, BitVec.getMsbD_extractLsb', Nat.add_sub_cancel, Nat.lt_add_one_iff (m := i) (n := (hi - lo)), show lo + (hi - lo - i) = hi - i by omega]
-    · simp [hil, BitVec.extractLsb]; omega
-  · simp [hlo, BitVec.extractLsb, show hi - lo = 0 by omega, show lo + (hi - lo - i) = lo by omega]
+    (extractLsb hi lo x).getMsbD i =
+      (decide (i < hi - lo + 1) &&
+      (decide ((max hi lo) - i < w) &&
+      x.getMsbD (w - 1 - ((max hi lo) - i)))) := by
+  rw [getMsbD_eq_getLsbD, getLsbD_extractLsb, getLsbD_eq_getMsbD]
+  simp only [Bool.true_and, and_congr_right_iff, Nat.add_one_sub_one, boolToPropSimps, show hi - lo - i < hi - lo + 1 by omega]
+  intro
+  by_cases hmax : lo ≤ hi
+  · simp [Nat.max_eq_left hmax, show lo + (hi - lo - i) = hi - i by omega]
+  · simp [Nat.max_eq_right (show hi ≤ lo by omega), show lo + (hi - lo - i) = lo - i by omega]
 
 @[simp] theorem msb_extractLsb {hi lo : Nat} {x : BitVec w} :
     (extractLsb hi lo x).msb
-    = if lo ≤ hi then (decide (hi < w) && x.getMsbD (w - 1 - hi))
-    else (decide (lo < w) && x.getMsbD (w - 1 - lo)) := by
+    = (decide ((max hi lo) < w) &&
+      x.getMsbD (w - 1 - ((max hi lo)))) := by
   simp [BitVec.msb, BitVec.getMsbD_extractLsb, Nat.le_sub_iff_add_le' (k := lo) (n := 0) (m := hi)]
 
 theorem extractLsb'_eq_extractLsb {w : Nat} (x : BitVec w) (start len : Nat) (h : len > 0) :

From 070ff210343656bb5679e93f70573f7b4668ad44 Mon Sep 17 00:00:00 2001
From: luisacicolini <lc985@cam.ac.uk>
Date: Wed, 5 Feb 2025 10:40:56 +0000
Subject: [PATCH 23/33] chore: format

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

diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean
index 3a6792470900..7b8b77de5f64 100644
--- a/src/Init/Data/BitVec/Lemmas.lean
+++ b/src/Init/Data/BitVec/Lemmas.lean
@@ -797,9 +797,8 @@ protected theorem extractLsb_ofNat (x n : Nat) (hi lo : Nat) :
       x.getMsbD (w - 1 - (start + (len - 1 - i))))) := by
   rcases len with rfl | len
   · simp
-  · have h : (len - i < len + 1) := by omega
-    rw [getMsbD_eq_getLsbD, getLsbD_extractLsb', getLsbD_eq_getMsbD]
-    simp [h]
+  · rw [getMsbD_eq_getLsbD, getLsbD_extractLsb', getLsbD_eq_getMsbD]
+    simp [show (len - i < len + 1) by omega]
 
 @[simp] theorem msb_extractLsb' {start len : Nat} {x : BitVec w} :
     (extractLsb' start len x).msb
@@ -822,8 +821,7 @@ attribute [boolToPropSimps] decide_eq_true_iff
 
 @[simp] theorem getLsbD_extractLsb (hi lo : Nat) (x : BitVec n) (i : Nat) :
     getLsbD (extractLsb hi lo x) i = (decide (i < hi - lo + 1) && x.getLsbD (lo + i)) := by
-  rw [extractLsb]
-  rw [getLsbD_extractLsb']
+  rw [extractLsb, getLsbD_extractLsb']
 
 @[simp] theorem getMsbD_extractLsb {hi lo : Nat} {x : BitVec w} {i : Nat} :
     (extractLsb hi lo x).getMsbD i =
@@ -831,7 +829,7 @@ attribute [boolToPropSimps] decide_eq_true_iff
       (decide ((max hi lo) - i < w) &&
       x.getMsbD (w - 1 - ((max hi lo) - i)))) := by
   rw [getMsbD_eq_getLsbD, getLsbD_extractLsb, getLsbD_eq_getMsbD]
-  simp only [Bool.true_and, and_congr_right_iff, Nat.add_one_sub_one, boolToPropSimps, show hi - lo - i < hi - lo + 1 by omega]
+  simp only [and_congr_right_iff, Nat.add_one_sub_one, boolToPropSimps, show hi - lo - i < hi - lo + 1 by omega]
   intro
   by_cases hmax : lo ≤ hi
   · simp [Nat.max_eq_left hmax, show lo + (hi - lo - i) = hi - i by omega]

From b1c04d1965377d691004ae39f4fad4bcf722f236 Mon Sep 17 00:00:00 2001
From: luisacicolini <lc985@cam.ac.uk>
Date: Wed, 5 Feb 2025 10:42:10 +0000
Subject: [PATCH 24/33] chore: remove unwanted space mod

---
 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 7b8b77de5f64..dee8a74610be 100644
--- a/src/Init/Data/BitVec/Lemmas.lean
+++ b/src/Init/Data/BitVec/Lemmas.lean
@@ -3404,7 +3404,7 @@ theorem shiftLeft_eq_mul_twoPow (x : BitVec w) (n : Nat) :
   simp [getLsbD_shiftLeft, Fin.is_lt, decide_true, Bool.true_and, mul_twoPow_eq_shiftLeft]
 
 /-- 2^i * 2^j = 2^(i + j) with bitvectors as well -/
-theorem twoPow_mul_twoPow_eq {w : Nat} (i j : Nat) : twoPow w i * twoPow w j = twoPow w (i + j) := by
+theorem twoPow_mul_twoPow_eq {w : Nat} (i j : Nat) : twoPow w i * twoPow w j = twoPow w (i + j) := by 
   apply BitVec.eq_of_toNat_eq
   simp only [toNat_mul, toNat_twoPow]
   rw [← Nat.mul_mod, Nat.pow_add]

From b42dfad6e09cc9fecfdd4153cca7354ac1e4c935 Mon Sep 17 00:00:00 2001
From: Luisa Cicolini <48860705+luisacicolini@users.noreply.github.com>
Date: Thu, 6 Feb 2025 09:09:04 +0000
Subject: [PATCH 25/33] chore: formatting

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

diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean
index dee8a74610be..a48ab87c5063 100644
--- a/src/Init/Data/BitVec/Lemmas.lean
+++ b/src/Init/Data/BitVec/Lemmas.lean
@@ -836,9 +836,9 @@ attribute [boolToPropSimps] decide_eq_true_iff
   · simp [Nat.max_eq_right (show hi ≤ lo by omega), show lo + (hi - lo - i) = lo - i by omega]
 
 @[simp] theorem msb_extractLsb {hi lo : Nat} {x : BitVec w} :
-    (extractLsb hi lo x).msb
-    = (decide ((max hi lo) < w) &&
-      x.getMsbD (w - 1 - ((max hi lo)))) := by
+    (extractLsb hi lo x).msb =
+    (decide ((max hi lo) < w) 
+     && x.getMsbD (w - 1 - ((max hi lo)))) := by
   simp [BitVec.msb, BitVec.getMsbD_extractLsb, Nat.le_sub_iff_add_le' (k := lo) (n := 0) (m := hi)]
 
 theorem extractLsb'_eq_extractLsb {w : Nat} (x : BitVec w) (start len : Nat) (h : len > 0) :

From fd5578ba957e5c51a193c2e871e733e0de3cdc04 Mon Sep 17 00:00:00 2001
From: luisacicolini <lc985@cam.ac.uk>
Date: Fri, 7 Feb 2025 13:01:41 +0000
Subject: [PATCH 26/33] chore: format

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

diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean
index a48ab87c5063..51fcdaedd97f 100644
--- a/src/Init/Data/BitVec/Lemmas.lean
+++ b/src/Init/Data/BitVec/Lemmas.lean
@@ -801,8 +801,8 @@ protected theorem extractLsb_ofNat (x n : Nat) (hi lo : Nat) :
     simp [show (len - i < len + 1) by omega]
 
 @[simp] theorem msb_extractLsb' {start len : Nat} {x : BitVec w} :
-    (extractLsb' start len x).msb
-    = (decide (0 < len) && x.getLsbD (start + len - 1)) := by
+    (extractLsb' start len x).msb =
+      (decide (0 < len) && x.getLsbD (start + len - 1)) := by
   cases len
   · simp [BitVec.extractLsb', BitVec.msb]
   · simp [BitVec.msb, BitVec.getMsbD_eq_getLsbD, BitVec.getLsbD_extractLsb', ← Nat.add_assoc]
@@ -837,7 +837,7 @@ attribute [boolToPropSimps] decide_eq_true_iff
 
 @[simp] theorem msb_extractLsb {hi lo : Nat} {x : BitVec w} :
     (extractLsb hi lo x).msb =
-    (decide ((max hi lo) < w) 
+    (decide ((max hi lo) < w)
      && x.getMsbD (w - 1 - ((max hi lo)))) := by
   simp [BitVec.msb, BitVec.getMsbD_extractLsb, Nat.le_sub_iff_add_le' (k := lo) (n := 0) (m := hi)]
 
@@ -3404,7 +3404,7 @@ theorem shiftLeft_eq_mul_twoPow (x : BitVec w) (n : Nat) :
   simp [getLsbD_shiftLeft, Fin.is_lt, decide_true, Bool.true_and, mul_twoPow_eq_shiftLeft]
 
 /-- 2^i * 2^j = 2^(i + j) with bitvectors as well -/
-theorem twoPow_mul_twoPow_eq {w : Nat} (i j : Nat) : twoPow w i * twoPow w j = twoPow w (i + j) := by 
+theorem twoPow_mul_twoPow_eq {w : Nat} (i j : Nat) : twoPow w i * twoPow w j = twoPow w (i + j) := by
   apply BitVec.eq_of_toNat_eq
   simp only [toNat_mul, toNat_twoPow]
   rw [← Nat.mul_mod, Nat.pow_add]

From d283c3b01ac88703ee249dd276b8489692479ce0 Mon Sep 17 00:00:00 2001
From: luisacicolini <lc985@cam.ac.uk>
Date: Fri, 7 Feb 2025 16:24:31 +0000
Subject: [PATCH 27/33] chore: format

---
 src/Init/Data/BitVec/Lemmas.lean | 30 ++++++++++++++++++++----------
 src/Init/Data/Bool.lean          |  1 +
 2 files changed, 21 insertions(+), 10 deletions(-)

diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean
index 51fcdaedd97f..7e2f79ae5378 100644
--- a/src/Init/Data/BitVec/Lemmas.lean
+++ b/src/Init/Data/BitVec/Lemmas.lean
@@ -802,7 +802,8 @@ protected theorem extractLsb_ofNat (x n : Nat) (hi lo : Nat) :
 
 @[simp] theorem msb_extractLsb' {start len : Nat} {x : BitVec w} :
     (extractLsb' start len x).msb =
-      (decide (0 < len) && x.getLsbD (start + len - 1)) := by
+      (decide (0 < len)
+      && x.getLsbD (start + len - 1)) := by
   cases len
   · simp [BitVec.extractLsb', BitVec.msb]
   · simp [BitVec.msb, BitVec.getMsbD_eq_getLsbD, BitVec.getLsbD_extractLsb', ← Nat.add_assoc]
@@ -815,7 +816,7 @@ protected theorem extractLsb_ofNat (x n : Nat) (hi lo : Nat) :
     getLsbD (extractLsb hi lo x) i = (i ≤ (hi-lo) && getLsbD x (lo+i)) := by
   simp [getLsbD, Nat.lt_succ]
 
-@[boolToPropSimps] theorem and_eq_decide (a b : Bool) : (a && b) = decide (a = true ∧ b = true) := by simp [Bool.decide_and]
+theorem test {a b c : Bool} : decide a && (decide b && decide c) = decide a && decide b && decide c := by sorry
 
 attribute [boolToPropSimps] decide_eq_true_iff
 
@@ -826,14 +827,23 @@ attribute [boolToPropSimps] decide_eq_true_iff
 @[simp] theorem getMsbD_extractLsb {hi lo : Nat} {x : BitVec w} {i : Nat} :
     (extractLsb hi lo x).getMsbD i =
       (decide (i < hi - lo + 1) &&
-      (decide ((max hi lo) - i < w) &&
-      x.getMsbD (w - 1 - ((max hi lo) - i)))) := by
-  rw [getMsbD_eq_getLsbD, getLsbD_extractLsb, getLsbD_eq_getMsbD]
-  simp only [and_congr_right_iff, Nat.add_one_sub_one, boolToPropSimps, show hi - lo - i < hi - lo + 1 by omega]
-  intro
-  by_cases hmax : lo ≤ hi
-  · simp [Nat.max_eq_left hmax, show lo + (hi - lo - i) = hi - i by omega]
-  · simp [Nat.max_eq_right (show hi ≤ lo by omega), show lo + (hi - lo - i) = lo - i by omega]
+      decide ((max hi lo) - i < w) &&
+      x.getMsbD (w - 1 - ((max hi lo) - i))) := by
+  rw [getMsbD_eq_getLsbD, getLsbD_extractLsb, getLsbD_eq_getMsbD, Nat.add_one_sub_one]
+  sorry
+
+  -- conv =>
+  --   lhs
+  --   rw [← decide_eq_true_eq (p := x.getMsbD (w - 1 - (lo + (hi - lo - i))))]
+  --   rw [Bool.and_eq_decide (p := (lo + (hi - lo - i) < w)) (q := )]
+
+  -- simp [and_congr_right_iff, Nat.add_one_sub_one, show hi - lo - i < hi - lo + 1 by omega]
+
+  -- by_cases hmax : lo ≤ hi
+  -- · simp [Nat.max_eq_left hmax, show lo + (hi - lo - i) = hi - i by omega]
+  --   sorry
+  -- · simp [Nat.max_eq_right (show hi ≤ lo by omega), show lo + (hi - lo - i) = lo - i by omega]
+  --   sorry
 
 @[simp] theorem msb_extractLsb {hi lo : Nat} {x : BitVec w} :
     (extractLsb hi lo x).msb =
diff --git a/src/Init/Data/Bool.lean b/src/Init/Data/Bool.lean
index a83d1976cbf9..8ebe2bee9eb4 100644
--- a/src/Init/Data/Bool.lean
+++ b/src/Init/Data/Bool.lean
@@ -593,6 +593,7 @@ theorem decide_beq_decide (p q : Prop) [dpq : Decidable (p ↔ q)] [dp : Decidab
     (decide p == decide q) = decide (p ↔ q) := by
   cases dp with | _ p => simp [p]
 
+
 end Bool
 
 export Bool (cond_eq_if xor and or not)

From 2db64615117338c023b0e064e29e287be4952656 Mon Sep 17 00:00:00 2001
From: luisacicolini <lc985@cam.ac.uk>
Date: Fri, 7 Feb 2025 17:22:05 +0000
Subject: [PATCH 28/33] chore: fix build

---
 src/Init/Data/BitVec/Lemmas.lean | 29 ++++++++---------------------
 src/Init/Data/Bool.lean          |  5 +++++
 2 files changed, 13 insertions(+), 21 deletions(-)

diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean
index 7e2f79ae5378..5a961a6caba5 100644
--- a/src/Init/Data/BitVec/Lemmas.lean
+++ b/src/Init/Data/BitVec/Lemmas.lean
@@ -816,10 +816,6 @@ protected theorem extractLsb_ofNat (x n : Nat) (hi lo : Nat) :
     getLsbD (extractLsb hi lo x) i = (i ≤ (hi-lo) && getLsbD x (lo+i)) := by
   simp [getLsbD, Nat.lt_succ]
 
-theorem test {a b c : Bool} : decide a && (decide b && decide c) = decide a && decide b && decide c := by sorry
-
-attribute [boolToPropSimps] decide_eq_true_iff
-
 @[simp] theorem getLsbD_extractLsb (hi lo : Nat) (x : BitVec n) (i : Nat) :
     getLsbD (extractLsb hi lo x) i = (decide (i < hi - lo + 1) && x.getLsbD (lo + i)) := by
   rw [extractLsb, getLsbD_extractLsb']
@@ -827,23 +823,14 @@ attribute [boolToPropSimps] decide_eq_true_iff
 @[simp] theorem getMsbD_extractLsb {hi lo : Nat} {x : BitVec w} {i : Nat} :
     (extractLsb hi lo x).getMsbD i =
       (decide (i < hi - lo + 1) &&
-      decide ((max hi lo) - i < w) &&
-      x.getMsbD (w - 1 - ((max hi lo) - i))) := by
-  rw [getMsbD_eq_getLsbD, getLsbD_extractLsb, getLsbD_eq_getMsbD, Nat.add_one_sub_one]
-  sorry
-
-  -- conv =>
-  --   lhs
-  --   rw [← decide_eq_true_eq (p := x.getMsbD (w - 1 - (lo + (hi - lo - i))))]
-  --   rw [Bool.and_eq_decide (p := (lo + (hi - lo - i) < w)) (q := )]
-
-  -- simp [and_congr_right_iff, Nat.add_one_sub_one, show hi - lo - i < hi - lo + 1 by omega]
-
-  -- by_cases hmax : lo ≤ hi
-  -- · simp [Nat.max_eq_left hmax, show lo + (hi - lo - i) = hi - i by omega]
-  --   sorry
-  -- · simp [Nat.max_eq_right (show hi ≤ lo by omega), show lo + (hi - lo - i) = lo - i by omega]
-  --   sorry
+      (decide ((max hi lo) - i < w) &&
+      x.getMsbD (w - 1 - ((max hi lo) - i)))) := by
+  rw [getMsbD_eq_getLsbD, getLsbD_extractLsb, getLsbD_eq_getMsbD]
+  simp only [decide_eq_true_iff, and_congr_right_iff, Nat.add_one_sub_one, boolToPropSimps, Bool.and_eq_decide_true, show hi - lo - i < hi - lo + 1 by omega]
+  intro
+  by_cases hmax : lo ≤ hi
+  · simp [Nat.max_eq_left hmax, show lo + (hi - lo - i) = hi - i by omega]
+  · simp [Nat.max_eq_right (show hi ≤ lo by omega), show lo + (hi - lo - i) = lo - i by omega]
 
 @[simp] theorem msb_extractLsb {hi lo : Nat} {x : BitVec w} :
     (extractLsb hi lo x).msb =
diff --git a/src/Init/Data/Bool.lean b/src/Init/Data/Bool.lean
index 8ebe2bee9eb4..4807d28b0eea 100644
--- a/src/Init/Data/Bool.lean
+++ b/src/Init/Data/Bool.lean
@@ -566,10 +566,15 @@ theorem apply_cond (f : α → β) {b : Bool} {a a' : α} :
 
 protected theorem decide_coe (b : Bool) [Decidable (b = true)] : decide (b = true) = b := decide_eq_true
 
+
 @[simp] theorem decide_and (p q : Prop) [dpq : Decidable (p ∧ q)] [dp : Decidable p] [dq : Decidable q] :
     decide (p ∧ q) = (p && q) := by
   cases dp with | _ p => simp [p]
 
+theorem and_eq_decide_true (a b : Bool) :
+    (a && b) = decide (a = true ∧ b = true) := by
+  simp [Bool.decide_and]
+
 @[simp] theorem decide_or (p q : Prop) [dpq : Decidable (p ∨ q)] [dp : Decidable p] [dq : Decidable q] :
     decide (p ∨ q) = (p || q) := by
   cases dp with | _ p => simp [p]

From 47cb161b56183a3f56a3f12ce3b5380bd43f6aa8 Mon Sep 17 00:00:00 2001
From: Luisa Cicolini <48860705+luisacicolini@users.noreply.github.com>
Date: Fri, 7 Feb 2025 17:24:12 +0000
Subject: [PATCH 29/33] chore: formatting

---
 src/Init/Data/Bool.lean | 1 -
 1 file changed, 1 deletion(-)

diff --git a/src/Init/Data/Bool.lean b/src/Init/Data/Bool.lean
index 4807d28b0eea..08343fb7710f 100644
--- a/src/Init/Data/Bool.lean
+++ b/src/Init/Data/Bool.lean
@@ -566,7 +566,6 @@ theorem apply_cond (f : α → β) {b : Bool} {a a' : α} :
 
 protected theorem decide_coe (b : Bool) [Decidable (b = true)] : decide (b = true) = b := decide_eq_true
 
-
 @[simp] theorem decide_and (p q : Prop) [dpq : Decidable (p ∧ q)] [dp : Decidable p] [dq : Decidable q] :
     decide (p ∧ q) = (p && q) := by
   cases dp with | _ p => simp [p]

From 2145d73c9b292e771f2d8fb4481458cdba55fe32 Mon Sep 17 00:00:00 2001
From: Luisa Cicolini <48860705+luisacicolini@users.noreply.github.com>
Date: Fri, 7 Feb 2025 17:24:30 +0000
Subject: [PATCH 30/33] chore: formatting

---
 src/Init/Data/Bool.lean | 1 -
 1 file changed, 1 deletion(-)

diff --git a/src/Init/Data/Bool.lean b/src/Init/Data/Bool.lean
index 08343fb7710f..07c61079cb50 100644
--- a/src/Init/Data/Bool.lean
+++ b/src/Init/Data/Bool.lean
@@ -597,7 +597,6 @@ theorem decide_beq_decide (p q : Prop) [dpq : Decidable (p ↔ q)] [dp : Decidab
     (decide p == decide q) = decide (p ↔ q) := by
   cases dp with | _ p => simp [p]
 
-
 end Bool
 
 export Bool (cond_eq_if xor and or not)

From d31a7d77b209d4acff902b875fdaf7311822b163 Mon Sep 17 00:00:00 2001
From: Luisa Cicolini <48860705+luisacicolini@users.noreply.github.com>
Date: Fri, 7 Feb 2025 17:24:48 +0000
Subject: [PATCH 31/33] chore: formatting

---
 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 5a961a6caba5..2a837f22f19a 100644
--- a/src/Init/Data/BitVec/Lemmas.lean
+++ b/src/Init/Data/BitVec/Lemmas.lean
@@ -3401,7 +3401,7 @@ theorem shiftLeft_eq_mul_twoPow (x : BitVec w) (n : Nat) :
   simp [getLsbD_shiftLeft, Fin.is_lt, decide_true, Bool.true_and, mul_twoPow_eq_shiftLeft]
 
 /-- 2^i * 2^j = 2^(i + j) with bitvectors as well -/
-theorem twoPow_mul_twoPow_eq {w : Nat} (i j : Nat) : twoPow w i * twoPow w j = twoPow w (i + j) := by
+theorem twoPow_mul_twoPow_eq {w : Nat} (i j : Nat) : twoPow w i * twoPow w j = twoPow w (i + j) := by 
   apply BitVec.eq_of_toNat_eq
   simp only [toNat_mul, toNat_twoPow]
   rw [← Nat.mul_mod, Nat.pow_add]

From 51825074e1ca342b030873fbbb3ec9a3a0605dc0 Mon Sep 17 00:00:00 2001
From: luisacicolini <lc985@cam.ac.uk>
Date: Fri, 7 Feb 2025 18:14:48 +0000
Subject: [PATCH 32/33] chore: format

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

diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean
index 2a837f22f19a..d9155f58c8e1 100644
--- a/src/Init/Data/BitVec/Lemmas.lean
+++ b/src/Init/Data/BitVec/Lemmas.lean
@@ -826,7 +826,8 @@ protected theorem extractLsb_ofNat (x n : Nat) (hi lo : Nat) :
       (decide ((max hi lo) - i < w) &&
       x.getMsbD (w - 1 - ((max hi lo) - i)))) := by
   rw [getMsbD_eq_getLsbD, getLsbD_extractLsb, getLsbD_eq_getMsbD]
-  simp only [decide_eq_true_iff, and_congr_right_iff, Nat.add_one_sub_one, boolToPropSimps, Bool.and_eq_decide_true, show hi - lo - i < hi - lo + 1 by omega]
+  simp only [decide_eq_true_iff, and_congr_right_iff, Nat.add_one_sub_one,
+    boolToPropSimps, Bool.and_eq_decide_true, show hi - lo - i < hi - lo + 1 by omega]
   intro
   by_cases hmax : lo ≤ hi
   · simp [Nat.max_eq_left hmax, show lo + (hi - lo - i) = hi - i by omega]
@@ -3401,7 +3402,7 @@ theorem shiftLeft_eq_mul_twoPow (x : BitVec w) (n : Nat) :
   simp [getLsbD_shiftLeft, Fin.is_lt, decide_true, Bool.true_and, mul_twoPow_eq_shiftLeft]
 
 /-- 2^i * 2^j = 2^(i + j) with bitvectors as well -/
-theorem twoPow_mul_twoPow_eq {w : Nat} (i j : Nat) : twoPow w i * twoPow w j = twoPow w (i + j) := by 
+theorem twoPow_mul_twoPow_eq {w : Nat} (i j : Nat) : twoPow w i * twoPow w j = twoPow w (i + j) := by
   apply BitVec.eq_of_toNat_eq
   simp only [toNat_mul, toNat_twoPow]
   rw [← Nat.mul_mod, Nat.pow_add]

From e46bc3854476f400e59e900f9a11b3590da24ca0 Mon Sep 17 00:00:00 2001
From: luisacicolini <lc985@cam.ac.uk>
Date: Fri, 7 Feb 2025 18:16:24 +0000
Subject: [PATCH 33/33] chore: format

---
 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 d9155f58c8e1..38ba43e4981e 100644
--- a/src/Init/Data/BitVec/Lemmas.lean
+++ b/src/Init/Data/BitVec/Lemmas.lean
@@ -3402,7 +3402,7 @@ theorem shiftLeft_eq_mul_twoPow (x : BitVec w) (n : Nat) :
   simp [getLsbD_shiftLeft, Fin.is_lt, decide_true, Bool.true_and, mul_twoPow_eq_shiftLeft]
 
 /-- 2^i * 2^j = 2^(i + j) with bitvectors as well -/
-theorem twoPow_mul_twoPow_eq {w : Nat} (i j : Nat) : twoPow w i * twoPow w j = twoPow w (i + j) := by
+theorem twoPow_mul_twoPow_eq {w : Nat} (i j : Nat) : twoPow w i * twoPow w j = twoPow w (i + j) := by 
   apply BitVec.eq_of_toNat_eq
   simp only [toNat_mul, toNat_twoPow]
   rw [← Nat.mul_mod, Nat.pow_add]