From b630163eb3eac51e726afbe0e15e37c84e1530bc Mon Sep 17 00:00:00 2001
From: "F. G. Dorais" <fgdorais@gmail.com>
Date: Mon, 23 Dec 2024 01:05:50 -0500
Subject: [PATCH 01/13] feat: add BitVec.ofFn and lemmas

---
 Batteries.lean             |  1 +
 Batteries/Data/BitVec.lean | 42 ++++++++++++++++++++++++++++++++++++++
 2 files changed, 43 insertions(+)
 create mode 100644 Batteries/Data/BitVec.lean

diff --git a/Batteries.lean b/Batteries.lean
index 1efcac66e7..0ffa2ffe02 100644
--- a/Batteries.lean
+++ b/Batteries.lean
@@ -16,6 +16,7 @@ import Batteries.Data.Array
 import Batteries.Data.AssocList
 import Batteries.Data.BinaryHeap
 import Batteries.Data.BinomialHeap
+import Batteries.Data.BitVec
 import Batteries.Data.ByteArray
 import Batteries.Data.ByteSubarray
 import Batteries.Data.Char
diff --git a/Batteries/Data/BitVec.lean b/Batteries/Data/BitVec.lean
new file mode 100644
index 0000000000..28d2ed3802
--- /dev/null
+++ b/Batteries/Data/BitVec.lean
@@ -0,0 +1,42 @@
+/-
+Copyright (c) 2024 François G. Dorais. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: François G. Dorais
+-/
+
+namespace BitVec
+
+theorem getElem_shifConcat (v : BitVec n) (b : Bool) (i) (h : i < n) :
+    (v.shiftConcat b)[i] = if i = 0 then b else v[i-1] := by
+  rw [← getLsbD_eq_getElem, getLsbD_shiftConcat, getLsbD_eq_getElem, decide_eq_true h,
+    Bool.true_and]
+
+@[simp] theorem getElem_shiftConcat_zero (v : BitVec n) (b : Bool) (h : 0 < n) :
+    (v.shiftConcat b)[0] = b := by simp [getElem_shifConcat]
+
+@[simp] theorem getElem_shiftConcat_succ (v : BitVec n) (b : Bool) (h : i + 1 < n) :
+    (v.shiftConcat b)[i+1] = v[i] := by simp [getElem_shifConcat]
+
+/-- `ofFnAux f` returns the `BitVec m` whose `i`th bit is `f i` when `i < m` -/
+@[inline] def ofFnAux (m : Nat) (f : Fin n → Bool) : BitVec m :=
+  Fin.foldr n (fun i v => v.shiftConcat (f i)) 0
+
+/-- `ofFn f` returns the `BitVec n` whose `i`th bit is `f i` -/
+abbrev ofFn (f : Fin n → Bool) : BitVec n := ofFnAux n f
+
+theorem getElem_ofFnAux (f : Fin n → Bool) (i) (h : i < n) (h' : i < m) :
+    (ofFnAux m f)[i] = f ⟨i, h⟩ := by
+  simp only [ofFnAux]
+  induction n generalizing i m with
+  | zero => contradiction
+  | succ n ih =>
+    simp only [Fin.foldr_succ, getElem_shifConcat]
+    cases i with
+    | zero =>
+      simp
+    | succ i =>
+      rw [ih (fun i => f i.succ)] <;> try omega
+      simp
+
+@[simp] theorem getElem_ofFn (f : Fin n → Bool) (i) (h : i < n) : (ofFn f)[i] = f ⟨i, h⟩ :=
+  getElem_ofFnAux ..

From f7ae994588f4ed1f3f0f41837ca24476eeb139e5 Mon Sep 17 00:00:00 2001
From: "F. G. Dorais" <fgdorais@gmail.com>
Date: Sat, 4 Jan 2025 20:27:39 -0500
Subject: [PATCH 02/13] feat: do both LE and BE versions

---
 Batteries/Data/BitVec.lean | 25 ++++++++++++++++---------
 1 file changed, 16 insertions(+), 9 deletions(-)

diff --git a/Batteries/Data/BitVec.lean b/Batteries/Data/BitVec.lean
index 28d2ed3802..28b1b8fe7e 100644
--- a/Batteries/Data/BitVec.lean
+++ b/Batteries/Data/BitVec.lean
@@ -17,16 +17,16 @@ theorem getElem_shifConcat (v : BitVec n) (b : Bool) (i) (h : i < n) :
 @[simp] theorem getElem_shiftConcat_succ (v : BitVec n) (b : Bool) (h : i + 1 < n) :
     (v.shiftConcat b)[i+1] = v[i] := by simp [getElem_shifConcat]
 
-/-- `ofFnAux f` returns the `BitVec m` whose `i`th bit is `f i` when `i < m` -/
-@[inline] def ofFnAux (m : Nat) (f : Fin n → Bool) : BitVec m :=
+/-- `ofFnLEAux f` returns the `BitVec m` whose `i`th bit is `f i` when `i < m`, little endian. -/
+@[inline] def ofFnLEAux (m : Nat) (f : Fin n → Bool) : BitVec m :=
   Fin.foldr n (fun i v => v.shiftConcat (f i)) 0
 
-/-- `ofFn f` returns the `BitVec n` whose `i`th bit is `f i` -/
-abbrev ofFn (f : Fin n → Bool) : BitVec n := ofFnAux n f
+/-- `ofFnLE f` returns the `BitVec n` whose `i`th bit is `f i` with little endian ordering. -/
+abbrev ofFnLE (f : Fin n → Bool) : BitVec n := ofFnLEAux n f
 
-theorem getElem_ofFnAux (f : Fin n → Bool) (i) (h : i < n) (h' : i < m) :
-    (ofFnAux m f)[i] = f ⟨i, h⟩ := by
-  simp only [ofFnAux]
+theorem getElem_ofFnLEAux (f : Fin n → Bool) (i) (h : i < n) (h' : i < m) :
+    (ofFnLEAux m f)[i] = f ⟨i, h⟩ := by
+  simp only [ofFnLEAux]
   induction n generalizing i m with
   | zero => contradiction
   | succ n ih =>
@@ -38,5 +38,12 @@ theorem getElem_ofFnAux (f : Fin n → Bool) (i) (h : i < n) (h' : i < m) :
       rw [ih (fun i => f i.succ)] <;> try omega
       simp
 
-@[simp] theorem getElem_ofFn (f : Fin n → Bool) (i) (h : i < n) : (ofFn f)[i] = f ⟨i, h⟩ :=
-  getElem_ofFnAux ..
+@[simp] theorem getElem_ofFnLE (f : Fin n → Bool) (i) (h : i < n) : (ofFnLE f)[i] = f ⟨i, h⟩ :=
+  getElem_ofFnLEAux ..
+
+/-- `ofFnBE f` returns the `BitVec n` whose `i`th bit is `f i` with big endian ordering. -/
+def ofFnBE (f : Fin n → Bool) : BitVec n :=
+  ofFnLE fun i => f i.rev
+
+@[simp] theorem getElem_ofFnBE (f : Fin n → Bool) (i) (h : i < n) :
+    (ofFnBE f)[i] = f (Fin.rev ⟨i, h⟩) := by simp [ofFnBE]

From 1f26464dba80b86055788b5f1dab7562dc03a37a Mon Sep 17 00:00:00 2001
From: "F. G. Dorais" <fgdorais@gmail.com>
Date: Sun, 5 Jan 2025 11:57:50 -0500
Subject: [PATCH 03/13] feat: more getter lemmas

---
 Batteries/Data/BitVec.lean | 16 +++++++++++++---
 1 file changed, 13 insertions(+), 3 deletions(-)

diff --git a/Batteries/Data/BitVec.lean b/Batteries/Data/BitVec.lean
index 28b1b8fe7e..a02000cf01 100644
--- a/Batteries/Data/BitVec.lean
+++ b/Batteries/Data/BitVec.lean
@@ -22,7 +22,7 @@ theorem getElem_shifConcat (v : BitVec n) (b : Bool) (i) (h : i < n) :
   Fin.foldr n (fun i v => v.shiftConcat (f i)) 0
 
 /-- `ofFnLE f` returns the `BitVec n` whose `i`th bit is `f i` with little endian ordering. -/
-abbrev ofFnLE (f : Fin n → Bool) : BitVec n := ofFnLEAux n f
+@[inline] def ofFnLE (f : Fin n → Bool) : BitVec n := ofFnLEAux n f
 
 theorem getElem_ofFnLEAux (f : Fin n → Bool) (i) (h : i < n) (h' : i < m) :
     (ofFnLEAux m f)[i] = f ⟨i, h⟩ := by
@@ -41,9 +41,19 @@ theorem getElem_ofFnLEAux (f : Fin n → Bool) (i) (h : i < n) (h' : i < m) :
 @[simp] theorem getElem_ofFnLE (f : Fin n → Bool) (i) (h : i < n) : (ofFnLE f)[i] = f ⟨i, h⟩ :=
   getElem_ofFnLEAux ..
 
+theorem getLsb'_ofFnLE (f : Fin n → Bool) (i) : (ofFnLE f).getLsb' i = f i := by simp
+
+@[simp] theorem getMsb'_ofFnLE (f : Fin n → Bool) (i) : (ofFnLE f).getMsb' i = f i.rev := by
+  simp [getMsb'_eq_getLsb', Fin.rev]; congr 2; omega
+
 /-- `ofFnBE f` returns the `BitVec n` whose `i`th bit is `f i` with big endian ordering. -/
-def ofFnBE (f : Fin n → Bool) : BitVec n :=
-  ofFnLE fun i => f i.rev
+@[inline] def ofFnBE (f : Fin n → Bool) : BitVec n := ofFnLE fun i => f i.rev
 
 @[simp] theorem getElem_ofFnBE (f : Fin n → Bool) (i) (h : i < n) :
     (ofFnBE f)[i] = f (Fin.rev ⟨i, h⟩) := by simp [ofFnBE]
+
+theorem getLsb'_ofFnBE (f : Fin n → Bool) (i) : (ofFnBE f).getLsb' i = f i.rev := by
+  simp
+
+@[simp] theorem getMsb'_ofFnBE (f : Fin n → Bool) (i) : (ofFnBE f).getMsb' i = f i := by
+  simp [ofFnBE]

From d8bd13d9904d1f370f19a4261c6f84c273a3ade0 Mon Sep 17 00:00:00 2001
From: "F. G. Dorais" <fgdorais@gmail.com>
Date: Sun, 5 Jan 2025 18:19:42 -0500
Subject: [PATCH 04/13] feat: add Nat.ofBits and Fin.ofBits

---
 Batteries/Data/BitVec.lean     | 29 +++++++++++++++++++++++
 Batteries/Data/Fin.lean        |  1 +
 Batteries/Data/Fin/OfBits.lean | 14 +++++++++++
 Batteries/Data/Nat.lean        |  2 ++
 Batteries/Data/Nat/OfBits.lean | 43 ++++++++++++++++++++++++++++++++++
 5 files changed, 89 insertions(+)
 create mode 100644 Batteries/Data/Fin/OfBits.lean
 create mode 100644 Batteries/Data/Nat/OfBits.lean

diff --git a/Batteries/Data/BitVec.lean b/Batteries/Data/BitVec.lean
index a02000cf01..475384cf46 100644
--- a/Batteries/Data/BitVec.lean
+++ b/Batteries/Data/BitVec.lean
@@ -4,6 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: François G. Dorais
 -/
 
+import Batteries.Data.Fin.OfBits
+
 namespace BitVec
 
 theorem getElem_shifConcat (v : BitVec n) (b : Bool) (i) (h : i < n) :
@@ -21,9 +23,30 @@ theorem getElem_shifConcat (v : BitVec n) (b : Bool) (i) (h : i < n) :
 @[inline] def ofFnLEAux (m : Nat) (f : Fin n → Bool) : BitVec m :=
   Fin.foldr n (fun i v => v.shiftConcat (f i)) 0
 
+@[simp] theorem toNat_ofFnLEAux (m : Nat) (f : Fin n → Bool) :
+    (ofFnLEAux m f).toNat = Nat.ofBits f % 2 ^ m := by
+  simp only [ofFnLEAux]
+  induction n with
+  | zero => rfl
+  | succ n ih =>
+    rw [Fin.foldr_succ, toNat_shiftConcat, Nat.shiftLeft_eq, Nat.pow_one, Nat.ofBits_succ, ih,
+      ← Nat.mod_add_div (Nat.ofBits (f ∘ Fin.succ)) (2 ^ m), Nat.mul_add 2, Nat.add_right_comm,
+      Nat.mul_left_comm, Nat.add_mul_mod_self_left, Nat.mul_comm 2]
+    rfl
+
+@[simp] theorem toFin_ofFnLEAux (m : Nat) (f : Fin n → Bool) :
+    (ofFnLEAux m f).toFin = Fin.ofNat' (2 ^ m) (Nat.ofBits f) := by
+  ext; simp
+
 /-- `ofFnLE f` returns the `BitVec n` whose `i`th bit is `f i` with little endian ordering. -/
 @[inline] def ofFnLE (f : Fin n → Bool) : BitVec n := ofFnLEAux n f
 
+@[simp] theorem toNat_ofFnLE (f : Fin n → Bool) : (ofFnLE f).toNat = Nat.ofBits f := by
+  rw [ofFnLE, toNat_ofFnLEAux, Nat.mod_eq_of_lt (Nat.ofBits_lt_two_pow f)]
+
+@[simp] theorem toFin_ofFnLE (f : Fin n → Bool) : (ofFnLE f).toFin = Fin.ofBits f := by
+  ext; simp
+
 theorem getElem_ofFnLEAux (f : Fin n → Bool) (i) (h : i < n) (h' : i < m) :
     (ofFnLEAux m f)[i] = f ⟨i, h⟩ := by
   simp only [ofFnLEAux]
@@ -49,6 +72,12 @@ theorem getLsb'_ofFnLE (f : Fin n → Bool) (i) : (ofFnLE f).getLsb' i = f i :=
 /-- `ofFnBE f` returns the `BitVec n` whose `i`th bit is `f i` with big endian ordering. -/
 @[inline] def ofFnBE (f : Fin n → Bool) : BitVec n := ofFnLE fun i => f i.rev
 
+@[simp] theorem toNat_ofFnBE (f : Fin n → Bool) : (ofFnBE f).toNat = Nat.ofBits (f ∘ Fin.rev) := by
+  simp [ofFnBE]; rfl
+
+@[simp] theorem toFin_ofFnBE (f : Fin n → Bool) : (ofFnBE f).toFin = Fin.ofBits (f ∘ Fin.rev) := by
+  ext; simp
+
 @[simp] theorem getElem_ofFnBE (f : Fin n → Bool) (i) (h : i < n) :
     (ofFnBE f)[i] = f (Fin.rev ⟨i, h⟩) := by simp [ofFnBE]
 
diff --git a/Batteries/Data/Fin.lean b/Batteries/Data/Fin.lean
index 7a5b9c16e8..c40ed38466 100644
--- a/Batteries/Data/Fin.lean
+++ b/Batteries/Data/Fin.lean
@@ -1,3 +1,4 @@
 import Batteries.Data.Fin.Basic
 import Batteries.Data.Fin.Fold
 import Batteries.Data.Fin.Lemmas
+import Batteries.Data.Fin.OfBits
diff --git a/Batteries/Data/Fin/OfBits.lean b/Batteries/Data/Fin/OfBits.lean
new file mode 100644
index 0000000000..dbff248739
--- /dev/null
+++ b/Batteries/Data/Fin/OfBits.lean
@@ -0,0 +1,14 @@
+/-
+Copyright (c) 2025 François G. Dorais. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: François G. Dorais
+-/
+
+import Batteries.Data.Nat.OfBits
+
+namespace Fin
+
+/-- Construct a `Fin (2 ^ n)` element from bit values (little endian). -/
+abbrev ofBits (f : Fin n → Bool) : Fin (2 ^ n) := ⟨Nat.ofBits f, Nat.ofBits_lt_two_pow f⟩
+
+theorem val_ofBits (f : Fin n → Bool) : (ofBits f).val = Nat.ofBits f := rfl
diff --git a/Batteries/Data/Nat.lean b/Batteries/Data/Nat.lean
index dbf3161213..ff32e03dfc 100644
--- a/Batteries/Data/Nat.lean
+++ b/Batteries/Data/Nat.lean
@@ -2,3 +2,5 @@ import Batteries.Data.Nat.Basic
 import Batteries.Data.Nat.Bisect
 import Batteries.Data.Nat.Gcd
 import Batteries.Data.Nat.Lemmas
+import Batteries.Data.Nat.OfBits
+
diff --git a/Batteries/Data/Nat/OfBits.lean b/Batteries/Data/Nat/OfBits.lean
new file mode 100644
index 0000000000..7aef651ccb
--- /dev/null
+++ b/Batteries/Data/Nat/OfBits.lean
@@ -0,0 +1,43 @@
+/-
+Copyright (c) 2025 François G. Dorais. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: François G. Dorais
+-/
+
+namespace Nat
+
+/-- Construct a natural number from bit values (little endian). -/
+@[inline] def ofBits (f : Fin n → Bool) : Nat :=
+  Fin.foldr n (fun i v => 2 * v + (f i).toNat) 0
+
+@[simp] theorem ofBits_zero (f : Fin 0 → Bool) : ofBits f = 0 := rfl
+
+@[simp] theorem ofBits_one (f : Fin 1 → Bool) : ofBits f = (f 0).toNat := Nat.zero_add ..
+
+theorem ofBits_succ (f : Fin (n+1) → Bool) : ofBits f = 2 * ofBits (f ∘ Fin.succ) + (f 0).toNat := by
+  simp [ofBits, Fin.foldr_succ]
+
+theorem ofBits_lt_two_pow (f : Fin n → Bool) : ofBits f < 2 ^ n := by
+  induction n with
+  | zero => simp
+  | succ n ih =>
+    calc ofBits f
+        = 2 * ofBits (f ∘ Fin.succ) + (f 0).toNat := ofBits_succ ..
+      _ ≤ 2 * ofBits (f ∘ Fin.succ) + 1 := Nat.add_le_add_left (Bool.toNat_le _) ..
+      _ < 2 * (ofBits (f ∘ Fin.succ) + 1) := Nat.lt_add_one ..
+      _ ≤ 2 * 2 ^ n := Nat.mul_le_mul_left 2 (Nat.succ_le_of_lt (ih _))
+      _ = 2 ^ (n + 1) := (Nat.pow_add_one' ..).symm
+
+@[simp] theorem testBit_ofBits (f : Fin n → Bool) (i) (h : i < n) :
+    (ofBits f).testBit i = f ⟨i, h⟩ := by
+  induction n generalizing i with
+  | zero => contradiction
+  | succ n ih =>
+    have h0 : (f 0).toNat < 2 := Bool.toNat_lt _
+    match i with
+    | 0 =>
+      rw [ofBits_succ, testBit_zero, Nat.mul_add_mod, Nat.mod_eq_of_lt h0, Fin.zero_eta]
+      cases f 0 <;> rfl
+    | i+1 =>
+      rw [ofBits_succ, testBit_add_one, Nat.mul_add_div Nat.zero_lt_two, Nat.div_eq_of_lt h0]
+      exact ih (f ∘ Fin.succ) i (Nat.lt_of_succ_lt_succ h)

From 7a8b3e2d08791be43f27cf8827480ea1effb6aa8 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois=20G=2E=20Dorais?= <fgdorais@gmail.com>
Date: Sun, 5 Jan 2025 18:24:14 -0500
Subject: [PATCH 05/13] fix: typo

Co-authored-by: Kim Morrison <kim@tqft.net>
---
 Batteries/Data/BitVec.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Batteries/Data/BitVec.lean b/Batteries/Data/BitVec.lean
index 475384cf46..213fc603e7 100644
--- a/Batteries/Data/BitVec.lean
+++ b/Batteries/Data/BitVec.lean
@@ -8,7 +8,7 @@ import Batteries.Data.Fin.OfBits
 
 namespace BitVec
 
-theorem getElem_shifConcat (v : BitVec n) (b : Bool) (i) (h : i < n) :
+theorem getElem_shiftConcat (v : BitVec n) (b : Bool) (i) (h : i < n) :
     (v.shiftConcat b)[i] = if i = 0 then b else v[i-1] := by
   rw [← getLsbD_eq_getElem, getLsbD_shiftConcat, getLsbD_eq_getElem, decide_eq_true h,
     Bool.true_and]

From 4613b2ebac225796d9d492a56f313e6d51c545ab Mon Sep 17 00:00:00 2001
From: "F. G. Dorais" <fgdorais@gmail.com>
Date: Sun, 5 Jan 2025 18:25:14 -0500
Subject: [PATCH 06/13] fix: long line

---
 Batteries/Data/Nat/OfBits.lean | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/Batteries/Data/Nat/OfBits.lean b/Batteries/Data/Nat/OfBits.lean
index 7aef651ccb..2bee937bd5 100644
--- a/Batteries/Data/Nat/OfBits.lean
+++ b/Batteries/Data/Nat/OfBits.lean
@@ -14,7 +14,8 @@ namespace Nat
 
 @[simp] theorem ofBits_one (f : Fin 1 → Bool) : ofBits f = (f 0).toNat := Nat.zero_add ..
 
-theorem ofBits_succ (f : Fin (n+1) → Bool) : ofBits f = 2 * ofBits (f ∘ Fin.succ) + (f 0).toNat := by
+theorem ofBits_succ (f : Fin (n+1) → Bool) :
+    ofBits f = 2 * ofBits (f ∘ Fin.succ) + (f 0).toNat := by
   simp [ofBits, Fin.foldr_succ]
 
 theorem ofBits_lt_two_pow (f : Fin n → Bool) : ofBits f < 2 ^ n := by

From 66a77249f2492948a66d2893efd817089546bd1f Mon Sep 17 00:00:00 2001
From: "F. G. Dorais" <fgdorais@gmail.com>
Date: Sun, 5 Jan 2025 18:46:53 -0500
Subject: [PATCH 07/13] fix: typos

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

diff --git a/Batteries/Data/BitVec.lean b/Batteries/Data/BitVec.lean
index 213fc603e7..ee109fdc3f 100644
--- a/Batteries/Data/BitVec.lean
+++ b/Batteries/Data/BitVec.lean
@@ -14,10 +14,10 @@ theorem getElem_shiftConcat (v : BitVec n) (b : Bool) (i) (h : i < n) :
     Bool.true_and]
 
 @[simp] theorem getElem_shiftConcat_zero (v : BitVec n) (b : Bool) (h : 0 < n) :
-    (v.shiftConcat b)[0] = b := by simp [getElem_shifConcat]
+    (v.shiftConcat b)[0] = b := by simp [getElem_shiftConcat]
 
 @[simp] theorem getElem_shiftConcat_succ (v : BitVec n) (b : Bool) (h : i + 1 < n) :
-    (v.shiftConcat b)[i+1] = v[i] := by simp [getElem_shifConcat]
+    (v.shiftConcat b)[i+1] = v[i] := by simp [getElem_shiftConcat]
 
 /-- `ofFnLEAux f` returns the `BitVec m` whose `i`th bit is `f i` when `i < m`, little endian. -/
 @[inline] def ofFnLEAux (m : Nat) (f : Fin n → Bool) : BitVec m :=
@@ -53,7 +53,7 @@ theorem getElem_ofFnLEAux (f : Fin n → Bool) (i) (h : i < n) (h' : i < m) :
   induction n generalizing i m with
   | zero => contradiction
   | succ n ih =>
-    simp only [Fin.foldr_succ, getElem_shifConcat]
+    simp only [Fin.foldr_succ, getElem_shiftConcat]
     cases i with
     | zero =>
       simp

From 4b995c9814d7915e7e4dfdd343ea235814ccd922 Mon Sep 17 00:00:00 2001
From: "F. G. Dorais" <fgdorais@gmail.com>
Date: Sun, 5 Jan 2025 20:34:32 -0500
Subject: [PATCH 08/13] feat: add `Int.testBit` and `Int.ofBits`

---
 Batteries.lean                 |  1 +
 Batteries/Data/Int.lean        |  1 +
 Batteries/Data/Int/OfBits.lean | 33 +++++++++++++++++++++++++++++++++
 Batteries/Data/Nat/OfBits.lean | 15 +++++++++++++--
 4 files changed, 48 insertions(+), 2 deletions(-)
 create mode 100644 Batteries/Data/Int.lean
 create mode 100644 Batteries/Data/Int/OfBits.lean

diff --git a/Batteries.lean b/Batteries.lean
index 6934764076..fc6c81cec2 100644
--- a/Batteries.lean
+++ b/Batteries.lean
@@ -24,6 +24,7 @@ import Batteries.Data.DList
 import Batteries.Data.Fin
 import Batteries.Data.FloatArray
 import Batteries.Data.HashMap
+import Batteries.Data.Int
 import Batteries.Data.LazyList
 import Batteries.Data.List
 import Batteries.Data.MLList
diff --git a/Batteries/Data/Int.lean b/Batteries/Data/Int.lean
new file mode 100644
index 0000000000..614e7851c6
--- /dev/null
+++ b/Batteries/Data/Int.lean
@@ -0,0 +1 @@
+import Batteries.Data.Int.OfBits
diff --git a/Batteries/Data/Int/OfBits.lean b/Batteries/Data/Int/OfBits.lean
new file mode 100644
index 0000000000..984b9db86f
--- /dev/null
+++ b/Batteries/Data/Int/OfBits.lean
@@ -0,0 +1,33 @@
+/-
+Copyright (c) 2025 François G. Dorais. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: François G. Dorais
+-/
+
+import Batteries.Data.Nat.OfBits
+
+namespace Int
+
+/-- `testBit m n` returns whether the `n+1` least significant bit is `1` or `0` -/
+@[inline] def testBit : Int → Nat → Bool
+  | .ofNat m, n => Nat.testBit m n
+  | .negSucc m, n => ! Nat.testBit m n
+
+
+/--
+Construct an integer from bit values (little endian).
+
+If `fill` is false, the result will be a nonnegative integer with all higher unspecified bits zero.
+If `fill` is true, the result will be a negative integer with all higher unspecified bits one.
+-/
+@[inline] def ofBits (f : Fin n → Bool) : (fill : Bool := false) → Int
+  | false => Int.ofNat (Nat.ofBits f)
+  | true => Int.negSucc (Nat.ofBits fun i => ! f i)
+
+@[simp] theorem testBit_ofBits_lt (f : Fin n → Bool) (fill : Bool) (i) (h : i < n) :
+    (ofBits f fill).testBit i = f ⟨i, h⟩ := by
+  cases fill <;> simp [ofBits, testBit, h]
+
+@[simp] theorem testBit_ofBits_ge (f : Fin n → Bool) (fill : Bool) (i) (h : n ≤ i) :
+    (ofBits f fill).testBit i = fill := by
+  cases fill <;> simp [ofBits, testBit, h]
diff --git a/Batteries/Data/Nat/OfBits.lean b/Batteries/Data/Nat/OfBits.lean
index 2bee937bd5..13c839083f 100644
--- a/Batteries/Data/Nat/OfBits.lean
+++ b/Batteries/Data/Nat/OfBits.lean
@@ -29,12 +29,12 @@ theorem ofBits_lt_two_pow (f : Fin n → Bool) : ofBits f < 2 ^ n := by
       _ ≤ 2 * 2 ^ n := Nat.mul_le_mul_left 2 (Nat.succ_le_of_lt (ih _))
       _ = 2 ^ (n + 1) := (Nat.pow_add_one' ..).symm
 
-@[simp] theorem testBit_ofBits (f : Fin n → Bool) (i) (h : i < n) :
+@[simp] theorem testBit_ofBits_lt (f : Fin n → Bool) (i) (h : i < n) :
     (ofBits f).testBit i = f ⟨i, h⟩ := by
   induction n generalizing i with
   | zero => contradiction
   | succ n ih =>
-    have h0 : (f 0).toNat < 2 := Bool.toNat_lt _
+    have h0 : (f 0).toNat < 2 := Bool.toNat_lt ..
     match i with
     | 0 =>
       rw [ofBits_succ, testBit_zero, Nat.mul_add_mod, Nat.mod_eq_of_lt h0, Fin.zero_eta]
@@ -42,3 +42,14 @@ theorem ofBits_lt_two_pow (f : Fin n → Bool) : ofBits f < 2 ^ n := by
     | i+1 =>
       rw [ofBits_succ, testBit_add_one, Nat.mul_add_div Nat.zero_lt_two, Nat.div_eq_of_lt h0]
       exact ih (f ∘ Fin.succ) i (Nat.lt_of_succ_lt_succ h)
+
+@[simp] theorem testBit_ofBits_ge (f : Fin n → Bool) (i) (h : n ≤ i) :
+    (ofBits f).testBit i = false := by
+  induction n generalizing i with
+  | zero => simp
+  | succ n ih =>
+    have h0 : (f 0).toNat < 2 := Bool.toNat_lt ..
+    match i with
+    | i+1 =>
+      rw [ofBits_succ, testBit_succ, Nat.mul_add_div Nat.zero_lt_two, Nat.div_eq_of_lt h0]
+      exact ih (f ∘ Fin.succ) i (Nat.le_of_succ_le_succ h)

From 9ac228f4e6e6aadde0fd185104009f82156bc1f3 Mon Sep 17 00:00:00 2001
From: "F. G. Dorais" <fgdorais@gmail.com>
Date: Sun, 5 Jan 2025 21:04:24 -0500
Subject: [PATCH 09/13] fix: use sign extension

---
 Batteries/Data/Int/OfBits.lean | 27 ++++++++++++++++++++-------
 1 file changed, 20 insertions(+), 7 deletions(-)

diff --git a/Batteries/Data/Int/OfBits.lean b/Batteries/Data/Int/OfBits.lean
index 984b9db86f..ff28694111 100644
--- a/Batteries/Data/Int/OfBits.lean
+++ b/Batteries/Data/Int/OfBits.lean
@@ -20,14 +20,27 @@ Construct an integer from bit values (little endian).
 If `fill` is false, the result will be a nonnegative integer with all higher unspecified bits zero.
 If `fill` is true, the result will be a negative integer with all higher unspecified bits one.
 -/
-@[inline] def ofBits (f : Fin n → Bool) : (fill : Bool := false) → Int
+@[inline] def ofBitsFill (f : Fin n → Bool) : (fill : Bool := false) → Int
   | false => Int.ofNat (Nat.ofBits f)
   | true => Int.negSucc (Nat.ofBits fun i => ! f i)
 
-@[simp] theorem testBit_ofBits_lt (f : Fin n → Bool) (fill : Bool) (i) (h : i < n) :
-    (ofBits f fill).testBit i = f ⟨i, h⟩ := by
-  cases fill <;> simp [ofBits, testBit, h]
+@[simp] theorem testBit_ofBitsFill_lt (f : Fin n → Bool) (fill : Bool) (i) (h : i < n) :
+    (ofBitsFill f fill).testBit i = f ⟨i, h⟩ := by
+  cases fill <;> simp [ofBitsFill, testBit, h]
 
-@[simp] theorem testBit_ofBits_ge (f : Fin n → Bool) (fill : Bool) (i) (h : n ≤ i) :
-    (ofBits f fill).testBit i = fill := by
-  cases fill <;> simp [ofBits, testBit, h]
+@[simp] theorem testBit_ofBitsFill_ge (f : Fin n → Bool) (fill : Bool) (i) (h : n ≤ i) :
+    (ofBitsFill f fill).testBit i = fill := by
+  cases fill <;> simp [ofBitsFill, testBit, h]
+
+/--
+Construct an integer from bit values (little endian). The most significant specified bit is used to
+determine the sign:
+* If the most significant specified bit is unset then the result will be nonnegative and all
+  higher order bits will read as unset.
+* If the most significant specified bit is set then the result will be negative and all higher
+  order bits will read as set.
+-/
+@[inline] def ofBits (f : Fin n → Bool) : Int :=
+  match n with
+  | 0 => 0
+  | n+1 => ofBitsFill f (f ⟨n, Nat.lt_succ_self n⟩)

From bbe6ae9f7e4ad5486d18007ba78ccc0f507a6918 Mon Sep 17 00:00:00 2001
From: "F. G. Dorais" <fgdorais@gmail.com>
Date: Wed, 8 Jan 2025 20:09:54 -0500
Subject: [PATCH 10/13] feat: add `Nat.ofBits`

---
 Batteries/Data/Nat/Basic.lean  |  7 +++++-
 Batteries/Data/Nat/Lemmas.lean | 42 ++++++++++++++++++++++++++++++++++
 2 files changed, 48 insertions(+), 1 deletion(-)

diff --git a/Batteries/Data/Nat/Basic.lean b/Batteries/Data/Nat/Basic.lean
index 21b4a4dd43..991791687f 100644
--- a/Batteries/Data/Nat/Basic.lean
+++ b/Batteries/Data/Nat/Basic.lean
@@ -6,7 +6,6 @@ Authors: Leonardo de Moura, Jeremy Avigad, Mario Carneiro
 
 namespace Nat
 
-
 /--
   Recursor identical to `Nat.recOn` but uses notations `0` for `Nat.zero` and `·+1` for `Nat.succ`
 -/
@@ -103,3 +102,9 @@ where
     else
       guess
   termination_by guess
+
+/--
+Construct a natural number from a sequence of bits using little endian convention.
+-/
+@[inline] def ofBits (f : Fin n → Bool) : Nat :=
+  Fin.foldr n (fun i v => 2 * v + (f i).toNat) 0
diff --git a/Batteries/Data/Nat/Lemmas.lean b/Batteries/Data/Nat/Lemmas.lean
index a97c558c44..944c473d33 100644
--- a/Batteries/Data/Nat/Lemmas.lean
+++ b/Batteries/Data/Nat/Lemmas.lean
@@ -162,3 +162,45 @@ protected def sum_trichotomy (a b : Nat) : a < b ⊕' a = b ⊕' b < a :=
 
 @[simp] theorem sum_append {l₁ l₂ : List Nat}: (l₁ ++ l₂).sum = l₁.sum + l₂.sum := by
   induction l₁ <;> simp [*, Nat.add_assoc]
+
+/-! ### ofBits -/
+
+@[simp] theorem ofBits_zero (f : Fin 0 → Bool) : ofBits f = 0 := rfl
+
+theorem ofBits_succ (f : Fin (n+1) → Bool) : ofBits f = 2 * ofBits (f ∘ Fin.succ) + (f 0).toNat :=
+  Fin.foldr_succ ..
+
+theorem ofBits_lt_two_pow (f : Fin n → Bool) : ofBits f < 2 ^ n := by
+  induction n with
+  | zero => simp
+  | succ n ih =>
+    calc ofBits f
+        = 2 * ofBits (f ∘ Fin.succ) + (f 0).toNat := ofBits_succ ..
+      _ < 2 * (ofBits (f ∘ Fin.succ) + 1) := Nat.add_lt_add_left (Bool.toNat_lt _) ..
+      _ ≤ 2 * 2 ^ n := Nat.mul_le_mul_left 2 (ih ..)
+      _ = 2 ^ (n + 1) := Nat.pow_add_one' .. |>.symm
+
+@[simp] theorem testBit_ofBits_lt (f : Fin n → Bool) (i : Nat) (h : i < n) :
+    (ofBits f).testBit i = f ⟨i, h⟩ := by
+  induction n generalizing i with
+  | zero => contradiction
+  | succ n ih =>
+    simp only [ofBits_succ]
+    match i with
+    | 0 => simp [mod_eq_of_lt (Bool.toNat_lt _)]
+    | i+1 =>
+      rw [testBit_add_one, mul_add_div Nat.zero_lt_two, Nat.div_eq_of_lt (Bool.toNat_lt _)]
+      exact ih (f ∘ Fin.succ) i (Nat.lt_of_succ_lt_succ h)
+
+@[simp] theorem testBit_ofBits_ge (f : Fin n → Bool) (i : Nat) (h : n ≤ i) :
+    (ofBits f).testBit i = false := by
+  apply testBit_lt_two_pow
+  apply Nat.lt_of_lt_of_le
+  · exact ofBits_lt_two_pow f
+  · exact pow_le_pow_of_le_right Nat.zero_lt_two h
+
+theorem testBit_ofBits (f : Fin n → Bool) :
+    (ofBits f).testBit i = if h : i < n then f ⟨i, h⟩ else false := by
+  cases Nat.lt_or_ge i n with
+  | inl h => simp [h]
+  | inr h => simp [h, Nat.not_lt_of_ge h]

From 287e0900321f45f065e1f3bb55084abb20bfcd08 Mon Sep 17 00:00:00 2001
From: "F. G. Dorais" <fgdorais@gmail.com>
Date: Wed, 8 Jan 2025 20:11:27 -0500
Subject: [PATCH 11/13] feat: add `Fin.ofBits`

---
 Batteries/Data/Fin.lean        |  1 +
 Batteries/Data/Fin/OfBits.lean | 16 ++++++++++++++++
 2 files changed, 17 insertions(+)
 create mode 100644 Batteries/Data/Fin/OfBits.lean

diff --git a/Batteries/Data/Fin.lean b/Batteries/Data/Fin.lean
index 7a5b9c16e8..c40ed38466 100644
--- a/Batteries/Data/Fin.lean
+++ b/Batteries/Data/Fin.lean
@@ -1,3 +1,4 @@
 import Batteries.Data.Fin.Basic
 import Batteries.Data.Fin.Fold
 import Batteries.Data.Fin.Lemmas
+import Batteries.Data.Fin.OfBits
diff --git a/Batteries/Data/Fin/OfBits.lean b/Batteries/Data/Fin/OfBits.lean
new file mode 100644
index 0000000000..55c081eb8b
--- /dev/null
+++ b/Batteries/Data/Fin/OfBits.lean
@@ -0,0 +1,16 @@
+/-
+Copyright (c) 2025 François G. Dorais. All rights reserved.
+Released under Apache 2. license as described in the file LICENSE.
+Authors: François G. Dorais
+-/
+
+import Batteries.Data.Nat.Lemmas
+
+namespace Fin
+
+/--
+Construct an element of `Fin (2 ^ n)` from a sequence of bits (little endian).
+-/
+abbrev ofBits (f : Fin n → Bool) : Fin (2 ^ n) := ⟨Nat.ofBits f, Nat.ofBits_lt_two_pow f⟩
+
+@[simp] theorem val_ofBits (f : Fin n → Bool) : (ofBits f).val = Nat.ofBits f := rfl

From 2ce1194ce8928f3b942ef80bbc331fe0d21dab18 Mon Sep 17 00:00:00 2001
From: "F. G. Dorais" <fgdorais@gmail.com>
Date: Wed, 8 Jan 2025 20:31:33 -0500
Subject: [PATCH 12/13] fix: revert last two commits

---
 Batteries.lean                 |  1 -
 Batteries/Data/Int.lean        |  1 -
 Batteries/Data/Int/OfBits.lean | 46 ----------------------------------
 Batteries/Data/Nat/OfBits.lean | 15 ++---------
 4 files changed, 2 insertions(+), 61 deletions(-)
 delete mode 100644 Batteries/Data/Int.lean
 delete mode 100644 Batteries/Data/Int/OfBits.lean

diff --git a/Batteries.lean b/Batteries.lean
index fc6c81cec2..6934764076 100644
--- a/Batteries.lean
+++ b/Batteries.lean
@@ -24,7 +24,6 @@ import Batteries.Data.DList
 import Batteries.Data.Fin
 import Batteries.Data.FloatArray
 import Batteries.Data.HashMap
-import Batteries.Data.Int
 import Batteries.Data.LazyList
 import Batteries.Data.List
 import Batteries.Data.MLList
diff --git a/Batteries/Data/Int.lean b/Batteries/Data/Int.lean
deleted file mode 100644
index 614e7851c6..0000000000
--- a/Batteries/Data/Int.lean
+++ /dev/null
@@ -1 +0,0 @@
-import Batteries.Data.Int.OfBits
diff --git a/Batteries/Data/Int/OfBits.lean b/Batteries/Data/Int/OfBits.lean
deleted file mode 100644
index ff28694111..0000000000
--- a/Batteries/Data/Int/OfBits.lean
+++ /dev/null
@@ -1,46 +0,0 @@
-/-
-Copyright (c) 2025 François G. Dorais. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: François G. Dorais
--/
-
-import Batteries.Data.Nat.OfBits
-
-namespace Int
-
-/-- `testBit m n` returns whether the `n+1` least significant bit is `1` or `0` -/
-@[inline] def testBit : Int → Nat → Bool
-  | .ofNat m, n => Nat.testBit m n
-  | .negSucc m, n => ! Nat.testBit m n
-
-
-/--
-Construct an integer from bit values (little endian).
-
-If `fill` is false, the result will be a nonnegative integer with all higher unspecified bits zero.
-If `fill` is true, the result will be a negative integer with all higher unspecified bits one.
--/
-@[inline] def ofBitsFill (f : Fin n → Bool) : (fill : Bool := false) → Int
-  | false => Int.ofNat (Nat.ofBits f)
-  | true => Int.negSucc (Nat.ofBits fun i => ! f i)
-
-@[simp] theorem testBit_ofBitsFill_lt (f : Fin n → Bool) (fill : Bool) (i) (h : i < n) :
-    (ofBitsFill f fill).testBit i = f ⟨i, h⟩ := by
-  cases fill <;> simp [ofBitsFill, testBit, h]
-
-@[simp] theorem testBit_ofBitsFill_ge (f : Fin n → Bool) (fill : Bool) (i) (h : n ≤ i) :
-    (ofBitsFill f fill).testBit i = fill := by
-  cases fill <;> simp [ofBitsFill, testBit, h]
-
-/--
-Construct an integer from bit values (little endian). The most significant specified bit is used to
-determine the sign:
-* If the most significant specified bit is unset then the result will be nonnegative and all
-  higher order bits will read as unset.
-* If the most significant specified bit is set then the result will be negative and all higher
-  order bits will read as set.
--/
-@[inline] def ofBits (f : Fin n → Bool) : Int :=
-  match n with
-  | 0 => 0
-  | n+1 => ofBitsFill f (f ⟨n, Nat.lt_succ_self n⟩)
diff --git a/Batteries/Data/Nat/OfBits.lean b/Batteries/Data/Nat/OfBits.lean
index 13c839083f..2bee937bd5 100644
--- a/Batteries/Data/Nat/OfBits.lean
+++ b/Batteries/Data/Nat/OfBits.lean
@@ -29,12 +29,12 @@ theorem ofBits_lt_two_pow (f : Fin n → Bool) : ofBits f < 2 ^ n := by
       _ ≤ 2 * 2 ^ n := Nat.mul_le_mul_left 2 (Nat.succ_le_of_lt (ih _))
       _ = 2 ^ (n + 1) := (Nat.pow_add_one' ..).symm
 
-@[simp] theorem testBit_ofBits_lt (f : Fin n → Bool) (i) (h : i < n) :
+@[simp] theorem testBit_ofBits (f : Fin n → Bool) (i) (h : i < n) :
     (ofBits f).testBit i = f ⟨i, h⟩ := by
   induction n generalizing i with
   | zero => contradiction
   | succ n ih =>
-    have h0 : (f 0).toNat < 2 := Bool.toNat_lt ..
+    have h0 : (f 0).toNat < 2 := Bool.toNat_lt _
     match i with
     | 0 =>
       rw [ofBits_succ, testBit_zero, Nat.mul_add_mod, Nat.mod_eq_of_lt h0, Fin.zero_eta]
@@ -42,14 +42,3 @@ theorem ofBits_lt_two_pow (f : Fin n → Bool) : ofBits f < 2 ^ n := by
     | i+1 =>
       rw [ofBits_succ, testBit_add_one, Nat.mul_add_div Nat.zero_lt_two, Nat.div_eq_of_lt h0]
       exact ih (f ∘ Fin.succ) i (Nat.lt_of_succ_lt_succ h)
-
-@[simp] theorem testBit_ofBits_ge (f : Fin n → Bool) (i) (h : n ≤ i) :
-    (ofBits f).testBit i = false := by
-  induction n generalizing i with
-  | zero => simp
-  | succ n ih =>
-    have h0 : (f 0).toNat < 2 := Bool.toNat_lt ..
-    match i with
-    | i+1 =>
-      rw [ofBits_succ, testBit_succ, Nat.mul_add_div Nat.zero_lt_two, Nat.div_eq_of_lt h0]
-      exact ih (f ∘ Fin.succ) i (Nat.le_of_succ_le_succ h)

From 3673ee9add0b59af8efffaedeb12e5f92ae6d14d Mon Sep 17 00:00:00 2001
From: "F. G. Dorais" <fgdorais@gmail.com>
Date: Wed, 15 Jan 2025 12:46:42 -0500
Subject: [PATCH 13/13] chore: split file

---
 Batteries/Data/BitVec.lean        | 90 +------------------------------
 Batteries/Data/BitVec/Basic.lean  | 19 +++++++
 Batteries/Data/BitVec/Lemmas.lean | 78 +++++++++++++++++++++++++++
 3 files changed, 99 insertions(+), 88 deletions(-)
 create mode 100644 Batteries/Data/BitVec/Basic.lean
 create mode 100644 Batteries/Data/BitVec/Lemmas.lean

diff --git a/Batteries/Data/BitVec.lean b/Batteries/Data/BitVec.lean
index ee109fdc3f..499e18cd7d 100644
--- a/Batteries/Data/BitVec.lean
+++ b/Batteries/Data/BitVec.lean
@@ -1,88 +1,2 @@
-/-
-Copyright (c) 2024 François G. Dorais. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: François G. Dorais
--/
-
-import Batteries.Data.Fin.OfBits
-
-namespace BitVec
-
-theorem getElem_shiftConcat (v : BitVec n) (b : Bool) (i) (h : i < n) :
-    (v.shiftConcat b)[i] = if i = 0 then b else v[i-1] := by
-  rw [← getLsbD_eq_getElem, getLsbD_shiftConcat, getLsbD_eq_getElem, decide_eq_true h,
-    Bool.true_and]
-
-@[simp] theorem getElem_shiftConcat_zero (v : BitVec n) (b : Bool) (h : 0 < n) :
-    (v.shiftConcat b)[0] = b := by simp [getElem_shiftConcat]
-
-@[simp] theorem getElem_shiftConcat_succ (v : BitVec n) (b : Bool) (h : i + 1 < n) :
-    (v.shiftConcat b)[i+1] = v[i] := by simp [getElem_shiftConcat]
-
-/-- `ofFnLEAux f` returns the `BitVec m` whose `i`th bit is `f i` when `i < m`, little endian. -/
-@[inline] def ofFnLEAux (m : Nat) (f : Fin n → Bool) : BitVec m :=
-  Fin.foldr n (fun i v => v.shiftConcat (f i)) 0
-
-@[simp] theorem toNat_ofFnLEAux (m : Nat) (f : Fin n → Bool) :
-    (ofFnLEAux m f).toNat = Nat.ofBits f % 2 ^ m := by
-  simp only [ofFnLEAux]
-  induction n with
-  | zero => rfl
-  | succ n ih =>
-    rw [Fin.foldr_succ, toNat_shiftConcat, Nat.shiftLeft_eq, Nat.pow_one, Nat.ofBits_succ, ih,
-      ← Nat.mod_add_div (Nat.ofBits (f ∘ Fin.succ)) (2 ^ m), Nat.mul_add 2, Nat.add_right_comm,
-      Nat.mul_left_comm, Nat.add_mul_mod_self_left, Nat.mul_comm 2]
-    rfl
-
-@[simp] theorem toFin_ofFnLEAux (m : Nat) (f : Fin n → Bool) :
-    (ofFnLEAux m f).toFin = Fin.ofNat' (2 ^ m) (Nat.ofBits f) := by
-  ext; simp
-
-/-- `ofFnLE f` returns the `BitVec n` whose `i`th bit is `f i` with little endian ordering. -/
-@[inline] def ofFnLE (f : Fin n → Bool) : BitVec n := ofFnLEAux n f
-
-@[simp] theorem toNat_ofFnLE (f : Fin n → Bool) : (ofFnLE f).toNat = Nat.ofBits f := by
-  rw [ofFnLE, toNat_ofFnLEAux, Nat.mod_eq_of_lt (Nat.ofBits_lt_two_pow f)]
-
-@[simp] theorem toFin_ofFnLE (f : Fin n → Bool) : (ofFnLE f).toFin = Fin.ofBits f := by
-  ext; simp
-
-theorem getElem_ofFnLEAux (f : Fin n → Bool) (i) (h : i < n) (h' : i < m) :
-    (ofFnLEAux m f)[i] = f ⟨i, h⟩ := by
-  simp only [ofFnLEAux]
-  induction n generalizing i m with
-  | zero => contradiction
-  | succ n ih =>
-    simp only [Fin.foldr_succ, getElem_shiftConcat]
-    cases i with
-    | zero =>
-      simp
-    | succ i =>
-      rw [ih (fun i => f i.succ)] <;> try omega
-      simp
-
-@[simp] theorem getElem_ofFnLE (f : Fin n → Bool) (i) (h : i < n) : (ofFnLE f)[i] = f ⟨i, h⟩ :=
-  getElem_ofFnLEAux ..
-
-theorem getLsb'_ofFnLE (f : Fin n → Bool) (i) : (ofFnLE f).getLsb' i = f i := by simp
-
-@[simp] theorem getMsb'_ofFnLE (f : Fin n → Bool) (i) : (ofFnLE f).getMsb' i = f i.rev := by
-  simp [getMsb'_eq_getLsb', Fin.rev]; congr 2; omega
-
-/-- `ofFnBE f` returns the `BitVec n` whose `i`th bit is `f i` with big endian ordering. -/
-@[inline] def ofFnBE (f : Fin n → Bool) : BitVec n := ofFnLE fun i => f i.rev
-
-@[simp] theorem toNat_ofFnBE (f : Fin n → Bool) : (ofFnBE f).toNat = Nat.ofBits (f ∘ Fin.rev) := by
-  simp [ofFnBE]; rfl
-
-@[simp] theorem toFin_ofFnBE (f : Fin n → Bool) : (ofFnBE f).toFin = Fin.ofBits (f ∘ Fin.rev) := by
-  ext; simp
-
-@[simp] theorem getElem_ofFnBE (f : Fin n → Bool) (i) (h : i < n) :
-    (ofFnBE f)[i] = f (Fin.rev ⟨i, h⟩) := by simp [ofFnBE]
-
-theorem getLsb'_ofFnBE (f : Fin n → Bool) (i) : (ofFnBE f).getLsb' i = f i.rev := by
-  simp
-
-@[simp] theorem getMsb'_ofFnBE (f : Fin n → Bool) (i) : (ofFnBE f).getMsb' i = f i := by
-  simp [ofFnBE]
+import Batteries.Data.BitVec.Basic
+import Batteries.Data.BitVec.Lemmas
diff --git a/Batteries/Data/BitVec/Basic.lean b/Batteries/Data/BitVec/Basic.lean
new file mode 100644
index 0000000000..d00c2d2324
--- /dev/null
+++ b/Batteries/Data/BitVec/Basic.lean
@@ -0,0 +1,19 @@
+/-
+Copyright (c) 2024 François G. Dorais. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: François G. Dorais
+-/
+
+import Batteries.Data.Fin.OfBits
+
+namespace BitVec
+
+/-- `ofFnLEAux f` returns the `BitVec m` whose `i`th bit is `f i` when `i < m`, little endian. -/
+@[inline] def ofFnLEAux (m : Nat) (f : Fin n → Bool) : BitVec m :=
+  Fin.foldr n (fun i v => v.shiftConcat (f i)) 0
+
+/-- `ofFnLE f` returns the `BitVec n` whose `i`th bit is `f i` with little endian ordering. -/
+@[inline] def ofFnLE (f : Fin n → Bool) : BitVec n := ofFnLEAux n f
+
+/-- `ofFnBE f` returns the `BitVec n` whose `i`th bit is `f i` with big endian ordering. -/
+@[inline] def ofFnBE (f : Fin n → Bool) : BitVec n := ofFnLE fun i => f i.rev
diff --git a/Batteries/Data/BitVec/Lemmas.lean b/Batteries/Data/BitVec/Lemmas.lean
new file mode 100644
index 0000000000..c08cf55cd7
--- /dev/null
+++ b/Batteries/Data/BitVec/Lemmas.lean
@@ -0,0 +1,78 @@
+/-
+Copyright (c) 2024 François G. Dorais. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: François G. Dorais
+-/
+
+import Batteries.Data.BitVec.Basic
+
+namespace BitVec
+
+theorem getElem_shiftConcat (v : BitVec n) (b : Bool) (i) (h : i < n) :
+    (v.shiftConcat b)[i] = if i = 0 then b else v[i-1] := by
+  rw [← getLsbD_eq_getElem, getLsbD_shiftConcat, getLsbD_eq_getElem, decide_eq_true h,
+    Bool.true_and]
+
+@[simp] theorem getElem_shiftConcat_zero (v : BitVec n) (b : Bool) (h : 0 < n) :
+    (v.shiftConcat b)[0] = b := by simp [getElem_shiftConcat]
+
+@[simp] theorem getElem_shiftConcat_succ (v : BitVec n) (b : Bool) (h : i + 1 < n) :
+    (v.shiftConcat b)[i+1] = v[i] := by simp [getElem_shiftConcat]
+
+@[simp] theorem toNat_ofFnLEAux (m : Nat) (f : Fin n → Bool) :
+    (ofFnLEAux m f).toNat = Nat.ofBits f % 2 ^ m := by
+  simp only [ofFnLEAux]
+  induction n with
+  | zero => rfl
+  | succ n ih =>
+    rw [Fin.foldr_succ, toNat_shiftConcat, Nat.shiftLeft_eq, Nat.pow_one, Nat.ofBits_succ, ih,
+      ← Nat.mod_add_div (Nat.ofBits (f ∘ Fin.succ)) (2 ^ m), Nat.mul_add 2, Nat.add_right_comm,
+      Nat.mul_left_comm, Nat.add_mul_mod_self_left, Nat.mul_comm 2]
+    rfl
+
+@[simp] theorem toFin_ofFnLEAux (m : Nat) (f : Fin n → Bool) :
+    (ofFnLEAux m f).toFin = Fin.ofNat' (2 ^ m) (Nat.ofBits f) := by
+  ext; simp
+
+@[simp] theorem toNat_ofFnLE (f : Fin n → Bool) : (ofFnLE f).toNat = Nat.ofBits f := by
+  rw [ofFnLE, toNat_ofFnLEAux, Nat.mod_eq_of_lt (Nat.ofBits_lt_two_pow f)]
+
+@[simp] theorem toFin_ofFnLE (f : Fin n → Bool) : (ofFnLE f).toFin = Fin.ofBits f := by
+  ext; simp
+
+theorem getElem_ofFnLEAux (f : Fin n → Bool) (i) (h : i < n) (h' : i < m) :
+    (ofFnLEAux m f)[i] = f ⟨i, h⟩ := by
+  simp only [ofFnLEAux]
+  induction n generalizing i m with
+  | zero => contradiction
+  | succ n ih =>
+    simp only [Fin.foldr_succ, getElem_shiftConcat]
+    cases i with
+    | zero =>
+      simp
+    | succ i =>
+      rw [ih (fun i => f i.succ)] <;> try omega
+      simp
+
+@[simp] theorem getElem_ofFnLE (f : Fin n → Bool) (i) (h : i < n) : (ofFnLE f)[i] = f ⟨i, h⟩ :=
+  getElem_ofFnLEAux ..
+
+theorem getLsb'_ofFnLE (f : Fin n → Bool) (i) : (ofFnLE f).getLsb' i = f i := by simp
+
+@[simp] theorem getMsb'_ofFnLE (f : Fin n → Bool) (i) : (ofFnLE f).getMsb' i = f i.rev := by
+  simp [getMsb'_eq_getLsb', Fin.rev]; congr 2; omega
+
+@[simp] theorem toNat_ofFnBE (f : Fin n → Bool) : (ofFnBE f).toNat = Nat.ofBits (f ∘ Fin.rev) := by
+  simp [ofFnBE]; rfl
+
+@[simp] theorem toFin_ofFnBE (f : Fin n → Bool) : (ofFnBE f).toFin = Fin.ofBits (f ∘ Fin.rev) := by
+  ext; simp
+
+@[simp] theorem getElem_ofFnBE (f : Fin n → Bool) (i) (h : i < n) :
+    (ofFnBE f)[i] = f (Fin.rev ⟨i, h⟩) := by simp [ofFnBE]
+
+theorem getLsb'_ofFnBE (f : Fin n → Bool) (i) : (ofFnBE f).getLsb' i = f i.rev := by
+  simp
+
+@[simp] theorem getMsb'_ofFnBE (f : Fin n → Bool) (i) : (ofFnBE f).getMsb' i = f i := by
+  simp [ofFnBE]