From b98d7fa665de87f92958f5e18dbc26c3ab4f0436 Mon Sep 17 00:00:00 2001
From: "F. G. Dorais" <fgdorais@gmail.com>
Date: Mon, 27 May 2024 16:59:31 -0400
Subject: [PATCH 01/25] feat: dependent array type

---
 Batteries.lean             |   2 +
 Batteries/Data/DArray.lean | 108 +++++++++++++++++++++++++++++++++++++
 Batteries/Data/Sigma.lean  |  29 ++++++++++
 3 files changed, 139 insertions(+)
 create mode 100644 Batteries/Data/DArray.lean
 create mode 100644 Batteries/Data/Sigma.lean

diff --git a/Batteries.lean b/Batteries.lean
index f56659960b..ebd3048cd9 100644
--- a/Batteries.lean
+++ b/Batteries.lean
@@ -20,6 +20,7 @@ import Batteries.Data.BitVec
 import Batteries.Data.Bool
 import Batteries.Data.ByteArray
 import Batteries.Data.Char
+import Batteries.Data.DArray
 import Batteries.Data.DList
 import Batteries.Data.Fin
 import Batteries.Data.HashMap
@@ -33,6 +34,7 @@ import Batteries.Data.PairingHeap
 import Batteries.Data.RBMap
 import Batteries.Data.Range
 import Batteries.Data.Rat
+import Batteries.Data.Sigma
 import Batteries.Data.String
 import Batteries.Data.Sum
 import Batteries.Data.UInt
diff --git a/Batteries/Data/DArray.lean b/Batteries/Data/DArray.lean
new file mode 100644
index 0000000000..7bfe901325
--- /dev/null
+++ b/Batteries/Data/DArray.lean
@@ -0,0 +1,108 @@
+/-
+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.Sigma
+
+namespace Batteries
+
+/-- `DArray` is a heterogenous array with element types given by `type`. -/
+structure DArray (size : Nat) (type : Fin size → Type _) where
+  private mk_ ::
+  /-- Data of a `DArray` represented as `Sigma type`. -/
+  data : Array (Sigma type)
+  /-- Data array of `DArray` has correct size. -/
+  size_eq : data.size = size
+  /-- Data of `DArray` have correct types. -/
+  idx_eq (i : Fin size) : data[i].fst = i
+
+namespace DArray
+
+theorem type_eq {type : Fin size → Type _} {a : DArray size type} (i : Fin size)
+    (h : i < a.data.size := a.size_eq.symm ▸ i.is_lt) : a.data[i].type = type i := by
+  rw [Sigma.type, a.idx_eq]
+
+/-- Constructs an `DArray` using `init` as inital values. -/
+protected def mk (init : (i : Fin size) → type i) : DArray size type where
+  data := Array.ofFn fun i => ⟨_, init i⟩
+  size_eq := Array.size_ofFn ..
+  idx_eq _ := Array.getElem_ofFn .. ▸ rfl
+
+/-- Gets the `DArray` item at index `i`. -/
+protected def get (a : DArray size type) (i : Fin size) : type i :=
+  have : i < a.data.size := a.size_eq.symm ▸ i.is_lt
+  a.data[i].castIdx (a.idx_eq i)
+
+/-- Sets the `DArray` item at index `i`. -/
+protected def set (a : DArray size type) (i : Fin size) (v : type i) :
+    DArray size type where
+  data := a.data.set (i.cast a.size_eq.symm) ⟨_, v⟩
+  size_eq := (Array.size_set ..).symm ▸ a.size_eq
+  idx_eq j := by
+    if h : i = j then
+      simp [h]
+    else
+      have h : i.val ≠ j.val := mt Fin.eq_of_val_eq h
+      simp [h]
+      exact a.idx_eq ..
+
+theorem data_getElem {type : Fin size → Type _} (a : DArray size type)
+    (i : Nat) (h : i < size) (h' : i < a.data.size) :
+    a.data[i] = ⟨_, a.get ⟨i, h⟩⟩ := by
+  ext
+  · congr 1; exact a.idx_eq ⟨i, h⟩
+  · exact Sigma.castIdx_heq_val .. |>.symm
+
+theorem data_inj {type : Fin size → Type _} :
+    {a b : DArray size type} → a.data = b.data → a = b
+  | {..}, {..}, rfl => rfl
+
+@[ext]
+protected theorem ext {type : Fin size → Type _} {a b : DArray size type}
+    (h : ∀ i, a.get i = b.get i) : a = b := by
+  apply data_inj
+  apply Array.ext
+  · rw [a.size_eq, b.size_eq]
+  · intro i hia hib
+    have hi : i < size := a.size_eq ▸ hia
+    rw [data_getElem a i hi, data_getElem b i hi]
+    ext
+    · simp
+    · exact heq_of_eq <| h ..
+
+@[simp]
+theorem get_set {type : Fin size → Type _} (a : DArray size type) (i : Fin size) (v : type i) :
+    (a.set i v).get i = v := by
+  simp [DArray.get, DArray.set]
+  exact eq_of_heq <| Sigma.castIdx_heq_val ..
+
+theorem get_set_ne {type : Fin size → Type _} (a : DArray size type) (v : type i) (h : i ≠ j) :
+    (a.set i v).get j = a.get j := by
+  simp [DArray.get, DArray.set]
+  congr 1
+  apply Array.getElem_set_ne
+  apply mt Fin.eq_of_val_eq h
+
+@[simp]
+theorem set_set {type : Fin size → Type _} (a : DArray size type) (i : Fin size)
+    (v w : type i) : (a.set i v).set i w = a.set i w := by
+  ext j
+  if h : i = j then
+    rw [← h, get_set, get_set]
+  else
+    rw [get_set_ne _ _ h, get_set_ne _ _ h, get_set_ne _ _ h]
+
+@[simp]
+theorem get_mk (i : Fin size) : DArray.get (.mk init) i = init i := by
+  simp [DArray.get, DArray.mk]
+  exact eq_of_heq <| Sigma.castIdx_heq_val ..
+
+theorem set_mk {type : Fin size → Type _} {init} (i : Fin size) (v : type i) :
+    DArray.set (.mk init) i v = .mk fun j => if h : i = j then h ▸ v else init j := by
+  ext j
+  if h : i = j then
+    rw [← h, get_set, get_mk, dif_pos rfl]
+  else
+    rw [get_set_ne _ _ h, get_mk, get_mk, dif_neg h]
diff --git a/Batteries/Data/Sigma.lean b/Batteries/Data/Sigma.lean
new file mode 100644
index 0000000000..e55c1a008d
--- /dev/null
+++ b/Batteries/Data/Sigma.lean
@@ -0,0 +1,29 @@
+/-
+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 Sigma
+
+/-- Type value of a `Sigma` object. -/
+protected abbrev type (a : Sigma α) : Type _ := α a.fst
+
+/-- Casts an `Sigma` object to  a value of compatible type. -/
+protected def cast : (a : Sigma α) → a.type = β → β
+  | {snd := a}, rfl => a
+
+/-- Casts an `Sigma` object to  a value of compatible index. -/
+protected def castIdx : (a : Sigma α) → a.fst = i → α i
+  | {snd := a}, rfl => a
+
+@[simp]
+theorem mk_val (a : Sigma α) : ⟨_, a.snd⟩ = a := rfl
+
+@[simp]
+theorem cast_heq_val : (a : Sigma α) → (h : a.type = β) → HEq (a.cast h) a.snd
+  | {..}, rfl => .rfl
+
+@[simp]
+theorem castIdx_heq_val : (a : Sigma α) → (h : a.fst = i) → HEq (a.castIdx h) a.snd
+  | {..}, rfl => .rfl

From 0eca0e0aa3834e84a8413906cd1cf3a7aeb76e01 Mon Sep 17 00:00:00 2001
From: "F. G. Dorais" <fgdorais@gmail.com>
Date: Mon, 27 May 2024 18:21:27 -0400
Subject: [PATCH 02/25] feat: experimental implementation

---
 Batteries/Data/DArray.lean | 27 +++++++++++++++++++++++++++
 test/darray.lean           | 10 ++++++++++
 2 files changed, 37 insertions(+)
 create mode 100644 test/darray.lean

diff --git a/Batteries/Data/DArray.lean b/Batteries/Data/DArray.lean
index 7bfe901325..957021fb32 100644
--- a/Batteries/Data/DArray.lean
+++ b/Batteries/Data/DArray.lean
@@ -106,3 +106,30 @@ theorem set_mk {type : Fin size → Type _} {init} (i : Fin size) (v : type i) :
     rw [← h, get_set, get_mk, dif_pos rfl]
   else
     rw [get_set_ne _ _ h, get_mk, get_mk, dif_neg h]
+
+/- Experimental Unsafe Implementation -/
+
+private unsafe def mkUnsafe (init : (i : Fin size) → type i) : DArray size type :=
+  let data : Array Unit := .ofFn fun i => unsafeCast (init i)
+  unsafeCast data
+
+private unsafe def getUnsafe (a : DArray size type) (i) : type i :=
+  let data : Array Unit := unsafeCast a
+  unsafeCast <| data[i.val]'(lcProof)
+
+private unsafe def setUnsafe (a : DArray size type) (i) (v : type i) : DArray size type :=
+  let data : Array Unit := unsafeCast a
+  unsafeCast <| data.set ⟨i.val, lcProof⟩ <| unsafeCast v
+
+private unsafe def dataUnsafe (a : DArray size type) : Array (Sigma type) :=
+  .ofFn fun i => ⟨_, a.getUnsafe i⟩
+
+private unsafe def mk_Unsafe {type : Fin size → Type _} (data : Array (Sigma type))
+    (size_eq : data.size = size) (idx_eq : ∀ (i : Fin size), data[i].fst = i) : DArray size type :=
+  mkUnsafe fun i => idx_eq i ▸ data[i].snd
+
+attribute [implemented_by mk_Unsafe] DArray.mk_
+attribute [implemented_by mkUnsafe] DArray.mk
+attribute [implemented_by dataUnsafe] DArray.data
+attribute [implemented_by getUnsafe] DArray.get
+attribute [implemented_by setUnsafe] DArray.set
diff --git a/test/darray.lean b/test/darray.lean
new file mode 100644
index 0000000000..9ead1eb240
--- /dev/null
+++ b/test/darray.lean
@@ -0,0 +1,10 @@
+import Batteries.Data.DArray
+
+open Batteries
+
+def foo : DArray 3 fun | 0 => String | 1 => Nat | 2 => Array Nat :=
+  .mk fun | 0 => "foo" | 1 => 42 | 2 => #[4, 2]
+
+#guard foo.get 0 == "foo"
+#guard foo.get 1 == 42
+#guard foo.get 2 == #[4, 2]

From c632cf5a120223376c25399de0097596f5b8927f Mon Sep 17 00:00:00 2001
From: "F. G. Dorais" <fgdorais@gmail.com>
Date: Mon, 27 May 2024 18:41:49 -0400
Subject: [PATCH 03/25] chore: docs and tests

---
 Batteries/Data/DArray.lean | 8 +++++++-
 test/darray.lean           | 4 ++++
 2 files changed, 11 insertions(+), 1 deletion(-)

diff --git a/Batteries/Data/DArray.lean b/Batteries/Data/DArray.lean
index 957021fb32..328c31aab0 100644
--- a/Batteries/Data/DArray.lean
+++ b/Batteries/Data/DArray.lean
@@ -107,7 +107,13 @@ theorem set_mk {type : Fin size → Type _} {init} (i : Fin size) (v : type i) :
   else
     rw [get_set_ne _ _ h, get_mk, get_mk, dif_neg h]
 
-/- Experimental Unsafe Implementation -/
+/-! # Experimental Unsafe Implementation
+
+For this implementation, `DArray n α` is secretly stored as an `Array Unit` with size `n`. This
+works because Lean never actually checks that the objects stored in an array have the appropriate
+type. So it's safe, in principle, to `unsafeCast` the fake `Unit` objects to the appropriate type
+and similarly to `unsafeCast` any relevant object to a fake `Unit` object.
+-/
 
 private unsafe def mkUnsafe (init : (i : Fin size) → type i) : DArray size type :=
   let data : Array Unit := .ofFn fun i => unsafeCast (init i)
diff --git a/test/darray.lean b/test/darray.lean
index 9ead1eb240..494aa67761 100644
--- a/test/darray.lean
+++ b/test/darray.lean
@@ -8,3 +8,7 @@ def foo : DArray 3 fun | 0 => String | 1 => Nat | 2 => Array Nat :=
 #guard foo.get 0 == "foo"
 #guard foo.get 1 == 42
 #guard foo.get 2 == #[4, 2]
+
+#guard (foo.set 1 1).get 0 == "foo"
+#guard (foo.set 1 1).get 1 == 1
+#guard (foo.set 1 1).get 2 == #[4, 2]

From 2e64898f6de673695d082998a6f744c03b94287a Mon Sep 17 00:00:00 2001
From: "F. G. Dorais" <fgdorais@gmail.com>
Date: Mon, 27 May 2024 19:32:09 -0400
Subject: [PATCH 04/25] feat: use inductive model definition

---
 Batteries/Data/DArray.lean | 95 +++++++-------------------------------
 1 file changed, 17 insertions(+), 78 deletions(-)

diff --git a/Batteries/Data/DArray.lean b/Batteries/Data/DArray.lean
index 328c31aab0..2c42c4a1f0 100644
--- a/Batteries/Data/DArray.lean
+++ b/Batteries/Data/DArray.lean
@@ -9,81 +9,30 @@ import Batteries.Data.Sigma
 namespace Batteries
 
 /-- `DArray` is a heterogenous array with element types given by `type`. -/
-structure DArray (size : Nat) (type : Fin size → Type _) where
-  private mk_ ::
-  /-- Data of a `DArray` represented as `Sigma type`. -/
-  data : Array (Sigma type)
-  /-- Data array of `DArray` has correct size. -/
-  size_eq : data.size = size
-  /-- Data of `DArray` have correct types. -/
-  idx_eq (i : Fin size) : data[i].fst = i
+inductive DArray (n) (α : Fin n → Type _) where
+/-- `DArray` constructor. -/
+| mk (get : (i : Fin n) → α i)
 
 namespace DArray
 
-theorem type_eq {type : Fin size → Type _} {a : DArray size type} (i : Fin size)
-    (h : i < a.data.size := a.size_eq.symm ▸ i.is_lt) : a.data[i].type = type i := by
-  rw [Sigma.type, a.idx_eq]
-
-/-- Constructs an `DArray` using `init` as inital values. -/
-protected def mk (init : (i : Fin size) → type i) : DArray size type where
-  data := Array.ofFn fun i => ⟨_, init i⟩
-  size_eq := Array.size_ofFn ..
-  idx_eq _ := Array.getElem_ofFn .. ▸ rfl
-
-/-- Gets the `DArray` item at index `i`. -/
-protected def get (a : DArray size type) (i : Fin size) : type i :=
-  have : i < a.data.size := a.size_eq.symm ▸ i.is_lt
-  a.data[i].castIdx (a.idx_eq i)
+  /-- Gets the `DArray` item at index `i`. -/
+protected def get : DArray n α → (i : Fin n) → α i
+  | mk get => get
 
 /-- Sets the `DArray` item at index `i`. -/
-protected def set (a : DArray size type) (i : Fin size) (v : type i) :
-    DArray size type where
-  data := a.data.set (i.cast a.size_eq.symm) ⟨_, v⟩
-  size_eq := (Array.size_set ..).symm ▸ a.size_eq
-  idx_eq j := by
-    if h : i = j then
-      simp [h]
-    else
-      have h : i.val ≠ j.val := mt Fin.eq_of_val_eq h
-      simp [h]
-      exact a.idx_eq ..
-
-theorem data_getElem {type : Fin size → Type _} (a : DArray size type)
-    (i : Nat) (h : i < size) (h' : i < a.data.size) :
-    a.data[i] = ⟨_, a.get ⟨i, h⟩⟩ := by
-  ext
-  · congr 1; exact a.idx_eq ⟨i, h⟩
-  · exact Sigma.castIdx_heq_val .. |>.symm
-
-theorem data_inj {type : Fin size → Type _} :
-    {a b : DArray size type} → a.data = b.data → a = b
-  | {..}, {..}, rfl => rfl
+protected def set (a : DArray n α) (i : Fin n) (v : α i) : DArray n α :=
+  mk fun j => if h : i = j then h ▸ v else a.get j
 
 @[ext]
-protected theorem ext {type : Fin size → Type _} {a b : DArray size type}
-    (h : ∀ i, a.get i = b.get i) : a = b := by
-  apply data_inj
-  apply Array.ext
-  · rw [a.size_eq, b.size_eq]
-  · intro i hia hib
-    have hi : i < size := a.size_eq ▸ hia
-    rw [data_getElem a i hi, data_getElem b i hi]
-    ext
-    · simp
-    · exact heq_of_eq <| h ..
+protected theorem ext : {a b : DArray n α} → (∀ i, a.get i = b.get i) → a = b
+  | mk _, mk _, h => congrArg _ <| funext fun i => h i
 
 @[simp]
-theorem get_set {type : Fin size → Type _} (a : DArray size type) (i : Fin size) (v : type i) :
-    (a.set i v).get i = v := by
-  simp [DArray.get, DArray.set]
-  exact eq_of_heq <| Sigma.castIdx_heq_val ..
-
-theorem get_set_ne {type : Fin size → Type _} (a : DArray size type) (v : type i) (h : i ≠ j) :
-    (a.set i v).get j = a.get j := by
-  simp [DArray.get, DArray.set]
-  congr 1
-  apply Array.getElem_set_ne
-  apply mt Fin.eq_of_val_eq h
+theorem get_set (a : DArray n α) (i : Fin n) (v : α i) : (a.set i v).get i = v := by
+  simp only [DArray.get, DArray.set, dif_pos]
+
+theorem get_set_ne (a : DArray n α) (v : α i) (h : i ≠ j) : (a.set i v).get j = a.get j := by
+  simp only [DArray.get, DArray.set, dif_neg h]
 
 @[simp]
 theorem set_set {type : Fin size → Type _} (a : DArray size type) (i : Fin size)
@@ -97,7 +46,6 @@ theorem set_set {type : Fin size → Type _} (a : DArray size type) (i : Fin siz
 @[simp]
 theorem get_mk (i : Fin size) : DArray.get (.mk init) i = init i := by
   simp [DArray.get, DArray.mk]
-  exact eq_of_heq <| Sigma.castIdx_heq_val ..
 
 theorem set_mk {type : Fin size → Type _} {init} (i : Fin size) (v : type i) :
     DArray.set (.mk init) i v = .mk fun j => if h : i = j then h ▸ v else init j := by
@@ -115,8 +63,8 @@ type. So it's safe, in principle, to `unsafeCast` the fake `Unit` objects to the
 and similarly to `unsafeCast` any relevant object to a fake `Unit` object.
 -/
 
-private unsafe def mkUnsafe (init : (i : Fin size) → type i) : DArray size type :=
-  let data : Array Unit := .ofFn fun i => unsafeCast (init i)
+private unsafe def mkUnsafe (get : (i : Fin size) → type i) : DArray size type :=
+  let data : Array Unit := .ofFn fun i => unsafeCast (get i)
   unsafeCast data
 
 private unsafe def getUnsafe (a : DArray size type) (i) : type i :=
@@ -127,15 +75,6 @@ private unsafe def setUnsafe (a : DArray size type) (i) (v : type i) : DArray si
   let data : Array Unit := unsafeCast a
   unsafeCast <| data.set ⟨i.val, lcProof⟩ <| unsafeCast v
 
-private unsafe def dataUnsafe (a : DArray size type) : Array (Sigma type) :=
-  .ofFn fun i => ⟨_, a.getUnsafe i⟩
-
-private unsafe def mk_Unsafe {type : Fin size → Type _} (data : Array (Sigma type))
-    (size_eq : data.size = size) (idx_eq : ∀ (i : Fin size), data[i].fst = i) : DArray size type :=
-  mkUnsafe fun i => idx_eq i ▸ data[i].snd
-
-attribute [implemented_by mk_Unsafe] DArray.mk_
 attribute [implemented_by mkUnsafe] DArray.mk
-attribute [implemented_by dataUnsafe] DArray.data
 attribute [implemented_by getUnsafe] DArray.get
 attribute [implemented_by setUnsafe] DArray.set

From a59a7269a5d9e5017dd9f54d226b376c0278ad50 Mon Sep 17 00:00:00 2001
From: "F. G. Dorais" <fgdorais@gmail.com>
Date: Mon, 27 May 2024 19:36:28 -0400
Subject: [PATCH 05/25] chore: cleanup

---
 Batteries.lean             |  1 -
 Batteries/Data/DArray.lean |  2 --
 Batteries/Data/Sigma.lean  | 29 -----------------------------
 3 files changed, 32 deletions(-)
 delete mode 100644 Batteries/Data/Sigma.lean

diff --git a/Batteries.lean b/Batteries.lean
index ebd3048cd9..c987926b24 100644
--- a/Batteries.lean
+++ b/Batteries.lean
@@ -34,7 +34,6 @@ import Batteries.Data.PairingHeap
 import Batteries.Data.RBMap
 import Batteries.Data.Range
 import Batteries.Data.Rat
-import Batteries.Data.Sigma
 import Batteries.Data.String
 import Batteries.Data.Sum
 import Batteries.Data.UInt
diff --git a/Batteries/Data/DArray.lean b/Batteries/Data/DArray.lean
index 2c42c4a1f0..881cc25324 100644
--- a/Batteries/Data/DArray.lean
+++ b/Batteries/Data/DArray.lean
@@ -4,8 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: François G. Dorais
 -/
 
-import Batteries.Data.Sigma
-
 namespace Batteries
 
 /-- `DArray` is a heterogenous array with element types given by `type`. -/
diff --git a/Batteries/Data/Sigma.lean b/Batteries/Data/Sigma.lean
deleted file mode 100644
index e55c1a008d..0000000000
--- a/Batteries/Data/Sigma.lean
+++ /dev/null
@@ -1,29 +0,0 @@
-/-
-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 Sigma
-
-/-- Type value of a `Sigma` object. -/
-protected abbrev type (a : Sigma α) : Type _ := α a.fst
-
-/-- Casts an `Sigma` object to  a value of compatible type. -/
-protected def cast : (a : Sigma α) → a.type = β → β
-  | {snd := a}, rfl => a
-
-/-- Casts an `Sigma` object to  a value of compatible index. -/
-protected def castIdx : (a : Sigma α) → a.fst = i → α i
-  | {snd := a}, rfl => a
-
-@[simp]
-theorem mk_val (a : Sigma α) : ⟨_, a.snd⟩ = a := rfl
-
-@[simp]
-theorem cast_heq_val : (a : Sigma α) → (h : a.type = β) → HEq (a.cast h) a.snd
-  | {..}, rfl => .rfl
-
-@[simp]
-theorem castIdx_heq_val : (a : Sigma α) → (h : a.fst = i) → HEq (a.castIdx h) a.snd
-  | {..}, rfl => .rfl

From 62a6444d698c1a0d967e9b993c826a3abe0d47de Mon Sep 17 00:00:00 2001
From: "F. G. Dorais" <fgdorais@gmail.com>
Date: Mon, 27 May 2024 19:49:30 -0400
Subject: [PATCH 06/25] chore: cleanup

---
 Batteries/Data/DArray.lean | 36 +++++++++++++++---------------------
 1 file changed, 15 insertions(+), 21 deletions(-)

diff --git a/Batteries/Data/DArray.lean b/Batteries/Data/DArray.lean
index 881cc25324..1c5a8bbbec 100644
--- a/Batteries/Data/DArray.lean
+++ b/Batteries/Data/DArray.lean
@@ -6,14 +6,14 @@ Authors: François G. Dorais
 
 namespace Batteries
 
-/-- `DArray` is a heterogenous array with element types given by `type`. -/
+/-- `DArray` is a heterogenous array where the type of each item depends on the index. -/
 inductive DArray (n) (α : Fin n → Type _) where
 /-- `DArray` constructor. -/
 | mk (get : (i : Fin n) → α i)
 
 namespace DArray
 
-  /-- Gets the `DArray` item at index `i`. -/
+/-- Gets the `DArray` item at index `i`. -/
 protected def get : DArray n α → (i : Fin n) → α i
   | mk get => get
 
@@ -25,6 +25,12 @@ protected def set (a : DArray n α) (i : Fin n) (v : α i) : DArray n α :=
 protected theorem ext : {a b : DArray n α} → (∀ i, a.get i = b.get i) → a = b
   | mk _, mk _, h => congrArg _ <| funext fun i => h i
 
+@[simp]
+theorem get_mk (i : Fin n) : DArray.get (.mk init) i = init i := rfl
+
+theorem set_mk {α : Fin n → Type _} {init} (i : Fin n) (v : α i) :
+    DArray.set (.mk init) i v = .mk fun j => if h : i = j then h ▸ v else init j := rfl
+
 @[simp]
 theorem get_set (a : DArray n α) (i : Fin n) (v : α i) : (a.set i v).get i = v := by
   simp only [DArray.get, DArray.set, dif_pos]
@@ -33,43 +39,31 @@ theorem get_set_ne (a : DArray n α) (v : α i) (h : i ≠ j) : (a.set i v).get
   simp only [DArray.get, DArray.set, dif_neg h]
 
 @[simp]
-theorem set_set {type : Fin size → Type _} (a : DArray size type) (i : Fin size)
-    (v w : type i) : (a.set i v).set i w = a.set i w := by
+theorem set_set {α : Fin n → Type _} (a : DArray n α) (i : Fin n)
+    (v w : α i) : (a.set i v).set i w = a.set i w := by
   ext j
   if h : i = j then
     rw [← h, get_set, get_set]
   else
     rw [get_set_ne _ _ h, get_set_ne _ _ h, get_set_ne _ _ h]
 
-@[simp]
-theorem get_mk (i : Fin size) : DArray.get (.mk init) i = init i := by
-  simp [DArray.get, DArray.mk]
-
-theorem set_mk {type : Fin size → Type _} {init} (i : Fin size) (v : type i) :
-    DArray.set (.mk init) i v = .mk fun j => if h : i = j then h ▸ v else init j := by
-  ext j
-  if h : i = j then
-    rw [← h, get_set, get_mk, dif_pos rfl]
-  else
-    rw [get_set_ne _ _ h, get_mk, get_mk, dif_neg h]
-
 /-! # Experimental Unsafe Implementation
 
-For this implementation, `DArray n α` is secretly stored as an `Array Unit` with size `n`. This
+For this implementation, `DArray n α` is secretly stored as an `Array Unit` with n `n`. This
 works because Lean never actually checks that the objects stored in an array have the appropriate
-type. So it's safe, in principle, to `unsafeCast` the fake `Unit` objects to the appropriate type
+α. So it's safe, in principle, to `unsafeCast` the fake `Unit` objects to the appropriate α
 and similarly to `unsafeCast` any relevant object to a fake `Unit` object.
 -/
 
-private unsafe def mkUnsafe (get : (i : Fin size) → type i) : DArray size type :=
+private unsafe def mkUnsafe (get : (i : Fin n) → α i) : DArray n α :=
   let data : Array Unit := .ofFn fun i => unsafeCast (get i)
   unsafeCast data
 
-private unsafe def getUnsafe (a : DArray size type) (i) : type i :=
+private unsafe def getUnsafe (a : DArray n α) (i) : α i :=
   let data : Array Unit := unsafeCast a
   unsafeCast <| data[i.val]'(lcProof)
 
-private unsafe def setUnsafe (a : DArray size type) (i) (v : type i) : DArray size type :=
+private unsafe def setUnsafe (a : DArray n α) (i) (v : α i) : DArray n α :=
   let data : Array Unit := unsafeCast a
   unsafeCast <| data.set ⟨i.val, lcProof⟩ <| unsafeCast v
 

From 90a1e93c12e76b224e8e6bfd5f891e62039f1b56 Mon Sep 17 00:00:00 2001
From: "F. G. Dorais" <fgdorais@gmail.com>
Date: Mon, 27 May 2024 19:54:21 -0400
Subject: [PATCH 07/25] chore: cleanup

---
 Batteries/Data/DArray.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Batteries/Data/DArray.lean b/Batteries/Data/DArray.lean
index 1c5a8bbbec..fcbf5e5a6e 100644
--- a/Batteries/Data/DArray.lean
+++ b/Batteries/Data/DArray.lean
@@ -28,7 +28,7 @@ protected theorem ext : {a b : DArray n α} → (∀ i, a.get i = b.get i) → a
 @[simp]
 theorem get_mk (i : Fin n) : DArray.get (.mk init) i = init i := rfl
 
-theorem set_mk {α : Fin n → Type _} {init} (i : Fin n) (v : α i) :
+theorem set_mk {α : Fin n → Type _} {init : (i : Fin n) → α i} (i : Fin n) (v : α i) :
     DArray.set (.mk init) i v = .mk fun j => if h : i = j then h ▸ v else init j := rfl
 
 @[simp]

From c2ef604cf709119f35997c5612b6370e35919d79 Mon Sep 17 00:00:00 2001
From: "F. G. Dorais" <fgdorais@gmail.com>
Date: Mon, 27 May 2024 20:02:48 -0400
Subject: [PATCH 08/25] chore: more tests

---
 test/darray.lean | 8 ++++++++
 1 file changed, 8 insertions(+)

diff --git a/test/darray.lean b/test/darray.lean
index 494aa67761..3bb0b9eaae 100644
--- a/test/darray.lean
+++ b/test/darray.lean
@@ -5,6 +5,8 @@ open Batteries
 def foo : DArray 3 fun | 0 => String | 1 => Nat | 2 => Array Nat :=
   .mk fun | 0 => "foo" | 1 => 42 | 2 => #[4, 2]
 
+def bar := foo.set 0 "bar"
+
 #guard foo.get 0 == "foo"
 #guard foo.get 1 == 42
 #guard foo.get 2 == #[4, 2]
@@ -12,3 +14,9 @@ def foo : DArray 3 fun | 0 => String | 1 => Nat | 2 => Array Nat :=
 #guard (foo.set 1 1).get 0 == "foo"
 #guard (foo.set 1 1).get 1 == 1
 #guard (foo.set 1 1).get 2 == #[4, 2]
+
+#guard bar.get 0 == "bar"
+#guard (bar.set 0 (foo.get 0)).get 0 == "foo"
+#guard ((bar.set 0 "baz").set 1 1).get 0 == "baz"
+#guard ((bar.set 0 "baz").set 0 "foo").get 0 == "foo"
+#guard ((bar.set 0 "foo").set 0 "baz").get 0 == "baz"

From e91f84c9401eafb498090394d8b4e85958222728 Mon Sep 17 00:00:00 2001
From: "F. G. Dorais" <fgdorais@gmail.com>
Date: Mon, 27 May 2024 20:09:28 -0400
Subject: [PATCH 09/25] fix: typos

---
 Batteries/Data/DArray.lean | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

diff --git a/Batteries/Data/DArray.lean b/Batteries/Data/DArray.lean
index fcbf5e5a6e..a11747115d 100644
--- a/Batteries/Data/DArray.lean
+++ b/Batteries/Data/DArray.lean
@@ -49,10 +49,10 @@ theorem set_set {α : Fin n → Type _} (a : DArray n α) (i : Fin n)
 
 /-! # Experimental Unsafe Implementation
 
-For this implementation, `DArray n α` is secretly stored as an `Array Unit` with n `n`. This
-works because Lean never actually checks that the objects stored in an array have the appropriate
-α. So it's safe, in principle, to `unsafeCast` the fake `Unit` objects to the appropriate α
-and similarly to `unsafeCast` any relevant object to a fake `Unit` object.
+For this implementation, `DArray n α` is secretly stored as an `Array Unit` with size `n`. This
+works because Lean never actually checks that objects have the appropriate type. So it's safe, in
+principle, to `unsafeCast` the fake `Unit` or `Array` objects to the appropriate type and similarly
+to `unsafeCast` any relevant object to a fake `Unit` or `Array` object.
 -/
 
 private unsafe def mkUnsafe (get : (i : Fin n) → α i) : DArray n α :=
@@ -61,7 +61,7 @@ private unsafe def mkUnsafe (get : (i : Fin n) → α i) : DArray n α :=
 
 private unsafe def getUnsafe (a : DArray n α) (i) : α i :=
   let data : Array Unit := unsafeCast a
-  unsafeCast <| data[i.val]'(lcProof)
+  unsafeCast <| data.get ⟨i.val, lcProof⟩
 
 private unsafe def setUnsafe (a : DArray n α) (i) (v : α i) : DArray n α :=
   let data : Array Unit := unsafeCast a

From 8bd44e000557cd94ac055b0e1019f25b0cdfc555 Mon Sep 17 00:00:00 2001
From: "F. G. Dorais" <fgdorais@gmail.com>
Date: Mon, 27 May 2024 21:42:57 -0400
Subject: [PATCH 10/25] feat: add `recOn` and `casesOn`

---
 Batteries/Data/DArray.lean | 6 ++++++
 test/darray.lean           | 6 ++++++
 2 files changed, 12 insertions(+)

diff --git a/Batteries/Data/DArray.lean b/Batteries/Data/DArray.lean
index a11747115d..11e1a96d4c 100644
--- a/Batteries/Data/DArray.lean
+++ b/Batteries/Data/DArray.lean
@@ -67,6 +67,12 @@ private unsafe def setUnsafe (a : DArray n α) (i) (v : α i) : DArray n α :=
   let data : Array Unit := unsafeCast a
   unsafeCast <| data.set ⟨i.val, lcProof⟩ <| unsafeCast v
 
+private unsafe def recOnUnsafe.{u} {motive : DArray n α → Sort u} (a : DArray n α)
+  (h : (get : (i : Fin n) → α i) → motive (.mk get)) : motive a :=
+  h a.get
+
 attribute [implemented_by mkUnsafe] DArray.mk
 attribute [implemented_by getUnsafe] DArray.get
 attribute [implemented_by setUnsafe] DArray.set
+attribute [implemented_by recOnUnsafe] DArray.recOn
+attribute [implemented_by recOnUnsafe] DArray.casesOn
diff --git a/test/darray.lean b/test/darray.lean
index 3bb0b9eaae..0af1a42520 100644
--- a/test/darray.lean
+++ b/test/darray.lean
@@ -20,3 +20,9 @@ def bar := foo.set 0 "bar"
 #guard ((bar.set 0 "baz").set 1 1).get 0 == "baz"
 #guard ((bar.set 0 "baz").set 0 "foo").get 0 == "foo"
 #guard ((bar.set 0 "foo").set 0 "baz").get 0 == "baz"
+
+def Batteries.DArray.head : DArray (n+1) α → α 0
+  | mk f => f 0
+
+#guard foo.head == "foo"
+#guard bar.head == "bar"

From ee049a587bd75aa2cdbb1a9bff2d155076fe7024 Mon Sep 17 00:00:00 2001
From: "F. G. Dorais" <fgdorais@gmail.com>
Date: Tue, 28 May 2024 08:07:09 -0400
Subject: [PATCH 11/25] chore: cleanup and docs

---
 Batteries/Data/DArray.lean | 102 ++++++++++++++++++++++++-------------
 1 file changed, 67 insertions(+), 35 deletions(-)

diff --git a/Batteries/Data/DArray.lean b/Batteries/Data/DArray.lean
index 11e1a96d4c..026707c212 100644
--- a/Batteries/Data/DArray.lean
+++ b/Batteries/Data/DArray.lean
@@ -6,21 +6,81 @@ Authors: François G. Dorais
 
 namespace Batteries
 
+/-!
+# Dependent Arrays
+
+`DArray` is a heterogenous array where the type of each item depends on the index. The model
+for this type is the dependent function type `(i : Fin n) → α i` where `α i` is the type assigned
+to items at index `i`.
+
+The implementation of `DArray` is based on Lean's persistent array type. This means that the array
+values are stored in a contiguous memory region and can be accessed in constant time. Lean's
+persistent arrays also support destructive updates when the array is exclusive (RC=1).
+
+### Implementation Details
+
+Lean's persistent array API does not directly support dependent arrays. Each `DArray n α` is
+internally stored as an `Array Unit` with length `n`. This is sound since Lean's persistent array
+implementation does not record nor use the type of the items stored in the array. So it is safe to
+use `UnsafeCast` to convert array items to the appropriate type when necessary.
+-/
+
 /-- `DArray` is a heterogenous array where the type of each item depends on the index. -/
 inductive DArray (n) (α : Fin n → Type _) where
-/-- `DArray` constructor. -/
-| mk (get : (i : Fin n) → α i)
+  /-- Makes a new `DArray` with given item values. -/
+  | mk (get : (i : Fin n) → α i)
 
 namespace DArray
 
-/-- Gets the `DArray` item at index `i`. -/
+section unsafe_implementation
+
+private unsafe abbrev data : DArray n α → Array Unit := unsafeCast
+
+private unsafe def mkImpl (get : (i : Fin n) → α i) : DArray n α :=
+  unsafeCast <| Array.ofFn fun i => (unsafeCast (get i) : Unit)
+
+private unsafe def getImpl (a : DArray n α) (i) : α i :=
+  unsafeCast <| a.data.get ⟨i.val, lcProof⟩
+
+private unsafe def setImpl (a : DArray n α) (i) (v : α i) : DArray n α :=
+  unsafeCast <| a.data.set ⟨i.val, lcProof⟩ <| unsafeCast v
+
+private unsafe def copyImpl (a : DArray n α) : DArray n α :=
+  unsafeCast <| a.data.extract 0 n
+
+end unsafe_implementation
+
+attribute [implemented_by mkImpl] DArray.mk
+
+/-- Gets the `DArray` item at index `i`. `O(1)`. -/
+@[implemented_by getImpl]
 protected def get : DArray n α → (i : Fin n) → α i
   | mk get => get
 
-/-- Sets the `DArray` item at index `i`. -/
+@[simp, inherit_doc DArray.get]
+protected abbrev getN (a : DArray n α) (i) (h : i < n := by get_elem_tactic) : α ⟨i, h⟩ :=
+  a.get ⟨i, h⟩
+
+private def recOnImpl.{u} {motive : DArray n α → Sort u} (a : DArray n α)
+  (h : (get : (i : Fin n) → α i) → motive (.mk get)) : motive a :=
+  h a.get
+
+attribute [implemented_by recOnImpl] DArray.recOn
+attribute [implemented_by recOnImpl] DArray.casesOn
+
+/-- Sets the `DArray` item at index `i`. `O(1)` if exclusive else `O(n)`. -/
+@[implemented_by setImpl]
 protected def set (a : DArray n α) (i : Fin n) (v : α i) : DArray n α :=
   mk fun j => if h : i = j then h ▸ v else a.get j
 
+@[simp, inherit_doc DArray.get]
+protected abbrev setN (a : DArray n α) (i) (h : i < n := by get_elem_tactic) (v : α ⟨i, h⟩) :=
+  a.set ⟨i, h⟩ v
+
+/-- Copies the `DArray` to an exclusive `DArray`. `O(1)` if exclusive else `O(n)`. -/
+@[implemented_by copyImpl]
+protected def copy (a : DArray n α) : DArray n α := mk a.get
+
 @[ext]
 protected theorem ext : {a b : DArray n α} → (∀ i, a.get i = b.get i) → a = b
   | mk _, mk _, h => congrArg _ <| funext fun i => h i
@@ -39,40 +99,12 @@ theorem get_set_ne (a : DArray n α) (v : α i) (h : i ≠ j) : (a.set i v).get
   simp only [DArray.get, DArray.set, dif_neg h]
 
 @[simp]
-theorem set_set {α : Fin n → Type _} (a : DArray n α) (i : Fin n)
-    (v w : α i) : (a.set i v).set i w = a.set i w := by
+theorem set_set (a : DArray n α) (i : Fin n) (v w : α i) : (a.set i v).set i w = a.set i w := by
   ext j
   if h : i = j then
     rw [← h, get_set, get_set]
   else
     rw [get_set_ne _ _ h, get_set_ne _ _ h, get_set_ne _ _ h]
 
-/-! # Experimental Unsafe Implementation
-
-For this implementation, `DArray n α` is secretly stored as an `Array Unit` with size `n`. This
-works because Lean never actually checks that objects have the appropriate type. So it's safe, in
-principle, to `unsafeCast` the fake `Unit` or `Array` objects to the appropriate type and similarly
-to `unsafeCast` any relevant object to a fake `Unit` or `Array` object.
--/
-
-private unsafe def mkUnsafe (get : (i : Fin n) → α i) : DArray n α :=
-  let data : Array Unit := .ofFn fun i => unsafeCast (get i)
-  unsafeCast data
-
-private unsafe def getUnsafe (a : DArray n α) (i) : α i :=
-  let data : Array Unit := unsafeCast a
-  unsafeCast <| data.get ⟨i.val, lcProof⟩
-
-private unsafe def setUnsafe (a : DArray n α) (i) (v : α i) : DArray n α :=
-  let data : Array Unit := unsafeCast a
-  unsafeCast <| data.set ⟨i.val, lcProof⟩ <| unsafeCast v
-
-private unsafe def recOnUnsafe.{u} {motive : DArray n α → Sort u} (a : DArray n α)
-  (h : (get : (i : Fin n) → α i) → motive (.mk get)) : motive a :=
-  h a.get
-
-attribute [implemented_by mkUnsafe] DArray.mk
-attribute [implemented_by getUnsafe] DArray.get
-attribute [implemented_by setUnsafe] DArray.set
-attribute [implemented_by recOnUnsafe] DArray.recOn
-attribute [implemented_by recOnUnsafe] DArray.casesOn
+@[simp]
+theorem copy_eq (a : DArray n α) : a.copy = a := rfl

From 45446e75fc00a157265c6e20b984a97a93e032ef Mon Sep 17 00:00:00 2001
From: "F. G. Dorais" <fgdorais@gmail.com>
Date: Tue, 28 May 2024 08:12:36 -0400
Subject: [PATCH 12/25] chore: time for `mk`

---
 Batteries/Data/DArray.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Batteries/Data/DArray.lean b/Batteries/Data/DArray.lean
index 026707c212..47dc8251b9 100644
--- a/Batteries/Data/DArray.lean
+++ b/Batteries/Data/DArray.lean
@@ -27,7 +27,7 @@ use `UnsafeCast` to convert array items to the appropriate type when necessary.
 
 /-- `DArray` is a heterogenous array where the type of each item depends on the index. -/
 inductive DArray (n) (α : Fin n → Type _) where
-  /-- Makes a new `DArray` with given item values. -/
+  /-- Makes a new `DArray` with given item values. `O(n*g)` where `get i` is `O(g)`. -/
   | mk (get : (i : Fin n) → α i)
 
 namespace DArray

From ddff5dfe561a49b9bbdb27b5ca714fb776916235 Mon Sep 17 00:00:00 2001
From: "F. G. Dorais" <fgdorais@gmail.com>
Date: Tue, 28 May 2024 09:28:25 -0400
Subject: [PATCH 13/25] fix: docs

---
 Batteries/Data/DArray.lean | 14 +++++++-------
 1 file changed, 7 insertions(+), 7 deletions(-)

diff --git a/Batteries/Data/DArray.lean b/Batteries/Data/DArray.lean
index 47dc8251b9..82b4a99351 100644
--- a/Batteries/Data/DArray.lean
+++ b/Batteries/Data/DArray.lean
@@ -13,16 +13,16 @@ namespace Batteries
 for this type is the dependent function type `(i : Fin n) → α i` where `α i` is the type assigned
 to items at index `i`.
 
-The implementation of `DArray` is based on Lean's persistent array type. This means that the array
-values are stored in a contiguous memory region and can be accessed in constant time. Lean's
-persistent arrays also support destructive updates when the array is exclusive (RC=1).
+The implementation of `DArray` is based on Lean's dynamic array type. This means that the array
+values are stored in a contiguous memory region and can be accessed in constant time. Lean's arrays
+also support destructive updates when the array is exclusive (RC=1).
 
 ### Implementation Details
 
-Lean's persistent array API does not directly support dependent arrays. Each `DArray n α` is
-internally stored as an `Array Unit` with length `n`. This is sound since Lean's persistent array
-implementation does not record nor use the type of the items stored in the array. So it is safe to
-use `UnsafeCast` to convert array items to the appropriate type when necessary.
+Lean's array API does not directly support dependent arrays. Each `DArray n α` is internally stored
+as an `Array Unit` with length `n`. This is sound since Lean's array implementation does not record
+nor use the type of the items stored in the array. So it is safe to use `UnsafeCast` to convert
+array items to the appropriate type when necessary.
 -/
 
 /-- `DArray` is a heterogenous array where the type of each item depends on the index. -/

From 419a4c4b653408ad5c4075c086b610590af805d6 Mon Sep 17 00:00:00 2001
From: "F. G. Dorais" <fgdorais@gmail.com>
Date: Tue, 28 May 2024 09:41:25 -0400
Subject: [PATCH 14/25] feat: add `Inhabited` instance

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

diff --git a/Batteries/Data/DArray.lean b/Batteries/Data/DArray.lean
index 82b4a99351..b007e7d335 100644
--- a/Batteries/Data/DArray.lean
+++ b/Batteries/Data/DArray.lean
@@ -52,6 +52,9 @@ end unsafe_implementation
 
 attribute [implemented_by mkImpl] DArray.mk
 
+instance (α : Fin n → Type _) [(i : Fin n) → Inhabited (α i)] : Inhabited (DArray n α) where
+  default := mk fun _ => default
+
 /-- Gets the `DArray` item at index `i`. `O(1)`. -/
 @[implemented_by getImpl]
 protected def get : DArray n α → (i : Fin n) → α i

From 88e32c9c85f181fb1fa54fe2f8f8a4d318b2b7a1 Mon Sep 17 00:00:00 2001
From: "F. G. Dorais" <fgdorais@gmail.com>
Date: Tue, 28 May 2024 09:51:01 -0400
Subject: [PATCH 15/25] chore: add todo for lean4#2292

---
 Batteries/Data/DArray.lean | 1 +
 1 file changed, 1 insertion(+)

diff --git a/Batteries/Data/DArray.lean b/Batteries/Data/DArray.lean
index b007e7d335..2f7308ea61 100644
--- a/Batteries/Data/DArray.lean
+++ b/Batteries/Data/DArray.lean
@@ -26,6 +26,7 @@ array items to the appropriate type when necessary.
 -/
 
 /-- `DArray` is a heterogenous array where the type of each item depends on the index. -/
+-- TODO: Use a structure once [lean4#2292](https://github.com/leanprover/lean4/pull/2292) is fixed.
 inductive DArray (n) (α : Fin n → Type _) where
   /-- Makes a new `DArray` with given item values. `O(n*g)` where `get i` is `O(g)`. -/
   | mk (get : (i : Fin n) → α i)

From 11d35877458fe46977248d5d205339777ff41c4a Mon Sep 17 00:00:00 2001
From: "F. G. Dorais" <fgdorais@gmail.com>
Date: Tue, 28 May 2024 10:13:06 -0400
Subject: [PATCH 16/25] fix: use `NonScalar` instead of `Unit`

---
 Batteries/Data/DArray.lean | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

diff --git a/Batteries/Data/DArray.lean b/Batteries/Data/DArray.lean
index 2f7308ea61..5e6c4e313a 100644
--- a/Batteries/Data/DArray.lean
+++ b/Batteries/Data/DArray.lean
@@ -20,9 +20,9 @@ also support destructive updates when the array is exclusive (RC=1).
 ### Implementation Details
 
 Lean's array API does not directly support dependent arrays. Each `DArray n α` is internally stored
-as an `Array Unit` with length `n`. This is sound since Lean's array implementation does not record
-nor use the type of the items stored in the array. So it is safe to use `UnsafeCast` to convert
-array items to the appropriate type when necessary.
+as an `Array NonScalar` with length `n`. This is sound since Lean's array implementation does not
+record nor use the type of the items stored in the array. So it is safe to use `UnsafeCast` to
+convert array items to the appropriate type when necessary.
 -/
 
 /-- `DArray` is a heterogenous array where the type of each item depends on the index. -/
@@ -35,10 +35,10 @@ namespace DArray
 
 section unsafe_implementation
 
-private unsafe abbrev data : DArray n α → Array Unit := unsafeCast
+private unsafe abbrev data : DArray n α → Array NonScalar := unsafeCast
 
 private unsafe def mkImpl (get : (i : Fin n) → α i) : DArray n α :=
-  unsafeCast <| Array.ofFn fun i => (unsafeCast (get i) : Unit)
+  unsafeCast <| Array.ofFn fun i => (unsafeCast (get i) : NonScalar)
 
 private unsafe def getImpl (a : DArray n α) (i) : α i :=
   unsafeCast <| a.data.get ⟨i.val, lcProof⟩

From bf511fd3554c5d793d0f06ce18ca12e72ac9b6b3 Mon Sep 17 00:00:00 2001
From: "F. G. Dorais" <fgdorais@gmail.com>
Date: Tue, 28 May 2024 10:31:59 -0400
Subject: [PATCH 17/25] feat: add `uget`

---
 Batteries/Data/DArray.lean | 12 ++++++++++++
 1 file changed, 12 insertions(+)

diff --git a/Batteries/Data/DArray.lean b/Batteries/Data/DArray.lean
index 5e6c4e313a..7e0248f827 100644
--- a/Batteries/Data/DArray.lean
+++ b/Batteries/Data/DArray.lean
@@ -43,6 +43,9 @@ private unsafe def mkImpl (get : (i : Fin n) → α i) : DArray n α :=
 private unsafe def getImpl (a : DArray n α) (i) : α i :=
   unsafeCast <| a.data.get ⟨i.val, lcProof⟩
 
+private unsafe def ugetImpl (a : DArray n α) (i : USize) (h : i.toNat < n) : α ⟨i.toNat, h⟩ :=
+  unsafeCast <| a.data.uget i lcProof
+
 private unsafe def setImpl (a : DArray n α) (i) (v : α i) : DArray n α :=
   unsafeCast <| a.data.set ⟨i.val, lcProof⟩ <| unsafeCast v
 
@@ -65,6 +68,11 @@ protected def get : DArray n α → (i : Fin n) → α i
 protected abbrev getN (a : DArray n α) (i) (h : i < n := by get_elem_tactic) : α ⟨i, h⟩ :=
   a.get ⟨i, h⟩
 
+/-- Gets the `DArray` item at index `i : USize`. Slightly faster than `get`; `O(1)`. -/
+@[implemented_by ugetImpl]
+protected def uget (a : DArray n α) (i : USize) (h : i.toNat < n) : α ⟨i.toNat, h⟩ :=
+  a.get ⟨i.toNat, h⟩
+
 private def recOnImpl.{u} {motive : DArray n α → Sort u} (a : DArray n α)
   (h : (get : (i : Fin n) → α i) → motive (.mk get)) : motive a :=
   h a.get
@@ -95,6 +103,10 @@ theorem get_mk (i : Fin n) : DArray.get (.mk init) i = init i := rfl
 theorem set_mk {α : Fin n → Type _} {init : (i : Fin n) → α i} (i : Fin n) (v : α i) :
     DArray.set (.mk init) i v = .mk fun j => if h : i = j then h ▸ v else init j := rfl
 
+@[simp]
+theorem uget_eq_get (a : DArray n α) (i : USize) (h : i.toNat < n) :
+    a.uget i h = a.get ⟨i.toNat, h⟩ := rfl
+
 @[simp]
 theorem get_set (a : DArray n α) (i : Fin n) (v : α i) : (a.set i v).get i = v := by
   simp only [DArray.get, DArray.set, dif_pos]

From f794ffad7216a2c640df7636f8e38dd966926eb9 Mon Sep 17 00:00:00 2001
From: "F. G. Dorais" <fgdorais@gmail.com>
Date: Tue, 28 May 2024 10:33:10 -0400
Subject: [PATCH 18/25] fix: remove `recOn`

---
 Batteries/Data/DArray.lean | 7 +++----
 1 file changed, 3 insertions(+), 4 deletions(-)

diff --git a/Batteries/Data/DArray.lean b/Batteries/Data/DArray.lean
index 7e0248f827..bb90a0fe2a 100644
--- a/Batteries/Data/DArray.lean
+++ b/Batteries/Data/DArray.lean
@@ -73,12 +73,11 @@ protected abbrev getN (a : DArray n α) (i) (h : i < n := by get_elem_tactic) :
 protected def uget (a : DArray n α) (i : USize) (h : i.toNat < n) : α ⟨i.toNat, h⟩ :=
   a.get ⟨i.toNat, h⟩
 
-private def recOnImpl.{u} {motive : DArray n α → Sort u} (a : DArray n α)
-  (h : (get : (i : Fin n) → α i) → motive (.mk get)) : motive a :=
+private def casesOnImpl.{u} {motive : DArray n α → Sort u} (a : DArray n α)
+    (h : (get : (i : Fin n) → α i) → motive (.mk get)) : motive a :=
   h a.get
 
-attribute [implemented_by recOnImpl] DArray.recOn
-attribute [implemented_by recOnImpl] DArray.casesOn
+attribute [implemented_by casesOnImpl] DArray.casesOn
 
 /-- Sets the `DArray` item at index `i`. `O(1)` if exclusive else `O(n)`. -/
 @[implemented_by setImpl]

From b58161172091d7154799a77f410523f28b7a1569 Mon Sep 17 00:00:00 2001
From: "F. G. Dorais" <fgdorais@gmail.com>
Date: Tue, 28 May 2024 10:34:20 -0400
Subject: [PATCH 19/25] fix: typo

---
 Batteries/Data/DArray.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Batteries/Data/DArray.lean b/Batteries/Data/DArray.lean
index bb90a0fe2a..8f0458da05 100644
--- a/Batteries/Data/DArray.lean
+++ b/Batteries/Data/DArray.lean
@@ -84,7 +84,7 @@ attribute [implemented_by casesOnImpl] DArray.casesOn
 protected def set (a : DArray n α) (i : Fin n) (v : α i) : DArray n α :=
   mk fun j => if h : i = j then h ▸ v else a.get j
 
-@[simp, inherit_doc DArray.get]
+@[simp, inherit_doc DArray.set]
 protected abbrev setN (a : DArray n α) (i) (h : i < n := by get_elem_tactic) (v : α ⟨i, h⟩) :=
   a.set ⟨i, h⟩ v
 

From 3f815fe320af9f55ee73aa1648b71417dc5a286a Mon Sep 17 00:00:00 2001
From: "F. G. Dorais" <fgdorais@gmail.com>
Date: Tue, 28 May 2024 10:41:42 -0400
Subject: [PATCH 20/25] feat: add `uset`

---
 Batteries/Data/DArray.lean | 23 +++++++++++++++++++----
 1 file changed, 19 insertions(+), 4 deletions(-)

diff --git a/Batteries/Data/DArray.lean b/Batteries/Data/DArray.lean
index 8f0458da05..09a00fe705 100644
--- a/Batteries/Data/DArray.lean
+++ b/Batteries/Data/DArray.lean
@@ -49,6 +49,9 @@ private unsafe def ugetImpl (a : DArray n α) (i : USize) (h : i.toNat < n) : α
 private unsafe def setImpl (a : DArray n α) (i) (v : α i) : DArray n α :=
   unsafeCast <| a.data.set ⟨i.val, lcProof⟩ <| unsafeCast v
 
+private unsafe def usetImpl (a : DArray n α) (i : USize) (h : i.toNat < n) (v : α ⟨i.toNat, h⟩) :
+    DArray n α := unsafeCast <| a.data.uset i (unsafeCast v) lcProof
+
 private unsafe def copyImpl (a : DArray n α) : DArray n α :=
   unsafeCast <| a.data.extract 0 n
 
@@ -84,6 +87,14 @@ attribute [implemented_by casesOnImpl] DArray.casesOn
 protected def set (a : DArray n α) (i : Fin n) (v : α i) : DArray n α :=
   mk fun j => if h : i = j then h ▸ v else a.get j
 
+/--
+Sets the `DArray` item at index `i : USize`.
+Slightly faster than `set` and `O(1)` if exclusive else `O(n)`.
+-/
+@[implemented_by usetImpl]
+protected def uset (a : DArray n α) (i : USize) (h : i.toNat < n) (v : α ⟨i.toNat, h⟩) :=
+  a.set ⟨i.toNat, h⟩ v
+
 @[simp, inherit_doc DArray.set]
 protected abbrev setN (a : DArray n α) (i) (h : i < n := by get_elem_tactic) (v : α ⟨i, h⟩) :=
   a.set ⟨i, h⟩ v
@@ -102,10 +113,6 @@ theorem get_mk (i : Fin n) : DArray.get (.mk init) i = init i := rfl
 theorem set_mk {α : Fin n → Type _} {init : (i : Fin n) → α i} (i : Fin n) (v : α i) :
     DArray.set (.mk init) i v = .mk fun j => if h : i = j then h ▸ v else init j := rfl
 
-@[simp]
-theorem uget_eq_get (a : DArray n α) (i : USize) (h : i.toNat < n) :
-    a.uget i h = a.get ⟨i.toNat, h⟩ := rfl
-
 @[simp]
 theorem get_set (a : DArray n α) (i : Fin n) (v : α i) : (a.set i v).get i = v := by
   simp only [DArray.get, DArray.set, dif_pos]
@@ -121,5 +128,13 @@ theorem set_set (a : DArray n α) (i : Fin n) (v w : α i) : (a.set i v).set i w
   else
     rw [get_set_ne _ _ h, get_set_ne _ _ h, get_set_ne _ _ h]
 
+@[simp]
+theorem uget_eq_get (a : DArray n α) (i : USize) (h : i.toNat < n) :
+    a.uget i h = a.get ⟨i.toNat, h⟩ := rfl
+
+@[simp]
+theorem uset_eq_set (a : DArray n α) (i : USize) (h : i.toNat < n) (v : α ⟨i.toNat, h⟩) :
+    a.uset i h v = a.set ⟨i.toNat, h⟩ v := rfl
+
 @[simp]
 theorem copy_eq (a : DArray n α) : a.copy = a := rfl

From 10d05301f0fb1625b444a3537389a125f9b5b2a7 Mon Sep 17 00:00:00 2001
From: "F. G. Dorais" <fgdorais@gmail.com>
Date: Tue, 28 May 2024 12:38:25 -0400
Subject: [PATCH 21/25] feat: add `modify` and `umodify`

---
 Batteries/Data/DArray.lean | 33 +++++++++++++++++++++++++++++++++
 1 file changed, 33 insertions(+)

diff --git a/Batteries/Data/DArray.lean b/Batteries/Data/DArray.lean
index 09a00fe705..065a839705 100644
--- a/Batteries/Data/DArray.lean
+++ b/Batteries/Data/DArray.lean
@@ -52,6 +52,20 @@ private unsafe def setImpl (a : DArray n α) (i) (v : α i) : DArray n α :=
 private unsafe def usetImpl (a : DArray n α) (i : USize) (h : i.toNat < n) (v : α ⟨i.toNat, h⟩) :
     DArray n α := unsafeCast <| a.data.uset i (unsafeCast v) lcProof
 
+private unsafe def modifyFImpl [Functor f] (a : DArray n α) (i : Fin n)
+    (t : α i → f (α i)) : f (DArray n α) :=
+  let v := unsafeCast <| a.data.get ⟨i.val, lcProof⟩
+  -- Make sure `v` is unshared, if possible, by replacing its array entry by `box(0)`.
+  let a := unsafeCast <| a.data.set ⟨i.val, lcProof⟩ (unsafeCast ())
+  setImpl a i <$> t v
+
+private unsafe def umodifyFImpl [Functor f] (a : DArray n α) (i : USize) (h : i.toNat < n)
+    (t : α ⟨i.toNat, h⟩ → f (α ⟨i.toNat, h⟩)) : f (DArray n α) :=
+  let v := unsafeCast <| a.data.uget i lcProof
+  -- Make sure `v` is unshared, if possible, by replacing its array entry by `box(0)`.
+  let a := unsafeCast <| a.data.uset i (unsafeCast ()) lcProof
+  usetImpl a i h <$> t v
+
 private unsafe def copyImpl (a : DArray n α) : DArray n α :=
   unsafeCast <| a.data.extract 0 n
 
@@ -99,6 +113,25 @@ protected def uset (a : DArray n α) (i : USize) (h : i.toNat < n) (v : α ⟨i.
 protected abbrev setN (a : DArray n α) (i) (h : i < n := by get_elem_tactic) (v : α ⟨i, h⟩) :=
   a.set ⟨i, h⟩ v
 
+/-- Modifies the `DArray` item at index `i` using transform `t` and the functor `f`. -/
+@[implemented_by modifyFImpl]
+protected def modifyF [Functor f] (a : DArray n α) (i : Fin n)
+    (t : α i → f (α i)) : f (DArray n α) := a.set i <$> t (a.get i)
+
+/-- Modifies the `DArray` item at index `i` using transform `t`. -/
+protected abbrev modify (a : DArray n α) (i : Fin n) (t : α i → α i) : DArray n α :=
+  a.modifyF (f:=Id) i t
+
+/-- Modifies the `DArray` item at index `i : USize` using transform `t` and the functor `f`. -/
+@[implemented_by umodifyFImpl]
+protected def umodifyF [Functor f] (a : DArray n α) (i : USize) (h : i.toNat < n)
+    (t : α ⟨i.toNat, h⟩ → f (α ⟨i.toNat, h⟩)) : f (DArray n α) := a.uset i h <$> t (a.uget i h)
+
+/-- Modifies the `DArray` item at index `i : USize` using transform `t`. -/
+protected abbrev umodify (a : DArray n α) (i : USize) (h : i.toNat < n)
+    (t : α ⟨i.toNat, h⟩ → α ⟨i.toNat, h⟩) : DArray n α :=
+  a.umodifyF (f:=Id) i h t
+
 /-- Copies the `DArray` to an exclusive `DArray`. `O(1)` if exclusive else `O(n)`. -/
 @[implemented_by copyImpl]
 protected def copy (a : DArray n α) : DArray n α := mk a.get

From c8d001ccf046e650ae455b0243bfbaa38332b770 Mon Sep 17 00:00:00 2001
From: "F. G. Dorais" <fgdorais@gmail.com>
Date: Tue, 28 May 2024 13:20:10 -0400
Subject: [PATCH 22/25] feat: add `push` and `pop`

---
 Batteries/Data/DArray.lean | 18 ++++++++++++++++++
 1 file changed, 18 insertions(+)

diff --git a/Batteries/Data/DArray.lean b/Batteries/Data/DArray.lean
index 065a839705..8b0ea9df82 100644
--- a/Batteries/Data/DArray.lean
+++ b/Batteries/Data/DArray.lean
@@ -66,6 +66,13 @@ private unsafe def umodifyFImpl [Functor f] (a : DArray n α) (i : USize) (h : i
   let a := unsafeCast <| a.data.uset i (unsafeCast ()) lcProof
   usetImpl a i h <$> t v
 
+private unsafe def pushImpl (a : DArray n α) (v : β) :
+    DArray (n+1) fun i => if h : i.val < n then α ⟨i.val, h⟩ else β :=
+  unsafeCast <| a.data.push <| unsafeCast v
+
+private unsafe def popImpl (a : DArray (n+1) α) : DArray n fun i => α i.castSucc :=
+  unsafeCast <| a.data.pop
+
 private unsafe def copyImpl (a : DArray n α) : DArray n α :=
   unsafeCast <| a.data.extract 0 n
 
@@ -136,6 +143,17 @@ protected abbrev umodify (a : DArray n α) (i : USize) (h : i.toNat < n)
 @[implemented_by copyImpl]
 protected def copy (a : DArray n α) : DArray n α := mk a.get
 
+/-- Push an element onto the end of a `DArray`. `O(1)` if exclusive else `O(n)`. -/
+@[implemented_by pushImpl]
+protected def push (a : DArray n α) (v : β) :
+    DArray (n+1) fun i => if h : i.val < n then α ⟨i.val, h⟩ else β :=
+  mk fun i => if h : i.val < n then dif_pos h ▸ a.get ⟨i.val, h⟩ else dif_neg h ▸ v
+
+/-- Delete the last item of a `DArray`. `O(1)` if exclusive else `O(n)`. -/
+@[implemented_by popImpl]
+protected def pop (a : DArray (n+1) α) : DArray n fun i => α i.castSucc :=
+  mk fun i => a.get i.castSucc
+
 @[ext]
 protected theorem ext : {a b : DArray n α} → (∀ i, a.get i = b.get i) → a = b
   | mk _, mk _, h => congrArg _ <| funext fun i => h i

From 332e74ded5dce9979b75ad0830c297009b04f1e4 Mon Sep 17 00:00:00 2001
From: "F. G. Dorais" <fgdorais@gmail.com>
Date: Tue, 28 May 2024 14:18:12 -0400
Subject: [PATCH 23/25] feat: lemmas for `modify`

---
 Batteries/Data/DArray.lean | 32 +++++++++++++++++++++++++++++++-
 1 file changed, 31 insertions(+), 1 deletion(-)

diff --git a/Batteries/Data/DArray.lean b/Batteries/Data/DArray.lean
index 8b0ea9df82..1c804aa825 100644
--- a/Batteries/Data/DArray.lean
+++ b/Batteries/Data/DArray.lean
@@ -149,7 +149,7 @@ protected def push (a : DArray n α) (v : β) :
     DArray (n+1) fun i => if h : i.val < n then α ⟨i.val, h⟩ else β :=
   mk fun i => if h : i.val < n then dif_pos h ▸ a.get ⟨i.val, h⟩ else dif_neg h ▸ v
 
-/-- Delete the last item of a `DArray`. `O(1)` if exclusive else `O(n)`. -/
+/-- Delete the last item of a `DArray`. `O(1)`. -/
 @[implemented_by popImpl]
 protected def pop (a : DArray (n+1) α) : DArray n fun i => α i.castSucc :=
   mk fun i => a.get i.castSucc
@@ -179,6 +179,28 @@ theorem set_set (a : DArray n α) (i : Fin n) (v w : α i) : (a.set i v).set i w
   else
     rw [get_set_ne _ _ h, get_set_ne _ _ h, get_set_ne _ _ h]
 
+theorem get_modifyF [Functor f] [LawfulFunctor f] (a : DArray n α) (i : Fin n) (t : α i → f (α i)) :
+    (DArray.get . i) <$> a.modifyF i t = t (a.get i) := by
+  simp [DArray.modifyF, ← comp_map]
+  conv => rhs; rw [← id_map (t (a.get i))]
+  congr; ext; simp
+
+@[simp]
+theorem get_modify (a : DArray n α) (i : Fin n) (t : α i → α i) :
+    (a.modify i t).get i = t (a.get i) := get_modifyF (f:=Id) a i t
+
+theorem get_modify_ne (a : DArray n α) (t : α i → α i) (h : i ≠ j) :
+    (a.modify i t).get j = a.get j := get_set_ne _ _ h
+
+@[simp]
+theorem set_modify (a : DArray n α) (i : Fin n) (t : α i → α i) (v : α i) :
+    (a.set i v).modify i t = a.set i (t v) := by
+  ext j
+  if h : i = j then
+    cases h; simp
+  else
+    simp [h, get_modify_ne, get_set_ne]
+
 @[simp]
 theorem uget_eq_get (a : DArray n α) (i : USize) (h : i.toNat < n) :
     a.uget i h = a.get ⟨i.toNat, h⟩ := rfl
@@ -187,5 +209,13 @@ theorem uget_eq_get (a : DArray n α) (i : USize) (h : i.toNat < n) :
 theorem uset_eq_set (a : DArray n α) (i : USize) (h : i.toNat < n) (v : α ⟨i.toNat, h⟩) :
     a.uset i h v = a.set ⟨i.toNat, h⟩ v := rfl
 
+@[simp]
+theorem umodifyF_eq_modifyF [Functor f] (a : DArray n α) (i : USize) (h : i.toNat < n)
+    (t : α ⟨i.toNat, h⟩ → f (α ⟨i.toNat, h⟩)) : a.umodifyF i h t = a.modifyF ⟨i.toNat, h⟩ t := rfl
+
+@[simp]
+theorem umodify_eq_modify (a : DArray n α) (i : USize) (h : i.toNat < n)
+    (t : α ⟨i.toNat, h⟩ → α ⟨i.toNat, h⟩) : a.umodify i h t = a.modify ⟨i.toNat, h⟩ t := rfl
+
 @[simp]
 theorem copy_eq (a : DArray n α) : a.copy = a := rfl

From c665f52a04ab49d7758da8edd2723e2feb367858 Mon Sep 17 00:00:00 2001
From: "F. G. Dorais" <fgdorais@gmail.com>
Date: Tue, 28 May 2024 14:30:56 -0400
Subject: [PATCH 24/25] fix: make `modify` and `umodify` semireducible

---
 Batteries/Data/DArray.lean | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

diff --git a/Batteries/Data/DArray.lean b/Batteries/Data/DArray.lean
index 1c804aa825..3938e29054 100644
--- a/Batteries/Data/DArray.lean
+++ b/Batteries/Data/DArray.lean
@@ -126,7 +126,8 @@ protected def modifyF [Functor f] (a : DArray n α) (i : Fin n)
     (t : α i → f (α i)) : f (DArray n α) := a.set i <$> t (a.get i)
 
 /-- Modifies the `DArray` item at index `i` using transform `t`. -/
-protected abbrev modify (a : DArray n α) (i : Fin n) (t : α i → α i) : DArray n α :=
+@[inline]
+protected def modify (a : DArray n α) (i : Fin n) (t : α i → α i) : DArray n α :=
   a.modifyF (f:=Id) i t
 
 /-- Modifies the `DArray` item at index `i : USize` using transform `t` and the functor `f`. -/
@@ -135,7 +136,8 @@ protected def umodifyF [Functor f] (a : DArray n α) (i : USize) (h : i.toNat <
     (t : α ⟨i.toNat, h⟩ → f (α ⟨i.toNat, h⟩)) : f (DArray n α) := a.uset i h <$> t (a.uget i h)
 
 /-- Modifies the `DArray` item at index `i : USize` using transform `t`. -/
-protected abbrev umodify (a : DArray n α) (i : USize) (h : i.toNat < n)
+@[inline]
+protected def umodify (a : DArray n α) (i : USize) (h : i.toNat < n)
     (t : α ⟨i.toNat, h⟩ → α ⟨i.toNat, h⟩) : DArray n α :=
   a.umodifyF (f:=Id) i h t
 

From f25aaa885ae144ebeca10235c641eb47db383383 Mon Sep 17 00:00:00 2001
From: "F. G. Dorais" <fgdorais@gmail.com>
Date: Tue, 28 May 2024 16:07:38 -0400
Subject: [PATCH 25/25] chore: split Basic and Lemmas

---
 Batteries/Data/DArray.lean        | 225 +-----------------------------
 Batteries/Data/DArray/Basic.lean  | 157 +++++++++++++++++++++
 Batteries/Data/DArray/Lemmas.lean |  75 ++++++++++
 3 files changed, 234 insertions(+), 223 deletions(-)
 create mode 100644 Batteries/Data/DArray/Basic.lean
 create mode 100644 Batteries/Data/DArray/Lemmas.lean

diff --git a/Batteries/Data/DArray.lean b/Batteries/Data/DArray.lean
index 3938e29054..65bab05079 100644
--- a/Batteries/Data/DArray.lean
+++ b/Batteries/Data/DArray.lean
@@ -1,223 +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
--/
-
-namespace Batteries
-
-/-!
-# Dependent Arrays
-
-`DArray` is a heterogenous array where the type of each item depends on the index. The model
-for this type is the dependent function type `(i : Fin n) → α i` where `α i` is the type assigned
-to items at index `i`.
-
-The implementation of `DArray` is based on Lean's dynamic array type. This means that the array
-values are stored in a contiguous memory region and can be accessed in constant time. Lean's arrays
-also support destructive updates when the array is exclusive (RC=1).
-
-### Implementation Details
-
-Lean's array API does not directly support dependent arrays. Each `DArray n α` is internally stored
-as an `Array NonScalar` with length `n`. This is sound since Lean's array implementation does not
-record nor use the type of the items stored in the array. So it is safe to use `UnsafeCast` to
-convert array items to the appropriate type when necessary.
--/
-
-/-- `DArray` is a heterogenous array where the type of each item depends on the index. -/
--- TODO: Use a structure once [lean4#2292](https://github.com/leanprover/lean4/pull/2292) is fixed.
-inductive DArray (n) (α : Fin n → Type _) where
-  /-- Makes a new `DArray` with given item values. `O(n*g)` where `get i` is `O(g)`. -/
-  | mk (get : (i : Fin n) → α i)
-
-namespace DArray
-
-section unsafe_implementation
-
-private unsafe abbrev data : DArray n α → Array NonScalar := unsafeCast
-
-private unsafe def mkImpl (get : (i : Fin n) → α i) : DArray n α :=
-  unsafeCast <| Array.ofFn fun i => (unsafeCast (get i) : NonScalar)
-
-private unsafe def getImpl (a : DArray n α) (i) : α i :=
-  unsafeCast <| a.data.get ⟨i.val, lcProof⟩
-
-private unsafe def ugetImpl (a : DArray n α) (i : USize) (h : i.toNat < n) : α ⟨i.toNat, h⟩ :=
-  unsafeCast <| a.data.uget i lcProof
-
-private unsafe def setImpl (a : DArray n α) (i) (v : α i) : DArray n α :=
-  unsafeCast <| a.data.set ⟨i.val, lcProof⟩ <| unsafeCast v
-
-private unsafe def usetImpl (a : DArray n α) (i : USize) (h : i.toNat < n) (v : α ⟨i.toNat, h⟩) :
-    DArray n α := unsafeCast <| a.data.uset i (unsafeCast v) lcProof
-
-private unsafe def modifyFImpl [Functor f] (a : DArray n α) (i : Fin n)
-    (t : α i → f (α i)) : f (DArray n α) :=
-  let v := unsafeCast <| a.data.get ⟨i.val, lcProof⟩
-  -- Make sure `v` is unshared, if possible, by replacing its array entry by `box(0)`.
-  let a := unsafeCast <| a.data.set ⟨i.val, lcProof⟩ (unsafeCast ())
-  setImpl a i <$> t v
-
-private unsafe def umodifyFImpl [Functor f] (a : DArray n α) (i : USize) (h : i.toNat < n)
-    (t : α ⟨i.toNat, h⟩ → f (α ⟨i.toNat, h⟩)) : f (DArray n α) :=
-  let v := unsafeCast <| a.data.uget i lcProof
-  -- Make sure `v` is unshared, if possible, by replacing its array entry by `box(0)`.
-  let a := unsafeCast <| a.data.uset i (unsafeCast ()) lcProof
-  usetImpl a i h <$> t v
-
-private unsafe def pushImpl (a : DArray n α) (v : β) :
-    DArray (n+1) fun i => if h : i.val < n then α ⟨i.val, h⟩ else β :=
-  unsafeCast <| a.data.push <| unsafeCast v
-
-private unsafe def popImpl (a : DArray (n+1) α) : DArray n fun i => α i.castSucc :=
-  unsafeCast <| a.data.pop
-
-private unsafe def copyImpl (a : DArray n α) : DArray n α :=
-  unsafeCast <| a.data.extract 0 n
-
-end unsafe_implementation
-
-attribute [implemented_by mkImpl] DArray.mk
-
-instance (α : Fin n → Type _) [(i : Fin n) → Inhabited (α i)] : Inhabited (DArray n α) where
-  default := mk fun _ => default
-
-/-- Gets the `DArray` item at index `i`. `O(1)`. -/
-@[implemented_by getImpl]
-protected def get : DArray n α → (i : Fin n) → α i
-  | mk get => get
-
-@[simp, inherit_doc DArray.get]
-protected abbrev getN (a : DArray n α) (i) (h : i < n := by get_elem_tactic) : α ⟨i, h⟩ :=
-  a.get ⟨i, h⟩
-
-/-- Gets the `DArray` item at index `i : USize`. Slightly faster than `get`; `O(1)`. -/
-@[implemented_by ugetImpl]
-protected def uget (a : DArray n α) (i : USize) (h : i.toNat < n) : α ⟨i.toNat, h⟩ :=
-  a.get ⟨i.toNat, h⟩
-
-private def casesOnImpl.{u} {motive : DArray n α → Sort u} (a : DArray n α)
-    (h : (get : (i : Fin n) → α i) → motive (.mk get)) : motive a :=
-  h a.get
-
-attribute [implemented_by casesOnImpl] DArray.casesOn
-
-/-- Sets the `DArray` item at index `i`. `O(1)` if exclusive else `O(n)`. -/
-@[implemented_by setImpl]
-protected def set (a : DArray n α) (i : Fin n) (v : α i) : DArray n α :=
-  mk fun j => if h : i = j then h ▸ v else a.get j
-
-/--
-Sets the `DArray` item at index `i : USize`.
-Slightly faster than `set` and `O(1)` if exclusive else `O(n)`.
--/
-@[implemented_by usetImpl]
-protected def uset (a : DArray n α) (i : USize) (h : i.toNat < n) (v : α ⟨i.toNat, h⟩) :=
-  a.set ⟨i.toNat, h⟩ v
-
-@[simp, inherit_doc DArray.set]
-protected abbrev setN (a : DArray n α) (i) (h : i < n := by get_elem_tactic) (v : α ⟨i, h⟩) :=
-  a.set ⟨i, h⟩ v
-
-/-- Modifies the `DArray` item at index `i` using transform `t` and the functor `f`. -/
-@[implemented_by modifyFImpl]
-protected def modifyF [Functor f] (a : DArray n α) (i : Fin n)
-    (t : α i → f (α i)) : f (DArray n α) := a.set i <$> t (a.get i)
-
-/-- Modifies the `DArray` item at index `i` using transform `t`. -/
-@[inline]
-protected def modify (a : DArray n α) (i : Fin n) (t : α i → α i) : DArray n α :=
-  a.modifyF (f:=Id) i t
-
-/-- Modifies the `DArray` item at index `i : USize` using transform `t` and the functor `f`. -/
-@[implemented_by umodifyFImpl]
-protected def umodifyF [Functor f] (a : DArray n α) (i : USize) (h : i.toNat < n)
-    (t : α ⟨i.toNat, h⟩ → f (α ⟨i.toNat, h⟩)) : f (DArray n α) := a.uset i h <$> t (a.uget i h)
-
-/-- Modifies the `DArray` item at index `i : USize` using transform `t`. -/
-@[inline]
-protected def umodify (a : DArray n α) (i : USize) (h : i.toNat < n)
-    (t : α ⟨i.toNat, h⟩ → α ⟨i.toNat, h⟩) : DArray n α :=
-  a.umodifyF (f:=Id) i h t
-
-/-- Copies the `DArray` to an exclusive `DArray`. `O(1)` if exclusive else `O(n)`. -/
-@[implemented_by copyImpl]
-protected def copy (a : DArray n α) : DArray n α := mk a.get
-
-/-- Push an element onto the end of a `DArray`. `O(1)` if exclusive else `O(n)`. -/
-@[implemented_by pushImpl]
-protected def push (a : DArray n α) (v : β) :
-    DArray (n+1) fun i => if h : i.val < n then α ⟨i.val, h⟩ else β :=
-  mk fun i => if h : i.val < n then dif_pos h ▸ a.get ⟨i.val, h⟩ else dif_neg h ▸ v
-
-/-- Delete the last item of a `DArray`. `O(1)`. -/
-@[implemented_by popImpl]
-protected def pop (a : DArray (n+1) α) : DArray n fun i => α i.castSucc :=
-  mk fun i => a.get i.castSucc
-
-@[ext]
-protected theorem ext : {a b : DArray n α} → (∀ i, a.get i = b.get i) → a = b
-  | mk _, mk _, h => congrArg _ <| funext fun i => h i
-
-@[simp]
-theorem get_mk (i : Fin n) : DArray.get (.mk init) i = init i := rfl
-
-theorem set_mk {α : Fin n → Type _} {init : (i : Fin n) → α i} (i : Fin n) (v : α i) :
-    DArray.set (.mk init) i v = .mk fun j => if h : i = j then h ▸ v else init j := rfl
-
-@[simp]
-theorem get_set (a : DArray n α) (i : Fin n) (v : α i) : (a.set i v).get i = v := by
-  simp only [DArray.get, DArray.set, dif_pos]
-
-theorem get_set_ne (a : DArray n α) (v : α i) (h : i ≠ j) : (a.set i v).get j = a.get j := by
-  simp only [DArray.get, DArray.set, dif_neg h]
-
-@[simp]
-theorem set_set (a : DArray n α) (i : Fin n) (v w : α i) : (a.set i v).set i w = a.set i w := by
-  ext j
-  if h : i = j then
-    rw [← h, get_set, get_set]
-  else
-    rw [get_set_ne _ _ h, get_set_ne _ _ h, get_set_ne _ _ h]
-
-theorem get_modifyF [Functor f] [LawfulFunctor f] (a : DArray n α) (i : Fin n) (t : α i → f (α i)) :
-    (DArray.get . i) <$> a.modifyF i t = t (a.get i) := by
-  simp [DArray.modifyF, ← comp_map]
-  conv => rhs; rw [← id_map (t (a.get i))]
-  congr; ext; simp
-
-@[simp]
-theorem get_modify (a : DArray n α) (i : Fin n) (t : α i → α i) :
-    (a.modify i t).get i = t (a.get i) := get_modifyF (f:=Id) a i t
-
-theorem get_modify_ne (a : DArray n α) (t : α i → α i) (h : i ≠ j) :
-    (a.modify i t).get j = a.get j := get_set_ne _ _ h
-
-@[simp]
-theorem set_modify (a : DArray n α) (i : Fin n) (t : α i → α i) (v : α i) :
-    (a.set i v).modify i t = a.set i (t v) := by
-  ext j
-  if h : i = j then
-    cases h; simp
-  else
-    simp [h, get_modify_ne, get_set_ne]
-
-@[simp]
-theorem uget_eq_get (a : DArray n α) (i : USize) (h : i.toNat < n) :
-    a.uget i h = a.get ⟨i.toNat, h⟩ := rfl
-
-@[simp]
-theorem uset_eq_set (a : DArray n α) (i : USize) (h : i.toNat < n) (v : α ⟨i.toNat, h⟩) :
-    a.uset i h v = a.set ⟨i.toNat, h⟩ v := rfl
-
-@[simp]
-theorem umodifyF_eq_modifyF [Functor f] (a : DArray n α) (i : USize) (h : i.toNat < n)
-    (t : α ⟨i.toNat, h⟩ → f (α ⟨i.toNat, h⟩)) : a.umodifyF i h t = a.modifyF ⟨i.toNat, h⟩ t := rfl
-
-@[simp]
-theorem umodify_eq_modify (a : DArray n α) (i : USize) (h : i.toNat < n)
-    (t : α ⟨i.toNat, h⟩ → α ⟨i.toNat, h⟩) : a.umodify i h t = a.modify ⟨i.toNat, h⟩ t := rfl
-
-@[simp]
-theorem copy_eq (a : DArray n α) : a.copy = a := rfl
+import Batteries.Data.DArray.Basic
+import Batteries.Data.DArray.Lemmas
diff --git a/Batteries/Data/DArray/Basic.lean b/Batteries/Data/DArray/Basic.lean
new file mode 100644
index 0000000000..bf21a7958c
--- /dev/null
+++ b/Batteries/Data/DArray/Basic.lean
@@ -0,0 +1,157 @@
+/-
+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 Batteries
+
+/-!
+# Dependent Arrays
+
+`DArray` is a heterogenous array where the type of each item depends on the index. The model
+for this type is the dependent function type `(i : Fin n) → α i` where `α i` is the type assigned
+to items at index `i`.
+
+The implementation of `DArray` is based on Lean's dynamic array type. This means that the array
+values are stored in a contiguous memory region and can be accessed in constant time. Lean's arrays
+also support destructive updates when the array is exclusive (RC=1).
+
+### Implementation Details
+
+Lean's array API does not directly support dependent arrays. Each `DArray n α` is internally stored
+as an `Array NonScalar` with length `n`. This is sound since Lean's array implementation does not
+record nor use the type of the items stored in the array. So it is safe to use `UnsafeCast` to
+convert array items to the appropriate type when necessary.
+-/
+
+/-- `DArray` is a heterogenous array where the type of each item depends on the index. -/
+-- TODO: Use a structure once [lean4#2292](https://github.com/leanprover/lean4/pull/2292) is fixed.
+inductive DArray (n) (α : Fin n → Type _) where
+  /-- Makes a new `DArray` with given item values. `O(n*g)` where `get i` is `O(g)`. -/
+  | mk (get : (i : Fin n) → α i)
+
+namespace DArray
+
+section unsafe_implementation
+
+private unsafe abbrev data : DArray n α → Array NonScalar := unsafeCast
+
+private unsafe def mkImpl (get : (i : Fin n) → α i) : DArray n α :=
+  unsafeCast <| Array.ofFn fun i => (unsafeCast (get i) : NonScalar)
+
+private unsafe def getImpl (a : DArray n α) (i) : α i :=
+  unsafeCast <| a.data.get ⟨i.val, lcProof⟩
+
+private unsafe def ugetImpl (a : DArray n α) (i : USize) (h : i.toNat < n) : α ⟨i.toNat, h⟩ :=
+  unsafeCast <| a.data.uget i lcProof
+
+private unsafe def setImpl (a : DArray n α) (i) (v : α i) : DArray n α :=
+  unsafeCast <| a.data.set ⟨i.val, lcProof⟩ <| unsafeCast v
+
+private unsafe def usetImpl (a : DArray n α) (i : USize) (h : i.toNat < n) (v : α ⟨i.toNat, h⟩) :
+    DArray n α := unsafeCast <| a.data.uset i (unsafeCast v) lcProof
+
+private unsafe def modifyFImpl [Functor f] (a : DArray n α) (i : Fin n)
+    (t : α i → f (α i)) : f (DArray n α) :=
+  let v := unsafeCast <| a.data.get ⟨i.val, lcProof⟩
+  -- Make sure `v` is unshared, if possible, by replacing its array entry by `box(0)`.
+  let a := unsafeCast <| a.data.set ⟨i.val, lcProof⟩ (unsafeCast ())
+  setImpl a i <$> t v
+
+private unsafe def umodifyFImpl [Functor f] (a : DArray n α) (i : USize) (h : i.toNat < n)
+    (t : α ⟨i.toNat, h⟩ → f (α ⟨i.toNat, h⟩)) : f (DArray n α) :=
+  let v := unsafeCast <| a.data.uget i lcProof
+  -- Make sure `v` is unshared, if possible, by replacing its array entry by `box(0)`.
+  let a := unsafeCast <| a.data.uset i (unsafeCast ()) lcProof
+  usetImpl a i h <$> t v
+
+private unsafe def pushImpl (a : DArray n α) (v : β) :
+    DArray (n+1) fun i => if h : i.val < n then α ⟨i.val, h⟩ else β :=
+  unsafeCast <| a.data.push <| unsafeCast v
+
+private unsafe def popImpl (a : DArray (n+1) α) : DArray n fun i => α i.castSucc :=
+  unsafeCast <| a.data.pop
+
+private unsafe def copyImpl (a : DArray n α) : DArray n α :=
+  unsafeCast <| a.data.extract 0 n
+
+end unsafe_implementation
+
+attribute [implemented_by mkImpl] DArray.mk
+
+instance (α : Fin n → Type _) [(i : Fin n) → Inhabited (α i)] : Inhabited (DArray n α) where
+  default := mk fun _ => default
+
+/-- Gets the `DArray` item at index `i`. `O(1)`. -/
+@[implemented_by getImpl]
+protected def get : DArray n α → (i : Fin n) → α i
+  | mk get => get
+
+@[simp, inherit_doc DArray.get]
+protected abbrev getN (a : DArray n α) (i) (h : i < n := by get_elem_tactic) : α ⟨i, h⟩ :=
+  a.get ⟨i, h⟩
+
+/-- Gets the `DArray` item at index `i : USize`. Slightly faster than `get`; `O(1)`. -/
+@[implemented_by ugetImpl]
+protected def uget (a : DArray n α) (i : USize) (h : i.toNat < n) : α ⟨i.toNat, h⟩ :=
+  a.get ⟨i.toNat, h⟩
+
+private def casesOnImpl.{u} {motive : DArray n α → Sort u} (a : DArray n α)
+    (h : (get : (i : Fin n) → α i) → motive (.mk get)) : motive a :=
+  h a.get
+
+attribute [implemented_by casesOnImpl] DArray.casesOn
+
+/-- Sets the `DArray` item at index `i`. `O(1)` if exclusive else `O(n)`. -/
+@[implemented_by setImpl]
+protected def set (a : DArray n α) (i : Fin n) (v : α i) : DArray n α :=
+  mk fun j => if h : i = j then h ▸ v else a.get j
+
+/--
+Sets the `DArray` item at index `i : USize`.
+Slightly faster than `set` and `O(1)` if exclusive else `O(n)`.
+-/
+@[implemented_by usetImpl]
+protected def uset (a : DArray n α) (i : USize) (h : i.toNat < n) (v : α ⟨i.toNat, h⟩) :=
+  a.set ⟨i.toNat, h⟩ v
+
+@[simp, inherit_doc DArray.set]
+protected abbrev setN (a : DArray n α) (i) (h : i < n := by get_elem_tactic) (v : α ⟨i, h⟩) :=
+  a.set ⟨i, h⟩ v
+
+/-- Modifies the `DArray` item at index `i` using transform `t` and the functor `f`. -/
+@[implemented_by modifyFImpl]
+protected def modifyF [Functor f] (a : DArray n α) (i : Fin n)
+    (t : α i → f (α i)) : f (DArray n α) := a.set i <$> t (a.get i)
+
+/-- Modifies the `DArray` item at index `i` using transform `t`. -/
+@[inline]
+protected def modify (a : DArray n α) (i : Fin n) (t : α i → α i) : DArray n α :=
+  a.modifyF (f:=Id) i t
+
+/-- Modifies the `DArray` item at index `i : USize` using transform `t` and the functor `f`. -/
+@[implemented_by umodifyFImpl]
+protected def umodifyF [Functor f] (a : DArray n α) (i : USize) (h : i.toNat < n)
+    (t : α ⟨i.toNat, h⟩ → f (α ⟨i.toNat, h⟩)) : f (DArray n α) := a.uset i h <$> t (a.uget i h)
+
+/-- Modifies the `DArray` item at index `i : USize` using transform `t`. -/
+@[inline]
+protected def umodify (a : DArray n α) (i : USize) (h : i.toNat < n)
+    (t : α ⟨i.toNat, h⟩ → α ⟨i.toNat, h⟩) : DArray n α :=
+  a.umodifyF (f:=Id) i h t
+
+/-- Copies the `DArray` to an exclusive `DArray`. `O(1)` if exclusive else `O(n)`. -/
+@[implemented_by copyImpl]
+protected def copy (a : DArray n α) : DArray n α := mk a.get
+
+/-- Push an element onto the end of a `DArray`. `O(1)` if exclusive else `O(n)`. -/
+@[implemented_by pushImpl]
+protected def push (a : DArray n α) (v : β) :
+    DArray (n+1) fun i => if h : i.val < n then α ⟨i.val, h⟩ else β :=
+  mk fun i => if h : i.val < n then dif_pos h ▸ a.get ⟨i.val, h⟩ else dif_neg h ▸ v
+
+/-- Delete the last item of a `DArray`. `O(1)`. -/
+@[implemented_by popImpl]
+protected def pop (a : DArray (n+1) α) : DArray n fun i => α i.castSucc :=
+  mk fun i => a.get i.castSucc
diff --git a/Batteries/Data/DArray/Lemmas.lean b/Batteries/Data/DArray/Lemmas.lean
new file mode 100644
index 0000000000..bea7603e67
--- /dev/null
+++ b/Batteries/Data/DArray/Lemmas.lean
@@ -0,0 +1,75 @@
+/-
+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.DArray.Basic
+
+namespace Batteries.DArray
+
+@[ext]
+protected theorem ext : {a b : DArray n α} → (∀ i, a.get i = b.get i) → a = b
+  | mk _, mk _, h => congrArg _ <| funext fun i => h i
+
+@[simp]
+theorem get_mk (i : Fin n) : DArray.get (.mk init) i = init i := rfl
+
+theorem set_mk {α : Fin n → Type _} {init : (i : Fin n) → α i} (i : Fin n) (v : α i) :
+    DArray.set (.mk init) i v = .mk fun j => if h : i = j then h ▸ v else init j := rfl
+
+@[simp]
+theorem get_set (a : DArray n α) (i : Fin n) (v : α i) : (a.set i v).get i = v := by
+  simp only [DArray.get, DArray.set, dif_pos]
+
+theorem get_set_ne (a : DArray n α) (v : α i) (h : i ≠ j) : (a.set i v).get j = a.get j := by
+  simp only [DArray.get, DArray.set, dif_neg h]
+
+@[simp]
+theorem set_set (a : DArray n α) (i : Fin n) (v w : α i) : (a.set i v).set i w = a.set i w := by
+  ext j
+  if h : i = j then
+    rw [← h, get_set, get_set]
+  else
+    rw [get_set_ne _ _ h, get_set_ne _ _ h, get_set_ne _ _ h]
+
+theorem get_modifyF [Functor f] [LawfulFunctor f] (a : DArray n α) (i : Fin n) (t : α i → f (α i)) :
+    (DArray.get . i) <$> a.modifyF i t = t (a.get i) := by
+  simp [DArray.modifyF, ← comp_map]
+  conv => rhs; rw [← id_map (t (a.get i))]
+  congr; ext; simp
+
+@[simp]
+theorem get_modify (a : DArray n α) (i : Fin n) (t : α i → α i) :
+    (a.modify i t).get i = t (a.get i) := get_modifyF (f:=Id) a i t
+
+theorem get_modify_ne (a : DArray n α) (t : α i → α i) (h : i ≠ j) :
+    (a.modify i t).get j = a.get j := get_set_ne _ _ h
+
+@[simp]
+theorem set_modify (a : DArray n α) (i : Fin n) (t : α i → α i) (v : α i) :
+    (a.set i v).modify i t = a.set i (t v) := by
+  ext j
+  if h : i = j then
+    cases h; simp
+  else
+    simp [h, get_modify_ne, get_set_ne]
+
+@[simp]
+theorem uget_eq_get (a : DArray n α) (i : USize) (h : i.toNat < n) :
+    a.uget i h = a.get ⟨i.toNat, h⟩ := rfl
+
+@[simp]
+theorem uset_eq_set (a : DArray n α) (i : USize) (h : i.toNat < n) (v : α ⟨i.toNat, h⟩) :
+    a.uset i h v = a.set ⟨i.toNat, h⟩ v := rfl
+
+@[simp]
+theorem umodifyF_eq_modifyF [Functor f] (a : DArray n α) (i : USize) (h : i.toNat < n)
+    (t : α ⟨i.toNat, h⟩ → f (α ⟨i.toNat, h⟩)) : a.umodifyF i h t = a.modifyF ⟨i.toNat, h⟩ t := rfl
+
+@[simp]
+theorem umodify_eq_modify (a : DArray n α) (i : USize) (h : i.toNat < n)
+    (t : α ⟨i.toNat, h⟩ → α ⟨i.toNat, h⟩) : a.umodify i h t = a.modify ⟨i.toNat, h⟩ t := rfl
+
+@[simp]
+theorem copy_eq (a : DArray n α) : a.copy = a := rfl