deprecation

src/Init/Data/Array/Basic.lean

@@ -613,13 +613,18 @@ def concatMapM [Monad m] (f : α → m (Array β)) (as : Array α) : m (Array β
 def concatMap (f : α → Array β) (as : Array α) : Array β :=
   as.foldl (init := empty) fun bs a => bs ++ f a
 
-/-- Joins array of array into a single array.
+/--
+Concatenates an array of arrays into a single array.
 
-`flatten #[#[a₁, a₂, ⋯], #[b₁, b₂, ⋯], ⋯]` = `#[a₁, a₂, ⋯, b₁, b₂, ⋯]`
+`O(|join L|)`.
+
+`join #[#[a₁, a₂, ⋯], #[b₁, b₂, ⋯], ⋯]` = `#[a₁, a₂, ⋯, b₁, b₂, ⋯]`
 -/
-def flatten (as : Array (Array α)) : Array α :=
+@[inline] def join (as : Array (Array α)) : Array α :=
   as.foldl (init := empty) fun r a => r ++ a
 
+@[deprecated join (since := "2024-09-30")] abbrev flatten := @join
+
 @[inline]
 def filter (p : α → Bool) (as : Array α) (start := 0) (stop := as.size) : Array α :=
   as.foldl (init := #[]) (start := start) (stop := stop) fun r a =>

src/Init/Data/Array/Lemmas.lean

@@ -996,6 +996,27 @@ abbrev get_append_right := @getElem_append_right
 theorem append_assoc (as bs cs : Array α) : as ++ bs ++ cs = as ++ (bs ++ cs) := by
   apply ext'; simp only [toList_append, List.append_assoc]
 
+/-! ### join -/
+
+@[simp] theorem toList_join {l : Array (Array α)} : l.join.toList = (l.toList.map toList).join := by
+  dsimp [join]
+  simp only [foldl_eq_foldl_toList]
+  generalize l.toList = l
+  have : ∀ a : Array α, (List.foldl ?_ a l).toList = a.toList ++ ?_ := ?_
+  exact this #[]
+  induction l with
+  | nil => simp
+  | cons h => induction h.toList <;> simp [*]
+
+theorem mem_join : ∀ {L : Array (Array α)}, a ∈ L.join ↔ ∃ l, l ∈ L ∧ a ∈ l := by
+  simp only [mem_def, toList_join, List.mem_join, List.mem_map]
+  intro l
+  constructor
+  · rintro ⟨_, ⟨s, m, rfl⟩, h⟩
+    exact ⟨s, m, h⟩
+  · rintro ⟨s, h₁, h₂⟩
+    refine ⟨s.toList, ⟨⟨s, h₁, rfl⟩, h₂⟩⟩
+
 /-! ### extract -/
 
 theorem extract_loop_zero (as bs : Array α) (start : Nat) : extract.loop as 0 start bs = bs := by
@@ -1448,6 +1469,10 @@ Our goal is to have `simp` "pull `List.toArray` outwards" as much as possible.
   apply ext'
   erw [toList_filterMap] -- `erw` required to unify `l.length` with `l.toArray.size`.
 
+@[simp] theorem join_toArray (l : List (List α)) : (l.toArray.map List.toArray).join = l.join.toArray := by
+  apply ext'
+  simp [Function.comp_def]
+
 @[simp] theorem toArray_range (n : Nat) : (range n).toArray = Array.range n := by
   apply ext'
   simp

src/Lean/Elab/PreDefinition/Structural/Basic.lean

@@ -73,7 +73,7 @@ def Positions.groupAndSort {α β} [Inhabited α] [DecidableEq β]
     (f : α → β) (xs : Array α) (ys : Array β) : Positions :=
   let positions := ys.map fun y => (Array.range xs.size).filter fun i => f xs[i]! = y
   -- Sanity check: is this really a grouped permutation of all the indices?
-  assert! Array.range xs.size == positions.flatten.qsort Nat.blt
+  assert! Array.range xs.size == positions.join.qsort Nat.blt
   positions
 
 /--

src/Lean/Util/Profiler.lean

@@ -316,7 +316,7 @@ weights. Minimizes profile size while preserving per-stack timing information.
 def Profile.collide (ps : Array Profile) : Option Profile := do
   let base ← ps[0]?
   let thread := Thread.new "collided"
-  let thread := ps.map (·.threads) |>.flatten.foldl collideThreads { thread with }
+  let thread := ps.map (·.threads) |>.join.foldl collideThreads { thread with }
   return { base with threads := #[thread.toThread] }
 
 end Lean.Firefox