refactor: remove Subarray.foldl and other slice operation aliases (#12441)

This PR removes `Subarray.foldl(M)`, `Subarray.toArray` and `Subarray.size` in favor of the `Std.Slice`-namespaced operations. Dot notation will continue to work. If, say, `Subarray.size` is explicitly referred to, an error suggesting to use `Std.Slice.size` will show up.
2026-02-20 09:18:33 +01:00 · 2026-02-20 09:18:33 +01:00 · 10770eda3e
commit 10770eda3e
parent 8038a8b890
4 changed files with 36 additions and 85 deletions
--- a/src/Init/Data/Array/Subarray.lean
+++ b/src/Init/Data/Array/Subarray.lean
@ -7,7 +7,7 @@ module

 prelude
 public import Init.Data.Array.Basic
-public import Init.Data.Slice.Basic
+public import Init.Data.Slice.Operations

 public section

@ -76,15 +76,17 @@ def Subarray.stop_le_array_size (xs : Subarray α) : xs.stop ≤ xs.array.size :

 namespace Subarray

-/--
-Computes the size of the subarray.
-/
-def size (s : Subarray α) : Nat :=
-  s.stop - s.start
+instance : SliceSize (Internal.SubarrayData α) where
+  size s := s.internalRepresentation.stop - s.internalRepresentation.start
+
+@[grind =, suggest_for Subarray.size]
+public theorem size_eq {xs : Subarray α} :
+    xs.size = xs.stop - xs.start := by
+  simp [Std.Slice.size, SliceSize.size, start, stop]

 theorem size_le_array_size {s : Subarray α} : s.size ≤ s.array.size := by
  let ⟨{array, start, stop, start_le_stop, stop_le_array_size}⟩ := s
-  simp only [size, ge_iff_le]
+  simp only [ge_iff_le, size_eq]
  apply Nat.le_trans (Nat.sub_le stop start)
  assumption

--- a/src/Init/Data/Slice/Array/Iterator.lean
+++ b/src/Init/Data/Slice/Array/Iterator.lean
@ -62,9 +62,6 @@ attribute [instance] Subarray.instToIterator

 universe v w

-instance : SliceSize (Internal.SubarrayData α) where
-  size s := s.internalRepresentation.stop - s.internalRepresentation.start
-
 instance {α : Type u} {m : Type v → Type w} [Monad m] : ForIn m (Subarray α) α :=
  inferInstance

@ -76,45 +73,6 @@ explicitly provide the wrapper function `Subarray.foldlM` for `Slice.foldlM`, pr
 specific docstring.
 -/

-/--
-Folds a monadic operation from left to right over the elements in a subarray.
-An accumulator of type `β` is constructed by starting with `init` and monadically combining each
-element of the subarray with the current accumulator value in turn. The monad in question may permit
-early termination or repetition.
-Examples:
-```lean example
-#eval #["red", "green", "blue"].toSubarray.foldlM (init := "") fun acc x => do
-  let l ← Option.guard (· ≠ 0) x.length
-  return s!"{acc}({l}){x} "
-```
-```output
-some "(3)red (5)green (4)blue "
-```
-```lean example
-#eval #["red", "green", "blue"].toSubarray.foldlM (init := 0) fun acc x => do
-  let l ← Option.guard (· ≠ 5) x.length
-  return s!"{acc}({l}){x} "
-```
-```output
-none
-```
-/
-@[inline]
-def Subarray.foldlM {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (f : β → α → m β) (init : β) (as : Subarray α) : m β :=
-  Slice.foldlM f (init := init) as
-
-/--
-Folds an operation from left to right over the elements in a subarray.
-An accumulator of type `β` is constructed by starting with `init` and combining each
-element of the subarray with the current accumulator value in turn.
-Examples:
- * `#["red", "green", "blue"].toSubarray.foldl (· + ·.length) 0 = 12`
- * `#["red", "green", "blue"].toSubarray.popFront.foldl (· + ·.length) 0 = 9`
-/
-@[inline]
-def Subarray.foldl {α : Type u} {β : Type v} (f : β → α → β) (init : β) (as : Subarray α) : β :=
-  Slice.foldl f (init := init) as
-
 /--
 The implementation of `ForIn.forIn` for `Subarray`, which allows it to be used with `for` loops in
 `do`-notation.
@ -126,16 +84,12 @@ def Subarray.forIn {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m]
 /--
 Allocates a new array that contains the contents of the subarray.
 -/
-@[coe]
-def Subarray.toArray (s : Subarray α) : Array α :=
+@[expose, coe]
+def Subarray.copy (s : Subarray α) : Array α :=
  Slice.toArray s

 instance instCoeSubarrayArray : Coe (Subarray α) (Array α) :=
-  ⟨Subarray.toArray⟩
-
-@[inherit_doc Subarray.toArray]
-def Subarray.copy (s : Subarray α) : Array α :=
-  Slice.toArray s
+  ⟨Subarray.copy⟩

@[simp]
 theorem Subarray.copy_eq_toArray {s : Subarray α} :
@ -149,7 +103,7 @@ theorem Subarray.sliceToArray_eq_toArray {s : Subarray α} :

 namespace Array

-@[inherit_doc Subarray.toArray]
+@[inherit_doc Subarray.copy]
 def ofSubarray (s : Subarray α) : Array α :=
  Slice.toArray s

--- a/src/Init/Data/Slice/Array/Lemmas.lean
+++ b/src/Init/Data/Slice/Array/Lemmas.lean
@ -121,7 +121,7 @@ public instance : LawfulSliceSize (Internal.SubarrayData α) where

 public theorem toArray_eq_sliceToArray {α : Type u} {s : Subarray α} :
    s.toArray = Slice.toArray s := by
-  simp [Subarray.toArray]
+  simp [Std.Slice.toArray]

@[simp]
 public theorem forIn_toList {α : Type u} {s : Subarray α}
@ -156,11 +156,11 @@ public theorem sliceFoldl_eq_foldl {α : Type u} {s : Subarray α} {f : β →
 public theorem foldlM_toList {m} [Monad m] {α : Type u} {s : Subarray α} {f}
    [LawfulMonad m] :
    s.toList.foldlM (init := init) f = s.foldlM (m := m) (init := init) f := by
-  simp [Std.Slice.foldlM_toList, sliceFoldlM_eq_foldlM]
+  simp [Std.Slice.foldlM_toList]

 public theorem foldl_toList {α : Type u} {s : Subarray α} {f} :
    s.toList.foldl (init := init) f = s.foldl (init := init) f := by
-  simp [Std.Slice.foldl_toList, sliceFoldl_eq_foldl]
+  simp [Std.Slice.foldl_toList]

 end Subarray

@ -251,21 +251,16 @@ public theorem Subarray.toList_eq_drop_take {xs : Subarray α} :
    xs.toList = (xs.array.toList.take xs.stop).drop xs.start := by
  rw [Subarray.toList_eq, Array.toList_extract, Std.Internal.List.extract_eq_drop_take']

-@[grind =]
-public theorem Subarray.size_eq {xs : Subarray α} :
-    xs.size = xs.stop - xs.start := by
-  simp [Subarray.size]
-
@[simp, grind =]
 public theorem Subarray.size_drop {xs : Subarray α} :
    (xs.drop i).size = xs.size - i := by
-  simp only [size, stop, drop, start]
+  simp only [size_eq, stop, drop, start]
  omega

@[simp, grind =]
 public theorem Subarray.size_take {xs : Subarray α} :
    (xs.take i).size = min i xs.size := by
-  simp only [size, stop, take, start]
+  simp only [size_eq, stop, take, start]
  omega

 public theorem Subarray.sliceSize_eq_size {xs : Subarray α} :
@ -273,7 +268,7 @@ public theorem Subarray.sliceSize_eq_size {xs : Subarray α} :
  rfl

 public theorem Subarray.getElem_eq_getElem_array {xs : Subarray α} {h : i < xs.size} :
-    xs[i] = xs.array[xs.start + i]'(by simp only [size] at h; have := xs.stop_le_array_size; omega) := by
+    xs[i] = xs.array[xs.start + i]'(by simp only [size_eq] at h; have := xs.stop_le_array_size; omega) := by
  rfl

 public theorem Subarray.getElem_toList {xs : Subarray α} {h : i < xs.toList.length} :
@ -297,24 +292,24 @@ public theorem Subarray.toList_take {xs : Subarray α} :
@[simp, grind =]
 public theorem Subarray.toArray_toList {xs : Subarray α} :
    xs.toList.toArray = xs.toArray := by
-  simp [Std.Slice.toList, Subarray.toArray, Std.Slice.toArray]
+  simp [Std.Slice.toList, Std.Slice.toArray, Std.Slice.toArray]

@[simp, grind =]
 public theorem Subarray.toList_toArray {xs : Subarray α} :
    xs.toArray.toList = xs.toList := by
-  simp [Std.Slice.toList, Subarray.toArray, Std.Slice.toArray]
+  simp [Std.Slice.toList, Std.Slice.toArray, Std.Slice.toArray]

@[simp, grind =]
 public theorem Subarray.length_toList {xs : Subarray α} :
    xs.toList.length = xs.size := by
  have : xs.start ≤ xs.stop := xs.internalRepresentation.start_le_stop
  have : xs.stop ≤ xs.array.size := xs.internalRepresentation.stop_le_array_size
-  simp [Subarray.toList_eq, Subarray.size]; omega
+  simp [Subarray.toList_eq, Subarray.size_eq]; omega

@[simp, grind =]
 public theorem Subarray.size_toArray {xs : Subarray α} :
    xs.toArray.size = xs.size := by
-  simp [← Subarray.toArray_toList, Subarray.size, Slice.size, SliceSize.size, start, stop]
+  simp [← Subarray.toArray_toList, Subarray.size_eq, start, stop]

 namespace Array

@ -708,7 +703,7 @@ public theorem toList_mkSlice_rco {xs : Subarray α} {lo hi : Nat} :
    Array.start_toSubarray, Array.stop_toSubarray, Array.toList_extract, List.take_drop,
    List.take_take]
  rw [Nat.add_sub_cancel' (by omega)]
-  simp [Subarray.size, ← Array.length_toList, ← List.take_eq_take_min, Nat.add_comm xs.start]
+  simp [Subarray.size_eq, ← Array.length_toList, ← List.take_eq_take_min, Nat.add_comm xs.start]

@[simp, grind =]
 public theorem toArray_mkSlice_rco {xs : Subarray α} {lo hi : Nat} :
@ -718,7 +713,7 @@ public theorem toArray_mkSlice_rco {xs : Subarray α} {lo hi : Nat} :
@[simp, grind =]
 public theorem size_mkSlice_rco {xs : Subarray α} {lo hi : Nat} :
    xs[lo...hi].size = min hi xs.size - lo := by
-  simp [← Subarray.length_toList]
+  simp [← length_toList, - length_toList_eq_size]

 public theorem mkSlice_rcc_eq_mkSlice_rco {xs : Subarray α} {lo hi : Nat} :
    xs[lo...=hi] = xs[lo...(hi + 1)] := by
@ -738,7 +733,7 @@ public theorem toArray_mkSlice_rcc {xs : Subarray α} {lo hi : Nat} :
@[simp, grind =]
 public theorem size_mkSlice_rcc {xs : Subarray α} {lo hi : Nat} :
    xs[lo...=hi].size = min (hi + 1) xs.size - lo := by
-  simp [← Subarray.length_toList]
+  simp [← length_toList, - length_toList_eq_size]

 public theorem mkSlice_rci_eq_mkSlice_rco {xs : Subarray α} {lo : Nat} :
    xs[lo...*] = xs[lo...xs.size] := by
@ -758,7 +753,7 @@ public theorem toArray_mkSlice_rci {xs : Subarray α} {lo : Nat} :
@[simp, grind =]
 public theorem size_mkSlice_rci {xs : Subarray α} {lo : Nat} :
    xs[lo...*].size = xs.size - lo := by
-  simp [← Subarray.length_toList]
+  simp [← length_toList, - length_toList_eq_size]

 public theorem mkSlice_roc_eq_mkSlice_roo {xs : Subarray α} {lo hi : Nat} :
    xs[lo<...=hi] = xs[lo<...(hi + 1)] := by
@ -787,7 +782,7 @@ public theorem toArray_mkSlice_roo {xs : Subarray α} {lo hi : Nat} :
@[simp, grind =]
 public theorem size_mkSlice_roo {xs : Subarray α} {lo hi : Nat} :
    xs[lo<...hi].size = min hi xs.size - (lo + 1) := by
-  simp [← Subarray.length_toList]
+  simp [← length_toList, - length_toList_eq_size]

 public theorem mkSlice_roc_eq_mkSlice_rcc {xs : Subarray α} {lo hi : Nat} :
    xs[lo<...=hi] = xs[(lo + 1)...=hi] := by
@ -806,7 +801,7 @@ public theorem toArray_mkSlice_roc {xs : Subarray α} {lo hi : Nat} :
@[simp, grind =]
 public theorem size_mkSlice_roc {xs : Subarray α} {lo hi : Nat} :
    xs[lo<...=hi].size = min (hi + 1) xs.size - (lo + 1) := by
-  simp [← Subarray.length_toList]
+  simp [← length_toList, - length_toList_eq_size]

 public theorem mkSlice_roi_eq_mkSlice_rci {xs : Subarray α} {lo : Nat} :
    xs[lo<...*] = xs[(lo + 1)...*] := by
@ -830,7 +825,7 @@ public theorem toArray_mkSlice_roi {xs : Subarray α} {lo : Nat} :
@[simp, grind =]
 public theorem size_mkSlice_roi {xs : Subarray α} {lo : Nat} :
    xs[lo<...*].size = xs.size - (lo + 1) := by
-  simp [← Subarray.length_toList]
+  simp [← length_toList, - length_toList_eq_size]

 public theorem mkSlice_ric_eq_mkSlice_rio {xs : Subarray α} {hi : Nat} :
    xs[*...=hi] = xs[*...(hi + 1)] := by
@ -859,7 +854,7 @@ public theorem toArray_mkSlice_rio {xs : Subarray α} {hi : Nat} :
@[simp, grind =]
 public theorem size_mkSlice_rio {xs : Subarray α} {hi : Nat} :
    xs[*...hi].size = min hi xs.size := by
-  simp [← Subarray.length_toList]
+  simp [← length_toList, - length_toList_eq_size]

 public theorem mkSlice_ric_eq_mkSlice_rcc {xs : Subarray α} {hi : Nat} :
    xs[*...=hi] = xs[0...=hi] := by
@ -880,7 +875,7 @@ public theorem toArray_mkSlice_ric {xs : Subarray α} {hi : Nat} :
@[simp, grind =]
 public theorem size_mkSlice_ric {xs : Subarray α} {hi : Nat} :
    xs[*...=hi].size = min (hi + 1) xs.size := by
-  simp [← Subarray.length_toList]
+  simp [← length_toList, - length_toList_eq_size]

@[simp, grind =, grind =]
 public theorem mkSlice_rii {xs : Subarray α} :
--- a/src/Init/Data/Slice/Operations.lean
+++ b/src/Init/Data/Slice/Operations.lean
@ -51,12 +51,12 @@ Returns the number of elements with distinct indices in the given slice.

 Example: `#[1, 1, 1][0...2].size = 2`.
 -/
-@[always_inline, inline]
+@[expose, always_inline, inline, suggest_for Subarray.size]
 def size (s : Slice γ) [SliceSize γ] :=
  SliceSize.size s

 /-- Allocates a new array that contains the elements of the slice. -/
-@[always_inline, inline]
+@[always_inline, inline, suggest_for Subarray.toArray]
 def toArray [ToIterator (Slice γ) Id α β] [Iterator α Id β]
    (s : Slice γ) : Array β :=
  Internal.iter s |>.toArray
@ -103,7 +103,7 @@ some "(3)red (5)green (4)blue "
 none
 ```
 -/
-@[always_inline, inline]
+@[always_inline, inline, suggest_for Subarray.foldlM]
 def foldlM {γ : Type u} {β : Type v}
    {δ : Type w} {m : Type w → Type w'} [Monad m] (f : δ → β → m δ) (init : δ)
    [ToIterator (Slice γ) Id α β] [Iterator α Id β]
@ -119,7 +119,7 @@ Examples for the special case of subarrays:
 * `#["red", "green", "blue"].toSubarray.foldl (· + ·.length) 0 = 12`
 * `#["red", "green", "blue"].toSubarray.popFront.foldl (· + ·.length) 0 = 9`
 -/
-@[always_inline, inline]
+@[always_inline, inline, suggest_for Subarray.foldl]
 def foldl {γ : Type u} {β : Type v}
    {δ : Type w} (f : δ → β → δ) (init : δ)
    [ToIterator (Slice γ) Id α β] [Iterator α Id β]