From cb98bd1c040ef49f78c39aa6f2523599e6b7da6b Mon Sep 17 00:00:00 2001
From: Tobias Grosser <tobias@grosser.es>
Date: Thu, 5 Dec 2024 07:21:19 +0000
Subject: [PATCH 01/15] bv_append

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

diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean
index 21523d5f8744..b7af4f53cf2c 100644
--- a/src/Init/Data/BitVec/Lemmas.lean
+++ b/src/Init/Data/BitVec/Lemmas.lean
@@ -1759,6 +1759,55 @@ theorem append_def (x : BitVec v) (y : BitVec w) :
     (x ++ y).toNat = x.toNat <<< n ||| y.toNat :=
   rfl
 
+@[simp] theorem toFin_append (x : BitVec m) (y : BitVec n) :
+    (x ++ y).toFin = @Fin.mk (2^(m+n)) (x.toNat <<< n ||| y.toNat) (by
+      have := BitVec.isLt x
+      have := BitVec.isLt y
+      rw [Nat.shiftLeft_eq]
+      by_cases m0 : m = 0
+      · subst m0
+        simp_all
+      · by_cases x0 : x = 0
+        · subst x0
+          simp_all
+          rw [Nat.pow_add]
+          have ax := Nat.two_pow_pos n
+          have bx := Nat.two_pow_pos m
+          simp_all
+          have aa := @Nat.mul_lt_mul_of_le_of_lt y.toNat (2^n) 1 (2^m) (by
+            omega
+          ) (by
+            have mpos : 0 < m := by omega
+            have := @Nat.one_lt_two_pow m (by omega)
+            omega
+          ) (by omega)
+          simp at aa
+          rw [Nat.mul_comm]
+          apply aa
+        · simp_all
+          have := @Nat.or_lt_two_pow (x.toNat * 2 ^ n) y.toNat (m+n) (by
+            simp only [Nat.pow_add, Nat.two_pow_pos n, Nat.mul_lt_mul_right, BitVec.isLt x]
+          ) (by
+            have ax := Nat.two_pow_pos n
+            have bx := Nat.two_pow_pos m
+            simp_all
+            simp_all [Nat.pow_add, Nat.two_pow_pos n, BitVec.isLt x]
+            have aa := @Nat.mul_lt_mul_of_le_of_lt y.toNat (2^n) 1 (2^m) (by
+              omega
+            ) (by
+              have mpos : 0 < m := by omega
+              have := @Nat.one_lt_two_pow m (by omega)
+              omega
+            ) (by omega)
+            simp at aa
+            rw [Nat.mul_comm]
+            apply aa
+          )
+          apply this
+    )  := by
+  ext
+  simp
+
 theorem getLsbD_append {x : BitVec n} {y : BitVec m} :
     getLsbD (x ++ y) i = bif i < m then getLsbD y i else getLsbD x (i - m) := by
   simp only [append_def, getLsbD_or, getLsbD_shiftLeftZeroExtend, getLsbD_setWidth']

From c49fff542c9caf5b2fd05b20d1f21d6c28e9bce8 Mon Sep 17 00:00:00 2001
From: Tobias Grosser <tobias@grosser.es>
Date: Thu, 5 Dec 2024 07:28:27 +0000
Subject: [PATCH 02/15] shorten proof

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

diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean
index b7af4f53cf2c..63a8c942dc1b 100644
--- a/src/Init/Data/BitVec/Lemmas.lean
+++ b/src/Init/Data/BitVec/Lemmas.lean
@@ -1761,26 +1761,17 @@ theorem append_def (x : BitVec v) (y : BitVec w) :
 
 @[simp] theorem toFin_append (x : BitVec m) (y : BitVec n) :
     (x ++ y).toFin = @Fin.mk (2^(m+n)) (x.toNat <<< n ||| y.toNat) (by
-      have := BitVec.isLt x
-      have := BitVec.isLt y
       rw [Nat.shiftLeft_eq]
       by_cases m0 : m = 0
       · subst m0
-        simp_all
+        simp [BitVec.isLt x, BitVec.isLt y]
       · by_cases x0 : x = 0
         · subst x0
           simp_all
           rw [Nat.pow_add]
           have ax := Nat.two_pow_pos n
-          have bx := Nat.two_pow_pos m
           simp_all
-          have aa := @Nat.mul_lt_mul_of_le_of_lt y.toNat (2^n) 1 (2^m) (by
-            omega
-          ) (by
-            have mpos : 0 < m := by omega
-            have := @Nat.one_lt_two_pow m (by omega)
-            omega
-          ) (by omega)
+          have aa := @Nat.mul_lt_mul_of_le_of_lt y.toNat (2^n) 1 (2^m) (by omega) (by apply Nat.one_lt_two_pow (by omega)) (by omega)
           simp at aa
           rw [Nat.mul_comm]
           apply aa
@@ -1788,19 +1779,10 @@ theorem append_def (x : BitVec v) (y : BitVec w) :
           have := @Nat.or_lt_two_pow (x.toNat * 2 ^ n) y.toNat (m+n) (by
             simp only [Nat.pow_add, Nat.two_pow_pos n, Nat.mul_lt_mul_right, BitVec.isLt x]
           ) (by
-            have ax := Nat.two_pow_pos n
-            have bx := Nat.two_pow_pos m
-            simp_all
             simp_all [Nat.pow_add, Nat.two_pow_pos n, BitVec.isLt x]
-            have aa := @Nat.mul_lt_mul_of_le_of_lt y.toNat (2^n) 1 (2^m) (by
-              omega
-            ) (by
-              have mpos : 0 < m := by omega
-              have := @Nat.one_lt_two_pow m (by omega)
-              omega
-            ) (by omega)
-            simp at aa
             rw [Nat.mul_comm]
+            have aa := @Nat.mul_lt_mul_of_le_of_lt y.toNat (2^n) 1 (2^m) (by omega) (Nat.one_lt_two_pow (by omega)) (by omega)
+            simp at aa
             apply aa
           )
           apply this

From 6f0e41c7a9dada0fa2f33760820fb850c970507a Mon Sep 17 00:00:00 2001
From: Tobias Grosser <tobias@grosser.es>
Date: Thu, 5 Dec 2024 07:46:16 +0000
Subject: [PATCH 03/15] chore: polish

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

diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean
index 63a8c942dc1b..468d4651c45b 100644
--- a/src/Init/Data/BitVec/Lemmas.lean
+++ b/src/Init/Data/BitVec/Lemmas.lean
@@ -1761,32 +1761,33 @@ theorem append_def (x : BitVec v) (y : BitVec w) :
 
 @[simp] theorem toFin_append (x : BitVec m) (y : BitVec n) :
     (x ++ y).toFin = @Fin.mk (2^(m+n)) (x.toNat <<< n ||| y.toNat) (by
+      have := BitVec.isLt y
       rw [Nat.shiftLeft_eq]
       by_cases m0 : m = 0
       · subst m0
-        simp [BitVec.isLt x, BitVec.isLt y]
+        have := BitVec.isLt x
+        simp_all
       · by_cases x0 : x = 0
         · subst x0
-          simp_all
           rw [Nat.pow_add]
-          have ax := Nat.two_pow_pos n
-          simp_all
           have aa := @Nat.mul_lt_mul_of_le_of_lt y.toNat (2^n) 1 (2^m) (by omega) (by apply Nat.one_lt_two_pow (by omega)) (by omega)
-          simp at aa
+          simp only [Nat.mul_one] at aa
+          simp only [ofNat_eq_ofNat, toNat_ofNat, Nat.zero_mod, Nat.zero_mul, Nat.zero_or,
+            gt_iff_lt]
           rw [Nat.mul_comm]
           apply aa
         · simp_all
           have := @Nat.or_lt_two_pow (x.toNat * 2 ^ n) y.toNat (m+n) (by
-            simp only [Nat.pow_add, Nat.two_pow_pos n, Nat.mul_lt_mul_right, BitVec.isLt x]
+            simp [Nat.pow_add, Nat.two_pow_pos n, BitVec.isLt x]
           ) (by
-            simp_all [Nat.pow_add, Nat.two_pow_pos n, BitVec.isLt x]
-            rw [Nat.mul_comm]
-            have aa := @Nat.mul_lt_mul_of_le_of_lt y.toNat (2^n) 1 (2^m) (by omega) (Nat.one_lt_two_pow (by omega)) (by omega)
-            simp at aa
+            rw [Nat.pow_add, Nat.mul_comm]
+            have aa :=
+            @Nat.mul_lt_mul_of_le_of_lt y.toNat (2^n) 1 (2^m) (by omega) (Nat.one_lt_two_pow (by omega)) (by omega)
+            rw [Nat.mul_one] at aa
             apply aa
           )
           apply this
-    )  := by
+    ) := by
   ext
   simp
 

From 2e5c3514bbf262e68992eff971a9997312ebe8bf Mon Sep 17 00:00:00 2001
From: Siddharth Bhat <siddu.druid@gmail.com>
Date: Thu, 5 Dec 2024 11:18:02 +0000
Subject: [PATCH 04/15] Chore: golf

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

diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean
index 468d4651c45b..65a8e1daae62 100644
--- a/src/Init/Data/BitVec/Lemmas.lean
+++ b/src/Init/Data/BitVec/Lemmas.lean
@@ -1759,35 +1759,23 @@ theorem append_def (x : BitVec v) (y : BitVec w) :
     (x ++ y).toNat = x.toNat <<< n ||| y.toNat :=
   rfl
 
-@[simp] theorem toFin_append (x : BitVec m) (y : BitVec n) :
-    (x ++ y).toFin = @Fin.mk (2^(m+n)) (x.toNat <<< n ||| y.toNat) (by
-      have := BitVec.isLt y
-      rw [Nat.shiftLeft_eq]
-      by_cases m0 : m = 0
-      · subst m0
-        have := BitVec.isLt x
-        simp_all
-      · by_cases x0 : x = 0
-        · subst x0
-          rw [Nat.pow_add]
-          have aa := @Nat.mul_lt_mul_of_le_of_lt y.toNat (2^n) 1 (2^m) (by omega) (by apply Nat.one_lt_two_pow (by omega)) (by omega)
-          simp only [Nat.mul_one] at aa
-          simp only [ofNat_eq_ofNat, toNat_ofNat, Nat.zero_mod, Nat.zero_mul, Nat.zero_or,
-            gt_iff_lt]
-          rw [Nat.mul_comm]
-          apply aa
-        · simp_all
-          have := @Nat.or_lt_two_pow (x.toNat * 2 ^ n) y.toNat (m+n) (by
-            simp [Nat.pow_add, Nat.two_pow_pos n, BitVec.isLt x]
-          ) (by
-            rw [Nat.pow_add, Nat.mul_comm]
-            have aa :=
-            @Nat.mul_lt_mul_of_le_of_lt y.toNat (2^n) 1 (2^m) (by omega) (Nat.one_lt_two_pow (by omega)) (by omega)
-            rw [Nat.mul_one] at aa
-            apply aa
-          )
-          apply this
-    ) := by
+/-- Helper theorem to show that the expression in `(x ++ y).toFin` is inbounds. -/
+theorem toNat_append_lt {m n : Nat} (x : BitVec m) (y : BitVec n) :
+    x.toNat <<< n ||| y.toNat < 2 ^ (m + n) := by
+  have hm : 0 < 2^m := by exact Nat.two_pow_pos m
+  have hn : 0 < 2^n := by exact Nat.two_pow_pos n
+
+  have hnLe : 2^n ≤ 2 ^(m + n) := by
+    rw [Nat.pow_add]
+    exact Nat.le_mul_of_pos_left (2 ^ n) hm
+  apply Nat.or_lt_two_pow
+  · rw [Nat.shiftLeft_eq, Nat.pow_add]
+    rw [Nat.mul_lt_mul_right] <;> omega
+  · omega
+
+@[simp] theorem toFin_append (x : BitVec m) (y : BitVec n)
+    (h : x.toNat <<< n ||| y.toNat < 2 ^ (m + n) := toNat_append_lt x y) :
+    (x ++ y).toFin = @Fin.mk (2^(m+n)) (x.toNat <<< n ||| y.toNat) h  := by
   ext
   simp
 

From cd4f969c6f075d608befc4267ffe70b7467bb5e8 Mon Sep 17 00:00:00 2001
From: Tobias Grosser <tobias@grosser.es>
Date: Thu, 5 Dec 2024 11:25:23 +0000
Subject: [PATCH 05/15] further golf

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

diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean
index 65a8e1daae62..9f24e2ff5ab8 100644
--- a/src/Init/Data/BitVec/Lemmas.lean
+++ b/src/Init/Data/BitVec/Lemmas.lean
@@ -1762,20 +1762,17 @@ theorem append_def (x : BitVec v) (y : BitVec w) :
 /-- Helper theorem to show that the expression in `(x ++ y).toFin` is inbounds. -/
 theorem toNat_append_lt {m n : Nat} (x : BitVec m) (y : BitVec n) :
     x.toNat <<< n ||| y.toNat < 2 ^ (m + n) := by
-  have hm : 0 < 2^m := by exact Nat.two_pow_pos m
-  have hn : 0 < 2^n := by exact Nat.two_pow_pos n
-
   have hnLe : 2^n ≤ 2 ^(m + n) := by
     rw [Nat.pow_add]
-    exact Nat.le_mul_of_pos_left (2 ^ n) hm
+    exact Nat.le_mul_of_pos_left (2 ^ n) (Nat.two_pow_pos m)
   apply Nat.or_lt_two_pow
-  · rw [Nat.shiftLeft_eq, Nat.pow_add]
-    rw [Nat.mul_lt_mul_right] <;> omega
+  · have := Nat.two_pow_pos n
+    rw [Nat.shiftLeft_eq, Nat.pow_add, Nat.mul_lt_mul_right]
+    <;> omega
   · omega
 
-@[simp] theorem toFin_append (x : BitVec m) (y : BitVec n)
-    (h : x.toNat <<< n ||| y.toNat < 2 ^ (m + n) := toNat_append_lt x y) :
-    (x ++ y).toFin = @Fin.mk (2^(m+n)) (x.toNat <<< n ||| y.toNat) h  := by
+@[simp] theorem toFin_append (x : BitVec m) (y : BitVec n) :
+    (x ++ y).toFin = @Fin.mk (2^(m+n)) (x.toNat <<< n ||| y.toNat) (toNat_append_lt x y) := by
   ext
   simp
 

From a09aa3c91f4c6555093549075c42f88e04d5b3f0 Mon Sep 17 00:00:00 2001
From: Tobias Grosser <github@grosser.es>
Date: Thu, 5 Dec 2024 11:33:06 +0000
Subject: [PATCH 06/15] 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 9f24e2ff5ab8..3abd443efb9f 100644
--- a/src/Init/Data/BitVec/Lemmas.lean
+++ b/src/Init/Data/BitVec/Lemmas.lean
@@ -1771,7 +1771,7 @@ theorem toNat_append_lt {m n : Nat} (x : BitVec m) (y : BitVec n) :
     <;> omega
   · omega
 
-@[simp] theorem toFin_append (x : BitVec m) (y : BitVec n) :
+@[simp] theorem toFin_append {x : BitVec m} {y : BitVec n} :
     (x ++ y).toFin = @Fin.mk (2^(m+n)) (x.toNat <<< n ||| y.toNat) (toNat_append_lt x y) := by
   ext
   simp

From 61aa020060a402717db18a4f97d573a0ed7162f0 Mon Sep 17 00:00:00 2001
From: Tobias Grosser <tobias@grosser.es>
Date: Sat, 7 Dec 2024 03:50:09 +0000
Subject: [PATCH 07/15] chore: add statement for toInt_append

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

diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean
index 3abd443efb9f..b62d1020296d 100644
--- a/src/Init/Data/BitVec/Lemmas.lean
+++ b/src/Init/Data/BitVec/Lemmas.lean
@@ -520,6 +520,9 @@ theorem eq_zero_or_eq_one (a : BitVec 1) : a = 0#1 ∨ a = 1#1 := by
 theorem toInt_zero {w : Nat} : (0#w).toInt = 0 := by
   simp [BitVec.toInt, show 0 < 2^w by exact Nat.two_pow_pos w]
 
+@[simp] theorem toInt_cast (h : w = v) (x : BitVec w) : (cast h x).toInt = x.toInt := by
+  simp [toInt_eq_toNat_bmod, h]
+
 /-! ### slt -/
 
 /--
@@ -1823,6 +1826,33 @@ theorem msb_append {x : BitVec w} {y : BitVec v} :
   ext
   simp only [getLsbD_append, getLsbD_zero, Bool.cond_self]
 
+def lhs (x : BitVec n) (y : BitVec m) : Int := (x++y).toInt
+def rhs (x : BitVec n) (y : BitVec m) : Int := if n == 0 then y.toInt else (x.toInt * (2^m)) + y.toNat
+
+def eq (x: BitVec n) (y: BitVec m) : Bool := (lhs x y) = (rhs x y)
+
+
+#eval (-5#10 ++ 3#2).toInt
+
+def test : Bool := Id.run do
+  for i in [0, 1, 2, 3, 4, 5, 6, 7, 8] do
+    for j in [0, 1, 2, 3, 4, 5, 6, 7, 8] do
+      for n in [0, 1, 2, 3, 4] do
+        for m in [0, 1, 2, 3, 4] do
+          let x := BitVec.ofNat n i
+          let y := BitVec.ofNat m j
+          if (!eq x y) then
+            return false
+  return true
+
+@[simp] theorem toInt_append {x : BitVec n} {y : BitVec m} :
+    (x ++ y).toInt = if n == 0 then y.toInt else x.toInt * (2 ^ m) + y.toNat := by
+  by_cases n0 : n = 0
+  · subst n0
+    simp [BitVec.eq_nil x]
+  · simp [n0]
+    sorry
+
 @[simp] theorem cast_append_right (h : w + v = w + v') (x : BitVec w) (y : BitVec v) :
     cast h (x ++ y) = x ++ cast (by omega) y := by
   ext

From 38abb0da470600c6e77ab825bf52b776ca87ce1d Mon Sep 17 00:00:00 2001
From: Tobias Grosser <tobias@grosser.es>
Date: Sat, 7 Dec 2024 05:08:45 +0000
Subject: [PATCH 08/15] More wip proofs

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

diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean
index b62d1020296d..ad6cd521f71b 100644
--- a/src/Init/Data/BitVec/Lemmas.lean
+++ b/src/Init/Data/BitVec/Lemmas.lean
@@ -1127,6 +1127,11 @@ theorem not_eq_comm {x y : BitVec w} : ~~~ x = y ↔ x = ~~~ y := by
     BitVec.toNat (x <<< n) = BitVec.toNat x <<< n % 2^v :=
   BitVec.toNat_ofNat _ _
 
+@[simp] theorem toInt_shiftLeft {n : Nat} {x : BitVec v} :
+    BitVec.toInt (x <<< n) = Int.bmod (BitVec.toInt x * 2^n) (2^v) := by
+  simp [toInt_eq_toNat_bmod, Nat.shiftLeft_eq]
+  norm_cast
+
 @[simp] theorem toFin_shiftLeft {n : Nat} (x : BitVec w) :
     BitVec.toFin (x <<< n) = Fin.ofNat' (2^w) (x.toNat <<< n) := rfl
 
@@ -1826,6 +1831,14 @@ theorem msb_append {x : BitVec w} {y : BitVec v} :
   ext
   simp only [getLsbD_append, getLsbD_zero, Bool.cond_self]
 
+@[simp] theorem append_zero {n m : Nat} {x : BitVec n} :
+    x ++ 0#m = x.setWidth (n + m) <<< m := by
+  induction m
+  case zero =>
+    simp
+  case succ i ih =>
+    sorry
+
 def lhs (x : BitVec n) (y : BitVec m) : Int := (x++y).toInt
 def rhs (x : BitVec n) (y : BitVec m) : Int := if n == 0 then y.toInt else (x.toInt * (2^m)) + y.toNat
 
@@ -1851,7 +1864,27 @@ def test : Bool := Id.run do
   · subst n0
     simp [BitVec.eq_nil x]
   · simp [n0]
-    sorry
+    by_cases y0 : y = 0
+    ·
+      have xlt := BitVec.isLt x
+      have hh : 2 ^ n < 2 ^ (n + m) := sorry
+      have h2 : x.toNat <<< m % 2 ^ (n + m) = x.toNat <<< m := sorry
+      simp only [y0]
+      simp only [ofNat_eq_ofNat, append_zero]
+      rw [toInt_eq_toNat_cond]
+      rw [toInt_eq_toNat_cond]
+      split
+      <;> split
+      <;> norm_cast
+      <;> simp
+      <;> rw [Nat.mod_eq_of_lt (a := x.toNat) (by omega)]
+      <;> norm_cast
+      <;> simp [h2]
+      rw [Nat.shiftLeft_eq]
+      <;> simp_all
+      · sorry
+      · sorry
+      · simp [Nat.shiftLeft_eq, Int.sub_mul, Nat.pow_add]
 
 @[simp] theorem cast_append_right (h : w + v = w + v') (x : BitVec w) (y : BitVec v) :
     cast h (x ++ y) = x ++ cast (by omega) y := by

From 6ede404178c03d195586add4ce3e20869033e8d4 Mon Sep 17 00:00:00 2001
From: Tobias Grosser <tobias@grosser.es>
Date: Sat, 7 Dec 2024 05:26:13 +0000
Subject: [PATCH 09/15] Nat

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

diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean
index ad6cd521f71b..b01a24a07954 100644
--- a/src/Init/Data/BitVec/Lemmas.lean
+++ b/src/Init/Data/BitVec/Lemmas.lean
@@ -1863,28 +1863,75 @@ def test : Bool := Id.run do
   by_cases n0 : n = 0
   · subst n0
     simp [BitVec.eq_nil x]
-  · simp [n0]
-    by_cases y0 : y = 0
-    ·
-      have xlt := BitVec.isLt x
-      have hh : 2 ^ n < 2 ^ (n + m) := sorry
-      have h2 : x.toNat <<< m % 2 ^ (n + m) = x.toNat <<< m := sorry
-      simp only [y0]
-      simp only [ofNat_eq_ofNat, append_zero]
-      rw [toInt_eq_toNat_cond]
-      rw [toInt_eq_toNat_cond]
-      split
-      <;> split
-      <;> norm_cast
-      <;> simp
-      <;> rw [Nat.mod_eq_of_lt (a := x.toNat) (by omega)]
-      <;> norm_cast
-      <;> simp [h2]
-      rw [Nat.shiftLeft_eq]
-      <;> simp_all
+  · by_cases m0 : m = 0
+    · subst m0
+      simp [BitVec.eq_nil y, n0]
+    · simp [m0]
+      by_cases y0 : y = 0
+      ·
+        have xlt := BitVec.isLt x
+        have hh : 2 ^ n < 2 ^ (n + m) := by
+          rw [Nat.pow_add]
+          have := @Nat.pow_pos 2 m (by omega)
+          have := @Nat.pow_pos 2 n (by omega)
+          have := @Nat.mul_lt_mul_of_le_of_lt' (2^n) (2^n) 1 (2^m) (by omega) (by simp [*]) (by omega)
+          simp at this
+          simp [this]
+
+        have h3 : x.toNat <<< m % 2 ^ (n + m) = x.toNat <<< m := sorry
+        have h2 : x.toNat % 2 ^ (n + m) = x.toNat := by
+          rw [Nat.mod_eq_of_lt]
+          rw [Nat.pow_add]
+          have := @Nat.pow_pos 2 m (by omega)
+          simp_all
+          rw [Nat.mul_lt_mul_of_lt_of_lt]
+
+          omega
+
+
+        sorry
+        simp only [y0]
+        simp only [ofNat_eq_ofNat, append_zero]
+        rw [toInt_eq_toNat_cond]
+        rw [toInt_eq_toNat_cond]
+        split
+        ·
+          split
+          <;> norm_cast
+          <;> simp
+          <;> rw [Nat.mod_eq_of_lt (a := x.toNat) (by omega)]
+          <;> norm_cast
+          <;> simp [h3]
+          <;> simp_all
+          · rw [Nat.shiftLeft_eq]
+          · rename_i aa bb
+            rw [Nat.shiftLeft_eq] at aa
+            rw [Nat.pow_add] at aa
+            rw [← Nat.mul_assoc] at aa
+
+            sorry
+        ·
+          split
+          <;> norm_cast
+          <;> simp
+          <;> rw [Nat.mod_eq_of_lt (a := x.toNat) (by omega)]
+          <;> norm_cast
+          <;> simp [h3]
+          <;> simp_all
+          · rename_i aa bb
+            rw [Nat.shiftLeft_eq] at aa
+            rw [Nat.pow_add] at aa
+            rw [← Nat.mul_assoc] at aa
+
+
+
+
+            simp_all
+
+
+            sorry
+          · simp [Nat.shiftLeft_eq, Int.sub_mul, Nat.pow_add]
       · sorry
-      · sorry
-      · simp [Nat.shiftLeft_eq, Int.sub_mul, Nat.pow_add]
 
 @[simp] theorem cast_append_right (h : w + v = w + v') (x : BitVec w) (y : BitVec v) :
     cast h (x ++ y) = x ++ cast (by omega) y := by

From 4b6b2ce93cd36c8c3a0d4c406ef0e6d7b5fdf9ad Mon Sep 17 00:00:00 2001
From: Tobias Grosser <tobias@grosser.es>
Date: Sat, 7 Dec 2024 12:59:24 +0000
Subject: [PATCH 10/15] clean up theorem

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

diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean
index b01a24a07954..5cd36277d369 100644
--- a/src/Init/Data/BitVec/Lemmas.lean
+++ b/src/Init/Data/BitVec/Lemmas.lean
@@ -1858,6 +1858,18 @@ def test : Bool := Id.run do
             return false
   return true
 
+private theorem Nat.lt_mul_of_le_of_lt_of_lt {a b c : Nat} (hab : a ≤ b) (ha : 0 < a) (hc : 1 < c) :
+    a < b * c := by
+  have : a * 1 < b * c := Nat.mul_lt_mul_of_le_of_lt' (by omega) (by simp [hc]) (by omega)
+  simp at this
+  simp [this]
+
+private theorem Nat.two_pow_lt_two_pow_add {n m : Nat} (h : m ≠ 0) :
+    2 ^ n < 2 ^ (n + m) := by
+  rw [Nat.pow_add]
+  have : 0 < 2 ^ n := Nat.pow_pos (by omega)
+  apply Nat.lt_mul_of_le_of_lt_of_lt (by omega) (by omega) (by simp [h])
+
 @[simp] theorem toInt_append {x : BitVec n} {y : BitVec m} :
     (x ++ y).toInt = if n == 0 then y.toInt else x.toInt * (2 ^ m) + y.toNat := by
   by_cases n0 : n = 0
@@ -1870,14 +1882,7 @@ def test : Bool := Id.run do
       by_cases y0 : y = 0
       ·
         have xlt := BitVec.isLt x
-        have hh : 2 ^ n < 2 ^ (n + m) := by
-          rw [Nat.pow_add]
-          have := @Nat.pow_pos 2 m (by omega)
-          have := @Nat.pow_pos 2 n (by omega)
-          have := @Nat.mul_lt_mul_of_le_of_lt' (2^n) (2^n) 1 (2^m) (by omega) (by simp [*]) (by omega)
-          simp at this
-          simp [this]
-
+        have hh : 2 ^ n < 2 ^ (n + m) := Nat.two_pow_lt_two_pow_add m0
         have h3 : x.toNat <<< m % 2 ^ (n + m) = x.toNat <<< m := sorry
         have h2 : x.toNat % 2 ^ (n + m) = x.toNat := by
           rw [Nat.mod_eq_of_lt]

From 03782d8f438ac0182b9692a68379c09eb6b047f3 Mon Sep 17 00:00:00 2001
From: Tobias Grosser <tobias@grosser.es>
Date: Sat, 7 Dec 2024 13:18:38 +0000
Subject: [PATCH 11/15] Further cleanup

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

diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean
index 5cd36277d369..d413efef0d00 100644
--- a/src/Init/Data/BitVec/Lemmas.lean
+++ b/src/Init/Data/BitVec/Lemmas.lean
@@ -1831,8 +1831,8 @@ theorem msb_append {x : BitVec w} {y : BitVec v} :
   ext
   simp only [getLsbD_append, getLsbD_zero, Bool.cond_self]
 
-@[simp] theorem append_zero {n m : Nat} {x : BitVec n} :
-    x ++ 0#m = x.setWidth (n + m) <<< m := by
+theorem append_zero {n m : Nat} {x : BitVec n} :
+    x ++ 0#m = x.signExtend (n + m) <<< m := by
   induction m
   case zero =>
     simp
@@ -1866,9 +1866,25 @@ private theorem Nat.lt_mul_of_le_of_lt_of_lt {a b c : Nat} (hab : a ≤ b) (ha :
 
 private theorem Nat.two_pow_lt_two_pow_add {n m : Nat} (h : m ≠ 0) :
     2 ^ n < 2 ^ (n + m) := by
-  rw [Nat.pow_add]
-  have : 0 < 2 ^ n := Nat.pow_pos (by omega)
-  apply Nat.lt_mul_of_le_of_lt_of_lt (by omega) (by omega) (by simp [h])
+  apply Nat.pow_lt_pow_of_lt (by omega) (by omega)
+
+@[simp] theorem toInt_append_zero {n m : Nat} {x : BitVec n} :
+    (x ++ 0#m).toInt = x.toInt * (2 ^ m) := by
+  by_cases m0 : m = 0
+  · subst m0
+    simp
+  ·
+    simp only [ofNat_eq_ofNat, append_zero]
+    rw [toInt_eq_msb_cond]
+    rw [toInt_eq_msb_cond]
+    split
+    <;> split
+
+    simp
+
+
+
+
 
 @[simp] theorem toInt_append {x : BitVec n} {y : BitVec m} :
     (x ++ y).toInt = if n == 0 then y.toInt else x.toInt * (2 ^ m) + y.toNat := by
@@ -1894,7 +1910,6 @@ private theorem Nat.two_pow_lt_two_pow_add {n m : Nat} (h : m ≠ 0) :
           omega
 
 
-        sorry
         simp only [y0]
         simp only [ofNat_eq_ofNat, append_zero]
         rw [toInt_eq_toNat_cond]

From fbe220189bcda19cfdbbc42f48b8d3daf4eaf069 Mon Sep 17 00:00:00 2001
From: Tobias Grosser <tobias@grosser.es>
Date: Sat, 7 Dec 2024 14:08:13 +0000
Subject: [PATCH 12/15] Further cleanup

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

diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean
index d413efef0d00..95a27166e27a 100644
--- a/src/Init/Data/BitVec/Lemmas.lean
+++ b/src/Init/Data/BitVec/Lemmas.lean
@@ -1868,23 +1868,24 @@ private theorem Nat.two_pow_lt_two_pow_add {n m : Nat} (h : m ≠ 0) :
     2 ^ n < 2 ^ (n + m) := by
   apply Nat.pow_lt_pow_of_lt (by omega) (by omega)
 
+@[simp] theorem signExtend_shiftLeft_of_lt {n m : Nat} {x : BitVec n} :
+    (signExtend (n + m) x <<< m).msb = x.msb := by
+  sorry
+
 @[simp] theorem toInt_append_zero {n m : Nat} {x : BitVec n} :
     (x ++ 0#m).toInt = x.toInt * (2 ^ m) := by
   by_cases m0 : m = 0
   · subst m0
     simp
-  ·
-    simp only [ofNat_eq_ofNat, append_zero]
-    rw [toInt_eq_msb_cond]
-    rw [toInt_eq_msb_cond]
-    split
-    <;> split
-
-    simp
-
-
-
-
+  · simp only [ofNat_eq_ofNat, append_zero, toInt_eq_msb_cond]
+    by_cases h1 : (signExtend (n + m) x <<< m).msb
+    · by_cases h2: x.msb
+      · sorry
+      · simp only [signExtend_shiftLeft_of_lt] at h1
+        contradiction
+    · by_cases h2: x.msb
+      · simp [signExtend_shiftLeft_of_lt, h2] at h1
+      · sorry
 
 @[simp] theorem toInt_append {x : BitVec n} {y : BitVec m} :
     (x ++ y).toInt = if n == 0 then y.toInt else x.toInt * (2 ^ m) + y.toNat := by

From 39df0cb6f8eb6c0ed49d4f4c9a41593e0b9c6a44 Mon Sep 17 00:00:00 2001
From: Tobias Grosser <tobias@grosser.es>
Date: Sun, 8 Dec 2024 13:03:26 +0000
Subject: [PATCH 13/15] WIP

---
 src/Init/Data/BitVec/Lemmas.lean | 125 ++++++++++++++++++++++++++-----
 1 file changed, 107 insertions(+), 18 deletions(-)

diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean
index 95a27166e27a..283d4714376c 100644
--- a/src/Init/Data/BitVec/Lemmas.lean
+++ b/src/Init/Data/BitVec/Lemmas.lean
@@ -498,6 +498,9 @@ theorem toInt_ofNat {n : Nat} (x : Nat) :
 @[simp] theorem ofInt_ofNat (w n : Nat) :
   BitVec.ofInt w (no_index (OfNat.ofNat n)) = BitVec.ofNat w (OfNat.ofNat n) := rfl
 
+@[simp] theorem ofInt_toInt (x : BitVec w) : BitVec.ofInt w (x.toInt) = x := by
+  by_cases h : 2 * x.toNat < 2^w <;> ext <;> simp [getLsbD, h, BitVec.toInt]
+
 theorem toInt_neg_iff {w : Nat} {x : BitVec w} :
     BitVec.toInt x < 0 ↔ 2 ^ w ≤ 2 * x.toNat := by
   simp [toInt_eq_toNat_cond]; omega
@@ -1665,11 +1668,54 @@ theorem getLsbD_signExtend (x  : BitVec w) {v i : Nat} :
   · rw [signExtend_eq_not_setWidth_not_of_msb_true hmsb]
     by_cases (i < v) <;> by_cases (i < w) <;> simp_all <;> omega
 
+protected theorem Nat.sub_sub_comm {n m k : Nat} : n - m - k = n - k - m := sorry
+
+theorem getMsbD_signExtend (x  : BitVec w) {v i : Nat} :
+    (x.signExtend v).getMsbD i = (decide (i < v) && if w+i-v < w then x.getMsbD (w+i-v) else x.msb) := by
+  rcases hmsb : x.msb with rfl | rfl
+  · rw [signExtend_eq_not_setWidth_not_of_msb_false hmsb]
+    simp_all [getMsbD]
+    by_cases h' : (i < v) <;> by_cases h'': ((w+i-v < w)) <;> simp [getMsbD, h', h'']
+    have h''': ((v - 1 - i < v)) := by omega
+    simp [h''']
+    by_cases h5 : v ≤ w
+    · rw [show (w - 1 - (w + i - v)) = (v - 1 - i) by (
+        rw [Nat.sub_add_comm]
+        rw [← Nat.sub_sub]
+        rw [Nat.sub_sub_comm (m := 1)]
+        rw [Nat.sub_sub_eq_min]
+        rw [Nat.min_eq_right]
+        omega; omega)]
+    ·
+
+
+
+  · rw [signExtend_eq_not_setWidth_not_of_msb_true hmsb]
+    by_cases h' : (i < v) <;> by_cases h'': ((w+i-v < w)) <;> simp [getMsbD, h', h'']
+    have h''': ((v - 1 - i < w)) := by omega
+    simp[h''']
+
+    <;> rw [show (w - 1 - (w - v + i)) = (v - 1 - i) by omega]
+
 theorem getElem_signExtend {x  : BitVec w} {v i : Nat} (h : i < v) :
     (x.signExtend v)[i] = if i < w then x.getLsbD i else x.msb := by
   rw [←getLsbD_eq_getElem, getLsbD_signExtend]
   simp [h]
 
+theorem msb_SignExtend (x : BitVec w) :
+    (x.signExtend v).msb = (if v ≥ w then x.msb else x.getLsbD v) := by
+  by_cases h : v ≥ w
+  · simp [h, BitVec.msb]
+
+
+
+
+  unfold signExtend
+
+  rw [msb_eq_getLsbD_last]
+  simp only [getLsbD_setWidth]
+  cases getLsbD x (v - 1) <;> simp; omega
+
 /-- Sign extending to a width smaller than the starting width is a truncation. -/
 theorem signExtend_eq_setWidth_of_lt (x : BitVec w) {v : Nat} (hv : v ≤ w):
   x.signExtend v = x.setWidth v := by
@@ -1868,8 +1914,47 @@ private theorem Nat.two_pow_lt_two_pow_add {n m : Nat} (h : m ≠ 0) :
     2 ^ n < 2 ^ (n + m) := by
   apply Nat.pow_lt_pow_of_lt (by omega) (by omega)
 
-@[simp] theorem signExtend_shiftLeft_of_lt {n m : Nat} {x : BitVec n} :
+@[simp] theorem signExtend_shiftLeft_msb {n m : Nat} {x : BitVec n} :
     (signExtend (n + m) x <<< m).msb = x.msb := by
+  induction m
+  case zero =>
+    simp [signExtend]
+  case succ i ih =>
+    rw [← ih]
+    rw [msb_setWidth]
+
+    unfold BitVec.msb getMsbD
+    simp
+    by_cases h : (0 < n + i)
+    ·
+      rw [← Nat.add_assoc]
+      simp [h]
+      have h' : (0 < n + i + 1) := by omega
+      have hh : (n + i - (i + 1)) = (n + i - i - 1) := by
+        omega
+      rw [hh]
+      simp
+      have hhh : (n + i - 1 - i) = (n + i - i - 1) := by omega
+      rw [hhh]
+      simp
+      rw [getLsbD_signExtend]
+
+
+
+
+
+
+    simp [BitVec.msb, getMsbD]
+
+    by_cases h : 0 < n + (i + 1)
+    · simp [h]
+
+      sorry
+    · simp [h]
+      sorry
+
+@[simp] theorem signExtend_toNat_shift_mod :
+    ((signExtend (n + m) x).toNat <<< m) % ↑(2 ^ (n + m)) = (signExtend (n + m) x).toNat <<< m :=
   sorry
 
 @[simp] theorem toInt_append_zero {n m : Nat} {x : BitVec n} :
@@ -1880,7 +1965,26 @@ private theorem Nat.two_pow_lt_two_pow_add {n m : Nat} (h : m ≠ 0) :
   · simp only [ofNat_eq_ofNat, append_zero, toInt_eq_msb_cond]
     by_cases h1 : (signExtend (n + m) x <<< m).msb
     · by_cases h2: x.msb
-      · sorry
+      · norm_cast
+        simp [h1, h2]
+        norm_cast
+        rw [Int.sub_mul, Nat.pow_add]
+        norm_cast
+        simp
+        rw [Nat.shiftLeft_eq]
+        norm_cast
+        have aa := @Nat.pow_pos 2 m (by omega)
+        norm_cast
+        have bb := @Nat.mul_right_cancel_iff (2^m) ((signExtend (n + m) x).toNat)
+        apply bb
+        rfl
+        rw [Nat.mul_right_cancel (m := 2 ^ m)]
+        simp [aa]
+        rw [Nat.mod_eq_of_lt (a := x.toNat) (by omega)]
+        norm_cast
+        simp [h3]
+        simp_all
+        rw [Nat.shiftLeft_eq]
       · simp only [signExtend_shiftLeft_of_lt] at h1
         contradiction
     · by_cases h2: x.msb
@@ -1897,22 +2001,7 @@ private theorem Nat.two_pow_lt_two_pow_add {n m : Nat} (h : m ≠ 0) :
       simp [BitVec.eq_nil y, n0]
     · simp [m0]
       by_cases y0 : y = 0
-      ·
-        have xlt := BitVec.isLt x
-        have hh : 2 ^ n < 2 ^ (n + m) := Nat.two_pow_lt_two_pow_add m0
-        have h3 : x.toNat <<< m % 2 ^ (n + m) = x.toNat <<< m := sorry
-        have h2 : x.toNat % 2 ^ (n + m) = x.toNat := by
-          rw [Nat.mod_eq_of_lt]
-          rw [Nat.pow_add]
-          have := @Nat.pow_pos 2 m (by omega)
-          simp_all
-          rw [Nat.mul_lt_mul_of_lt_of_lt]
-
-          omega
-
-
-        simp only [y0]
-        simp only [ofNat_eq_ofNat, append_zero]
+      · simp [toInt_append_zero, y0, n0]
         rw [toInt_eq_toNat_cond]
         rw [toInt_eq_toNat_cond]
         split

From dcd6e057361d57a19b1ac225ab06d5e25b1e1f8d Mon Sep 17 00:00:00 2001
From: Tobias Grosser <tobias@grosser.es>
Date: Sun, 8 Dec 2024 15:18:38 +0000
Subject: [PATCH 14/15] add setWidth Proofs

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

diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean
index 283d4714376c..c7a68b5e0ad9 100644
--- a/src/Init/Data/BitVec/Lemmas.lean
+++ b/src/Init/Data/BitVec/Lemmas.lean
@@ -575,6 +575,10 @@ theorem zeroExtend_eq_setWidth {v : Nat} {x : BitVec w} :
     (x.setWidth v).toInt = Int.bmod x.toNat (2^v) := by
   simp [toInt_eq_toNat_bmod, toNat_setWidth, Int.emod_bmod]
 
+@[simp] theorem toFin_setWidth (x : BitVec w) :
+    (x.setWidth v).toFin = Fin.ofNat' (2^v) x.toNat := by
+  ext; simp
+
 theorem setWidth'_eq {x : BitVec w} (h : w ≤ v) : x.setWidth' h = x.setWidth v := by
   apply eq_of_toNat_eq
   rw [toNat_setWidth, toNat_setWidth']
@@ -651,6 +655,21 @@ theorem getElem?_setWidth (m : Nat) (x : BitVec n) (i : Nat) :
     getLsbD (setWidth m x) i = (decide (i < m) && getLsbD x i) := by
   simp [getLsbD, toNat_setWidth, Nat.testBit_mod_two_pow]
 
+@[simp] theorem getMsbD_setWidth {m : Nat} {x : BitVec n} {i : Nat} :
+    getMsbD (setWidth m x) i = (decide (m - n ≤ i) && getMsbD x (i + n - m)) := by
+  unfold setWidth
+  by_cases h : n ≤ m <;> simp only [h]
+  · by_cases h' : (m - n ≤ i)
+    · simp [h', show (i - (m - n)) = i + n - m by omega]
+    · simp [h']
+  · simp only [show m-n = 0 by omega, getMsbD, getLsbD_setWidth]
+    by_cases h'' : i < m
+    · simp [show m - 1 - i < m by omega, show i + n - m < n by omega,
+        show (n - 1 - (i + n - m)) = m - 1 - i by omega]
+      omega
+    · simp [h'']
+      omega
+
 @[simp] theorem getMsbD_setWidth_add {x : BitVec w} (h : k ≤ i) :
     (x.setWidth (w + k)).getMsbD i = x.getMsbD (i - k) := by
   by_cases h : w = 0
@@ -1627,7 +1646,7 @@ private theorem Int.negSucc_emod (m : Nat) (n : Int) :
     -(m + 1) % n = Int.subNatNat (Int.natAbs n) ((m % Int.natAbs n) + 1) := rfl
 
 /-- The sign extension is the same as zero extending when `msb = false`. -/
-theorem signExtend_eq_not_setWidth_not_of_msb_false {x : BitVec w} {v : Nat} (hmsb : x.msb = false) :
+theorem signExtend_eq_setWidth_of_msb_false {x : BitVec w} {v : Nat} (hmsb : x.msb = false) :
     x.signExtend v = x.setWidth v := by
   ext i
   by_cases hv : i < v
@@ -1663,7 +1682,7 @@ theorem signExtend_eq_not_setWidth_not_of_msb_true {x : BitVec w} {v : Nat} (hms
 theorem getLsbD_signExtend (x  : BitVec w) {v i : Nat} :
     (x.signExtend v).getLsbD i = (decide (i < v) && if i < w then x.getLsbD i else x.msb) := by
   rcases hmsb : x.msb with rfl | rfl
-  · rw [signExtend_eq_not_setWidth_not_of_msb_false hmsb]
+  · rw [signExtend_eq_setWidth_of_msb_false hmsb]
     by_cases (i < v) <;> by_cases (i < w) <;> simp_all <;> omega
   · rw [signExtend_eq_not_setWidth_not_of_msb_true hmsb]
     by_cases (i < v) <;> by_cases (i < w) <;> simp_all <;> omega
@@ -1671,31 +1690,46 @@ theorem getLsbD_signExtend (x  : BitVec w) {v i : Nat} :
 protected theorem Nat.sub_sub_comm {n m k : Nat} : n - m - k = n - k - m := sorry
 
 theorem getMsbD_signExtend (x  : BitVec w) {v i : Nat} :
-    (x.signExtend v).getMsbD i = (decide (i < v) && if w+i-v < w then x.getMsbD (w+i-v) else x.msb) := by
+    (x.signExtend v).getMsbD i = (decide (i < v) && (if i > v-w then x.getMsbD (i-(v-w)) else x.msb)) := by
   rcases hmsb : x.msb with rfl | rfl
-  · rw [signExtend_eq_not_setWidth_not_of_msb_false hmsb]
-    simp_all [getMsbD]
-    by_cases h' : (i < v) <;> by_cases h'': ((w+i-v < w)) <;> simp [getMsbD, h', h'']
-    have h''': ((v - 1 - i < v)) := by omega
-    simp [h''']
-    by_cases h5 : v ≤ w
-    · rw [show (w - 1 - (w + i - v)) = (v - 1 - i) by (
-        rw [Nat.sub_add_comm]
-        rw [← Nat.sub_sub]
-        rw [Nat.sub_sub_comm (m := 1)]
-        rw [Nat.sub_sub_eq_min]
-        rw [Nat.min_eq_right]
-        omega; omega)]
-    ·
+  · simp [signExtend_eq_setWidth_of_msb_false hmsb]
+    simp [getMsbD_setWidth']
 
 
+    rw [signExtend_eq_not_setWidth_not_of_msb_false hmsb]
+    rw [getMsbD]
+    rw [getMsbD]
+    simp
+    by_cases h : i < v
+    ·
+      simp [h]
+      simp [show v - 1 - i < v by omega]
+      by_cases h' : v - w < i
+      · simp [h']
+        simp [show (i - (v - w) < w) by omega]
+        rw [show (w - 1 - (i - (v-w))) = (v - 1 - i) by omega]
+      · simp [h']
+        omega
+    · simp [h]
 
   · rw [signExtend_eq_not_setWidth_not_of_msb_true hmsb]
-    by_cases h' : (i < v) <;> by_cases h'': ((w+i-v < w)) <;> simp [getMsbD, h', h'']
-    have h''': ((v - 1 - i < w)) := by omega
-    simp[h''']
+    rw [getMsbD]
+    rw [getMsbD]
+    simp
+    by_cases h : i < v
+    ·
+      simp [h]
+      simp [show v - 1 - i < v by omega]
+      by_cases h' : v - w < i
+      · simp [h']
+        simp [show (i - (v - w) < w) by omega]
+        simp [show (v - 1 - i < w) by omega]
+        rw [show (w - 1 - (i - (v-w))) = (v - 1 - i) by omega]
+      · simp [h']
+        rw [getlsbD_of]
 
-    <;> rw [show (w - 1 - (w - v + i)) = (v - 1 - i) by omega]
+        omega
+    · simp [h]
 
 theorem getElem_signExtend {x  : BitVec w} {v i : Nat} (h : i < v) :
     (x.signExtend v)[i] = if i < w then x.getLsbD i else x.msb := by

From be732475065b6aaba2d3117446b1554af3c26358 Mon Sep 17 00:00:00 2001
From: Tobias Grosser <tobias@grosser.es>
Date: Sun, 8 Dec 2024 15:54:57 +0000
Subject: [PATCH 15/15] WIP

---
 src/Init/Data/BitVec/Lemmas.lean | 75 ++++++++------------------------
 1 file changed, 18 insertions(+), 57 deletions(-)

diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean
index c7a68b5e0ad9..7e5de36317bf 100644
--- a/src/Init/Data/BitVec/Lemmas.lean
+++ b/src/Init/Data/BitVec/Lemmas.lean
@@ -655,7 +655,7 @@ theorem getElem?_setWidth (m : Nat) (x : BitVec n) (i : Nat) :
     getLsbD (setWidth m x) i = (decide (i < m) && getLsbD x i) := by
   simp [getLsbD, toNat_setWidth, Nat.testBit_mod_two_pow]
 
-@[simp] theorem getMsbD_setWidth {m : Nat} {x : BitVec n} {i : Nat} :
+theorem getMsbD_setWidth {m : Nat} {x : BitVec n} {i : Nat} :
     getMsbD (setWidth m x) i = (decide (m - n ≤ i) && getMsbD x (i + n - m)) := by
   unfold setWidth
   by_cases h : n ≤ m <;> simp only [h]
@@ -1253,6 +1253,7 @@ theorem shiftLeftZeroExtend_eq {x : BitVec w} :
     (shiftLeftZeroExtend x i).msb = x.msb := by
   simp [shiftLeftZeroExtend_eq, BitVec.msb]
 
+
 theorem shiftLeft_add {w : Nat} (x : BitVec w) (n m : Nat) :
     x <<< (n + m) = (x <<< n) <<< m := by
   ext i
@@ -1687,68 +1688,27 @@ theorem getLsbD_signExtend (x  : BitVec w) {v i : Nat} :
   · rw [signExtend_eq_not_setWidth_not_of_msb_true hmsb]
     by_cases (i < v) <;> by_cases (i < w) <;> simp_all <;> omega
 
-protected theorem Nat.sub_sub_comm {n m k : Nat} : n - m - k = n - k - m := sorry
-
-theorem getMsbD_signExtend (x  : BitVec w) {v i : Nat} :
-    (x.signExtend v).getMsbD i = (decide (i < v) && (if i > v-w then x.getMsbD (i-(v-w)) else x.msb)) := by
+theorem getMsbD_signExtend {x : BitVec w} {v i : Nat} :
+    (x.signExtend v).getMsbD i =
+      (decide (i < v) && if v - w ≤ i then x.getMsbD (i + w - v) else x.msb) := by
   rcases hmsb : x.msb with rfl | rfl
-  · simp [signExtend_eq_setWidth_of_msb_false hmsb]
-    simp [getMsbD_setWidth']
-
-
-    rw [signExtend_eq_not_setWidth_not_of_msb_false hmsb]
-    rw [getMsbD]
-    rw [getMsbD]
-    simp
-    by_cases h : i < v
-    ·
-      simp [h]
-      simp [show v - 1 - i < v by omega]
-      by_cases h' : v - w < i
-      · simp [h']
-        simp [show (i - (v - w) < w) by omega]
-        rw [show (w - 1 - (i - (v-w))) = (v - 1 - i) by omega]
-      · simp [h']
-        omega
-    · simp [h]
-
-  · rw [signExtend_eq_not_setWidth_not_of_msb_true hmsb]
-    rw [getMsbD]
-    rw [getMsbD]
-    simp
-    by_cases h : i < v
-    ·
-      simp [h]
-      simp [show v - 1 - i < v by omega]
-      by_cases h' : v - w < i
-      · simp [h']
-        simp [show (i - (v - w) < w) by omega]
-        simp [show (v - 1 - i < w) by omega]
-        rw [show (w - 1 - (i - (v-w))) = (v - 1 - i) by omega]
-      · simp [h']
-        rw [getlsbD_of]
-
-        omega
-    · simp [h]
+  · simp [signExtend_eq_setWidth_of_msb_false hmsb, getMsbD_setWidth]
+    by_cases h : (v - w ≤ i) <;> simp [h, getMsbD] <;> omega
+  · simp only [signExtend_eq_not_setWidth_not_of_msb_true hmsb, getMsbD_not,
+      getMsbD_setWidth, Bool.not_and, Bool.not_not, Bool.if_true_right]
+    by_cases h : i < v <;> by_cases h' : v - w ≤ i <;> simp [h, h'] <;> omega
 
 theorem getElem_signExtend {x  : BitVec w} {v i : Nat} (h : i < v) :
     (x.signExtend v)[i] = if i < w then x.getLsbD i else x.msb := by
   rw [←getLsbD_eq_getElem, getLsbD_signExtend]
   simp [h]
 
-theorem msb_SignExtend (x : BitVec w) :
-    (x.signExtend v).msb = (if v ≥ w then x.msb else x.getLsbD v) := by
-  by_cases h : v ≥ w
-  · simp [h, BitVec.msb]
-
-
-
-
-  unfold signExtend
-
-  rw [msb_eq_getLsbD_last]
-  simp only [getLsbD_setWidth]
-  cases getLsbD x (v - 1) <;> simp; omega
+theorem msb_SignExtend {x : BitVec w} :
+    (x.signExtend v).msb = (decide (0 < v) && if w ≥ v then x.getMsbD (w - v) else x.msb) := by
+  simp [BitVec.msb, getMsbD_signExtend]
+  by_cases h : w ≥ v
+  · simp [h, show v - w = 0 by omega]
+  · simp [h, show ¬ (v - w = 0) by omega]
 
 /-- Sign extending to a width smaller than the starting width is a truncation. -/
 theorem signExtend_eq_setWidth_of_lt (x : BitVec w) {v : Nat} (hv : v ≤ w):
@@ -1915,8 +1875,9 @@ theorem append_zero {n m : Nat} {x : BitVec n} :
     x ++ 0#m = x.signExtend (n + m) <<< m := by
   induction m
   case zero =>
-    simp
+    simp [signExtend]
   case succ i ih =>
+    simp [bv_toNat]
     sorry
 
 def lhs (x : BitVec n) (y : BitVec m) : Int := (x++y).toInt