feat: rename Array.data to Array.toList (#5288)

Also renames the current `Array.toList` to `Array.toListImpl`. (This
function should barely be used.)

See previous discussion on
[zulip](https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Understanding.20the.20docstring.20for.20docs.23Array.2Edata).
(I had managed to miss that discussion, thanks @nomeata for pointing it
out. Happily what I've done here mostly agrees with the consensus
there!)

src/Init/Data/Array/Attach.lean

@@ -20,7 +20,7 @@ Unsafe implementation of `attachWith`, taking advantage of the fact that the rep
   with the same elements but in the type `{x // P x}`. -/
 @[implemented_by attachWithImpl] def attachWith
     (xs : Array α) (P : α → Prop) (H : ∀ x ∈ xs, P x) : Array {x // P x} :=
-  ⟨xs.data.attachWith P fun x h => H x (Array.Mem.mk h)⟩
+  ⟨xs.toList.attachWith P fun x h => H x (Array.Mem.mk h)⟩
 
 /-- `O(1)`. "Attach" the proof that the elements of `xs` are in `xs` to produce a new array
   with the same elements but in the type `{x // x ∈ xs}`. -/

src/Init/Data/Array/Basic.lean

@@ -16,10 +16,11 @@ universe u v w
 namespace Array
 variable {α : Type u}
 
+@[deprecated Array.toList (since := "2024-09-10")] abbrev Array.data := @Array.toList
+
 @[extern "lean_mk_array"]
-def mkArray {α : Type u} (n : Nat) (v : α) : Array α := {
-  data := List.replicate n v
-}
+def mkArray {α : Type u} (n : Nat) (v : α) : Array α where
+  toList := List.replicate n v
 
 /--
 `ofFn f` with `f : Fin n → α` returns the list whose ith element is `f i`.
@@ -134,9 +135,8 @@ def swapAt! (a : Array α) (i : Nat) (v : α) : α × Array α :=
     panic! ("index " ++ toString i ++ " out of bounds")
 
 @[extern "lean_array_pop"]
-def pop (a : Array α) : Array α := {
-  data := a.data.dropLast
-}
+def pop (a : Array α) : Array α where
+  toList := a.toList.dropLast
 
 def shrink (a : Array α) (n : Nat) : Array α :=
   let rec loop
@@ -499,10 +499,10 @@ def elem [BEq α] (a : α) (as : Array α) : Bool :=
       (true, r)
 
 /-- Convert a `Array α` into an `List α`. This is O(n) in the size of the array.  -/
--- This function is exported to C, where it is called by `Array.data`
+-- This function is exported to C, where it is called by `Array.toList`
 -- (the projection) to implement this functionality.
-@[export lean_array_to_list]
-def toList (as : Array α) : List α :=
+@[export lean_array_to_list_impl]
+def toListImpl (as : Array α) : List α :=
   as.foldr List.cons []
 
 /-- Prepends an `Array α` onto the front of a list.  Equivalent to `as.toList ++ l`. -/
@@ -793,30 +793,32 @@ def toListLitAux (a : Array α) (n : Nat) (hsz : a.size = n) : ∀ (i : Nat), i
 def toArrayLit (a : Array α) (n : Nat) (hsz : a.size = n) : Array α :=
   List.toArray <| toListLitAux a n hsz n (hsz ▸ Nat.le_refl _) []
 
-theorem ext' {as bs : Array α} (h : as.data = bs.data) : as = bs := by
+theorem ext' {as bs : Array α} (h : as.toList = bs.toList) : as = bs := by
   cases as; cases bs; simp at h; rw [h]
 
-@[simp] theorem toArrayAux_eq (as : List α) (acc : Array α) : (as.toArrayAux acc).data = acc.data ++ as := by
+@[simp] theorem toArrayAux_eq (as : List α) (acc : Array α) : (as.toArrayAux acc).toList = acc.toList ++ as := by
   induction as generalizing acc <;> simp [*, List.toArrayAux, Array.push, List.append_assoc, List.concat_eq_append]
 
-@[simp] theorem data_toArray (as : List α) : as.toArray.data = as := by
+@[simp] theorem toList_toArray (as : List α) : as.toArray.toList = as := by
   simp [List.toArray, Array.mkEmpty]
 
+@[deprecated toList_toArray (since := "2024-09-09")] abbrev data_toArray := @toList_toArray
+
 @[simp] theorem size_toArray (as : List α) : as.toArray.size = as.length := by simp [size]
 
 theorem toArrayLit_eq (as : Array α) (n : Nat) (hsz : as.size = n) : as = toArrayLit as n hsz := by
   apply ext'
-  simp [toArrayLit, data_toArray]
+  simp [toArrayLit, toList_toArray]
   have hle : n ≤ as.size := hsz ▸ Nat.le_refl _
   have hge : as.size ≤ n := hsz ▸ Nat.le_refl _
   have := go n hle
   rw [List.drop_eq_nil_of_le hge] at this
   rw [this]
 where
-  getLit_eq (as : Array α) (i : Nat) (h₁ : as.size = n) (h₂ : i < n) : as.getLit i h₁ h₂ = getElem as.data i ((id (α := as.data.length = n) h₁) ▸ h₂) :=
+  getLit_eq (as : Array α) (i : Nat) (h₁ : as.size = n) (h₂ : i < n) : as.getLit i h₁ h₂ = getElem as.toList i ((id (α := as.toList.length = n) h₁) ▸ h₂) :=
     rfl
 
-  go (i : Nat) (hi : i ≤ as.size) : toListLitAux as n hsz i hi (as.data.drop i) = as.data := by
+  go (i : Nat) (hi : i ≤ as.size) : toListLitAux as n hsz i hi (as.toList.drop i) = as.toList := by
     induction i <;> simp [getLit_eq, List.get_drop_eq_drop, toListLitAux, List.drop, *]
 
 def isPrefixOfAux [BEq α] (as bs : Array α) (hle : as.size ≤ bs.size) (i : Nat) : Bool :=

src/Init/Data/Array/Bootstrap.lean

@@ -15,76 +15,106 @@ This file contains some theorems about `Array` and `List` needed for `Init.Data.
 
 namespace Array
 
-theorem foldlM_eq_foldlM_data.aux [Monad m]
+theorem foldlM_eq_foldlM_toList.aux [Monad m]
     (f : β → α → m β) (arr : Array α) (i j) (H : arr.size ≤ i + j) (b) :
-    foldlM.loop f arr arr.size (Nat.le_refl _) i j b = (arr.data.drop j).foldlM f b := by
+    foldlM.loop f arr arr.size (Nat.le_refl _) i j b = (arr.toList.drop j).foldlM f b := by
   unfold foldlM.loop
   split; split
   · cases Nat.not_le_of_gt ‹_› (Nat.zero_add _ ▸ H)
   · rename_i i; rw [Nat.succ_add] at H
-    simp [foldlM_eq_foldlM_data.aux f arr i (j+1) H]
+    simp [foldlM_eq_foldlM_toList.aux f arr i (j+1) H]
     rw (config := {occs := .pos [2]}) [← List.get_drop_eq_drop _ _ ‹_›]
     rfl
   · rw [List.drop_of_length_le (Nat.ge_of_not_lt ‹_›)]; rfl
 
-theorem foldlM_eq_foldlM_data [Monad m]
+theorem foldlM_eq_foldlM_toList [Monad m]
     (f : β → α → m β) (init : β) (arr : Array α) :
-    arr.foldlM f init = arr.data.foldlM f init := by
-  simp [foldlM, foldlM_eq_foldlM_data.aux]
+    arr.foldlM f init = arr.toList.foldlM f init := by
+  simp [foldlM, foldlM_eq_foldlM_toList.aux]
 
-theorem foldl_eq_foldl_data (f : β → α → β) (init : β) (arr : Array α) :
-    arr.foldl f init = arr.data.foldl f init :=
-  List.foldl_eq_foldlM .. ▸ foldlM_eq_foldlM_data ..
+theorem foldl_eq_foldl_toList (f : β → α → β) (init : β) (arr : Array α) :
+    arr.foldl f init = arr.toList.foldl f init :=
+  List.foldl_eq_foldlM .. ▸ foldlM_eq_foldlM_toList ..
 
-theorem foldrM_eq_reverse_foldlM_data.aux [Monad m]
+theorem foldrM_eq_reverse_foldlM_toList.aux [Monad m]
     (f : α → β → m β) (arr : Array α) (init : β) (i h) :
-    (arr.data.take i).reverse.foldlM (fun x y => f y x) init = foldrM.fold f arr 0 i h init := by
+    (arr.toList.take i).reverse.foldlM (fun x y => f y x) init = foldrM.fold f arr 0 i h init := by
   unfold foldrM.fold
   match i with
   | 0 => simp [List.foldlM, List.take]
   | i+1 => rw [← List.take_concat_get _ _ h]; simp [← (aux f arr · i)]; rfl
 
-theorem foldrM_eq_reverse_foldlM_data [Monad m] (f : α → β → m β) (init : β) (arr : Array α) :
-    arr.foldrM f init = arr.data.reverse.foldlM (fun x y => f y x) init := by
+theorem foldrM_eq_reverse_foldlM_toList [Monad m] (f : α → β → m β) (init : β) (arr : Array α) :
+    arr.foldrM f init = arr.toList.reverse.foldlM (fun x y => f y x) init := by
   have : arr = #[] ∨ 0 < arr.size :=
     match arr with | ⟨[]⟩ => .inl rfl | ⟨a::l⟩ => .inr (Nat.zero_lt_succ _)
   match arr, this with | _, .inl rfl => rfl | arr, .inr h => ?_
-  simp [foldrM, h, ← foldrM_eq_reverse_foldlM_data.aux, List.take_length]
+  simp [foldrM, h, ← foldrM_eq_reverse_foldlM_toList.aux, List.take_length]
 
-theorem foldrM_eq_foldrM_data [Monad m]
+theorem foldrM_eq_foldrM_toList [Monad m]
     (f : α → β → m β) (init : β) (arr : Array α) :
-    arr.foldrM f init = arr.data.foldrM f init := by
-  rw [foldrM_eq_reverse_foldlM_data, List.foldlM_reverse]
+    arr.foldrM f init = arr.toList.foldrM f init := by
+  rw [foldrM_eq_reverse_foldlM_toList, List.foldlM_reverse]
 
-theorem foldr_eq_foldr_data (f : α → β → β) (init : β) (arr : Array α) :
-    arr.foldr f init = arr.data.foldr f init :=
-  List.foldr_eq_foldrM .. ▸ foldrM_eq_foldrM_data ..
+theorem foldr_eq_foldr_toList (f : α → β → β) (init : β) (arr : Array α) :
+    arr.foldr f init = arr.toList.foldr f init :=
+  List.foldr_eq_foldrM .. ▸ foldrM_eq_foldrM_toList ..
 
-@[simp] theorem push_data (arr : Array α) (a : α) : (arr.push a).data = arr.data ++ [a] := by
+@[simp] theorem push_toList (arr : Array α) (a : α) : (arr.push a).toList = arr.toList ++ [a] := by
   simp [push, List.concat_eq_append]
 
-@[simp] theorem toListAppend_eq (arr : Array α) (l) : arr.toListAppend l = arr.data ++ l := by
-  simp [toListAppend, foldr_eq_foldr_data]
+@[simp] theorem toListAppend_eq (arr : Array α) (l) : arr.toListAppend l = arr.toList ++ l := by
+  simp [toListAppend, foldr_eq_foldr_toList]
 
-@[simp] theorem toList_eq (arr : Array α) : arr.toList = arr.data := by
-  simp [toList, foldr_eq_foldr_data]
+@[simp] theorem toListImpl_eq (arr : Array α) : arr.toListImpl = arr.toList := by
+  simp [toListImpl, foldr_eq_foldr_toList]
 
-@[simp] theorem pop_data (arr : Array α) : arr.pop.data = arr.data.dropLast := rfl
+@[simp] theorem pop_toList (arr : Array α) : arr.pop.toList = arr.toList.dropLast := rfl
 
 @[simp] theorem append_eq_append (arr arr' : Array α) : arr.append arr' = arr ++ arr' := rfl
 
-@[simp] theorem append_data (arr arr' : Array α) :
-    (arr ++ arr').data = arr.data ++ arr'.data := by
+@[simp] theorem append_toList (arr arr' : Array α) :
+    (arr ++ arr').toList = arr.toList ++ arr'.toList := by
   rw [← append_eq_append]; unfold Array.append
-  rw [foldl_eq_foldl_data]
-  induction arr'.data generalizing arr <;> simp [*]
+  rw [foldl_eq_foldl_toList]
+  induction arr'.toList generalizing arr <;> simp [*]
 
 @[simp] theorem appendList_eq_append
     (arr : Array α) (l : List α) : arr.appendList l = arr ++ l := rfl
 
-@[simp] theorem appendList_data (arr : Array α) (l : List α) :
-    (arr ++ l).data = arr.data ++ l := by
+@[simp] theorem appendList_toList (arr : Array α) (l : List α) :
+    (arr ++ l).toList = arr.toList ++ l := by
   rw [← appendList_eq_append]; unfold Array.appendList
   induction l generalizing arr <;> simp [*]
 
+@[deprecated foldlM_eq_foldlM_toList (since := "2024-09-09")]
+abbrev foldlM_eq_foldlM_data := @foldlM_eq_foldlM_toList
+
+@[deprecated foldl_eq_foldl_toList (since := "2024-09-09")]
+abbrev foldl_eq_foldl_data := @foldl_eq_foldl_toList
+
+@[deprecated foldrM_eq_reverse_foldlM_toList (since := "2024-09-09")]
+abbrev foldrM_eq_reverse_foldlM_data := @foldrM_eq_reverse_foldlM_toList
+
+@[deprecated foldrM_eq_foldrM_toList (since := "2024-09-09")]
+abbrev foldrM_eq_foldrM_data := @foldrM_eq_foldrM_toList
+
+@[deprecated foldr_eq_foldr_toList (since := "2024-09-09")]
+abbrev foldr_eq_foldr_data := @foldr_eq_foldr_toList
+
+@[deprecated push_toList (since := "2024-09-09")]
+abbrev push_data := @push_toList
+
+@[deprecated toListImpl_eq (since := "2024-09-09")]
+abbrev toList_eq := @toListImpl_eq
+
+@[deprecated pop_toList (since := "2024-09-09")]
+abbrev pop_data := @pop_toList
+
+@[deprecated append_toList (since := "2024-09-09")]
+abbrev append_data := @append_toList
+
+@[deprecated appendList_toList (since := "2024-09-09")]
+abbrev appendList_data := @appendList_toList
+
 end Array