chore: reordering in Array.Basic

This is to simplify the manual's cross-referencing.

src/Init/Data/Array.lean

@@ -15,3 +15,4 @@ import Init.Data.Array.BasicAux
 import Init.Data.Array.Lemmas
 import Init.Data.Array.TakeDrop
 import Init.Data.Array.Bootstrap
+import Init.Data.Array.GetLit

src/Init/Data/Array/Basic.lean

@@ -13,43 +13,76 @@ import Init.Data.ToString.Basic
 import Init.GetElem
 universe u v w
 
-namespace Array
+/-! ### Array literal syntax -/
+
+syntax "#[" withoutPosition(sepBy(term, ", ")) "]" : term
+
+macro_rules
+  | `(#[ $elems,* ]) => `(List.toArray [ $elems,* ])
+
 variable {α : Type u}
 
+namespace Array
+
+/-! ### Preliminary theorems -/
+
+@[simp] theorem size_set (a : Array α) (i : Fin a.size) (v : α) : (set a i v).size = a.size :=
+  List.length_set ..
+
+@[simp] theorem size_push (a : Array α) (v : α) : (push a v).size = a.size + 1 :=
+  List.length_concat ..
+
+theorem ext (a b : Array α)
+    (h₁ : a.size = b.size)
+    (h₂ : (i : Nat) → (hi₁ : i < a.size) → (hi₂ : i < b.size) → a[i] = b[i])
+    : a = b := by
+  let rec extAux (a b : List α)
+      (h₁ : a.length = b.length)
+      (h₂ : (i : Nat) → (hi₁ : i < a.length) → (hi₂ : i < b.length) → a.get ⟨i, hi₁⟩ = b.get ⟨i, hi₂⟩)
+      : a = b := by
+    induction a generalizing b with
+    | nil =>
+      cases b with
+      | nil       => rfl
+      | cons b bs => rw [List.length_cons] at h₁; injection h₁
+    | cons a as ih =>
+      cases b with
+      | nil => rw [List.length_cons] at h₁; injection h₁
+      | cons b bs =>
+        have hz₁ : 0 < (a::as).length := by rw [List.length_cons]; apply Nat.zero_lt_succ
+        have hz₂ : 0 < (b::bs).length := by rw [List.length_cons]; apply Nat.zero_lt_succ
+        have headEq : a = b := h₂ 0 hz₁ hz₂
+        have h₁' : as.length = bs.length := by rw [List.length_cons, List.length_cons] at h₁; injection h₁
+        have h₂' : (i : Nat) → (hi₁ : i < as.length) → (hi₂ : i < bs.length) → as.get ⟨i, hi₁⟩ = bs.get ⟨i, hi₂⟩ := by
+          intro i hi₁ hi₂
+          have hi₁' : i+1 < (a::as).length := by rw [List.length_cons]; apply Nat.succ_lt_succ; assumption
+          have hi₂' : i+1 < (b::bs).length := by rw [List.length_cons]; apply Nat.succ_lt_succ; assumption
+          have : (a::as).get ⟨i+1, hi₁'⟩ = (b::bs).get ⟨i+1, hi₂'⟩ := h₂ (i+1) hi₁' hi₂'
+          apply this
+        have tailEq : as = bs := ih bs h₁' h₂'
+        rw [headEq, tailEq]
+  cases a; cases b
+  apply congrArg
+  apply extAux
+  assumption
+  assumption
+
+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).toList = acc.toList ++ as := by
+  induction as generalizing acc <;> simp [*, List.toArrayAux, Array.push, List.append_assoc, List.concat_eq_append]
+
+@[simp] theorem toList_toArray (as : List α) : as.toArray.toList = as := by
+  simp [List.toArray, Array.mkEmpty]
+
+@[simp] theorem size_toArray (as : List α) : as.toArray.size = as.length := by simp [size]
+
+@[deprecated toList_toArray (since := "2024-09-09")] abbrev data_toArray := @toList_toArray
+
 @[deprecated Array.toList (since := "2024-09-10")] abbrev Array.data := @Array.toList
 
-@[extern "lean_mk_array"]
-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`.
-```
-ofFn f = #[f 0, f 1, ... , f(n - 1)]
-``` -/
-def ofFn {n} (f : Fin n → α) : Array α := go 0 (mkEmpty n) where
-  /-- Auxiliary for `ofFn`. `ofFn.go f i acc = acc ++ #[f i, ..., f(n - 1)]` -/
-  go (i : Nat) (acc : Array α) : Array α :=
-    if h : i < n then go (i+1) (acc.push (f ⟨i, h⟩)) else acc
-termination_by n - i
-decreasing_by simp_wf; decreasing_trivial_pre_omega
-
-/-- The array `#[0, 1, ..., n - 1]`. -/
-def range (n : Nat) : Array Nat :=
-  n.fold (flip Array.push) (mkEmpty n)
-
-@[simp] theorem size_mkArray (n : Nat) (v : α) : (mkArray n v).size = n :=
-  List.length_replicate ..
-
-instance : EmptyCollection (Array α) := ⟨Array.empty⟩
-instance : Inhabited (Array α) where
-  default := Array.empty
-
-@[simp] def isEmpty (a : Array α) : Bool :=
-  a.size = 0
-
-def singleton (v : α) : Array α :=
-  mkArray 1 v
+/-! ### Externs -/
 
 /-- Low-level version of `size` that directly queries the C array object cached size.
     While this is not provable, `usize` always returns the exact size of the array since
@@ -65,29 +98,6 @@ def usize (a : @& Array α) : USize := a.size.toUSize
 def uget (a : @& Array α) (i : USize) (h : i.toNat < a.size) : α :=
   a[i.toNat]
 
-instance : GetElem (Array α) USize α fun xs i => i.toNat < xs.size where
-  getElem xs i h := xs.uget i h
-
-def back [Inhabited α] (a : Array α) : α :=
-  a.get! (a.size - 1)
-
-def get? (a : Array α) (i : Nat) : Option α :=
-  if h : i < a.size then some a[i] else none
-
-def back? (a : Array α) : Option α :=
-  a.get? (a.size - 1)
-
--- auxiliary declaration used in the equation compiler when pattern matching array literals.
-abbrev getLit {α : Type u} {n : Nat} (a : Array α) (i : Nat) (h₁ : a.size = n) (h₂ : i < n) : α :=
-  have := h₁.symm ▸ h₂
-  a[i]
-
-@[simp] theorem size_set (a : Array α) (i : Fin a.size) (v : α) : (set a i v).size = a.size :=
-  List.length_set ..
-
-@[simp] theorem size_push (a : Array α) (v : α) : (push a v).size = a.size + 1 :=
-  List.length_concat ..
-
 /-- Low-level version of `fset` which is as fast as a C array fset.
    `Fin` values are represented as tag pointers in the Lean runtime. Thus,
    `fset` may be slightly slower than `uset`. -/
@@ -95,6 +105,19 @@ abbrev getLit {α : Type u} {n : Nat} (a : Array α) (i : Nat) (h₁ : a.size =
 def uset (a : Array α) (i : USize) (v : α) (h : i.toNat < a.size) : Array α :=
   a.set ⟨i.toNat, h⟩ v
 
+@[extern "lean_array_pop"]
+def pop (a : Array α) : Array α where
+  toList := a.toList.dropLast
+
+@[simp] theorem size_pop (a : Array α) : a.pop.size = a.size - 1 := by
+  match a with
+  | ⟨[]⟩ => rfl
+  | ⟨a::as⟩ => simp [pop, Nat.succ_sub_succ_eq_sub, size]
+
+@[extern "lean_mk_array"]
+def mkArray {α : Type u} (n : Nat) (v : α) : Array α where
+  toList := List.replicate n v
+
 /--
 Swaps two entries in an array.
 
@@ -108,6 +131,10 @@ def swap (a : Array α) (i j : @& Fin a.size) : Array α :=
   let a'  := a.set i v₂
   a'.set (size_set a i v₂ ▸ j) v₁
 
+@[simp] theorem size_swap (a : Array α) (i j : Fin a.size) : (a.swap i j).size = a.size := by
+  show ((a.set i (a.get j)).set (size_set a i _ ▸ j) (a.get i)).size = a.size
+  rw [size_set, size_set]
+
 /--
 Swaps two entries in an array, or returns the array unchanged if either index is out of bounds.
 
@@ -121,6 +148,66 @@ def swap! (a : Array α) (i j : @& Nat) : Array α :=
   else a
   else a
 
+/-! ### GetElem instance for `USize`, backed by `uget` -/
+
+instance : GetElem (Array α) USize α fun xs i => i.toNat < xs.size where
+  getElem xs i h := xs.uget i h
+
+/-! ### Definitions -/
+
+instance : EmptyCollection (Array α) := ⟨Array.empty⟩
+instance : Inhabited (Array α) where
+  default := Array.empty
+
+@[simp] def isEmpty (a : Array α) : Bool :=
+  a.size = 0
+
+-- TODO(Leo): cleanup
+@[specialize]
+def isEqvAux (a b : Array α) (hsz : a.size = b.size) (p : α → α → Bool) (i : Nat) : Bool :=
+  if h : i < a.size then
+     have : i < b.size := hsz ▸ h
+     p a[i] b[i] && isEqvAux a b hsz p (i+1)
+  else
+    true
+decreasing_by simp_wf; decreasing_trivial_pre_omega
+
+@[inline] def isEqv (a b : Array α) (p : α → α → Bool) : Bool :=
+  if h : a.size = b.size then
+    isEqvAux a b h p 0
+  else
+    false
+
+instance [BEq α] : BEq (Array α) :=
+  ⟨fun a b => isEqv a b BEq.beq⟩
+
+/--
+`ofFn f` with `f : Fin n → α` returns the list whose ith element is `f i`.
+```
+ofFn f = #[f 0, f 1, ... , f(n - 1)]
+``` -/
+def ofFn {n} (f : Fin n → α) : Array α := go 0 (mkEmpty n) where
+  /-- Auxiliary for `ofFn`. `ofFn.go f i acc = acc ++ #[f i, ..., f(n - 1)]` -/
+  go (i : Nat) (acc : Array α) : Array α :=
+    if h : i < n then go (i+1) (acc.push (f ⟨i, h⟩)) else acc
+decreasing_by simp_wf; decreasing_trivial_pre_omega
+
+/-- The array `#[0, 1, ..., n - 1]`. -/
+def range (n : Nat) : Array Nat :=
+  n.fold (flip Array.push) (mkEmpty n)
+
+def singleton (v : α) : Array α :=
+  mkArray 1 v
+
+def back [Inhabited α] (a : Array α) : α :=
+  a.get! (a.size - 1)
+
+def get? (a : Array α) (i : Nat) : Option α :=
+  if h : i < a.size then some a[i] else none
+
+def back? (a : Array α) : Option α :=
+  a.get? (a.size - 1)
+
 @[inline] def swapAt (a : Array α) (i : Fin a.size) (v : α) : α × Array α :=
   let e := a.get i
   let a := a.set i v
@@ -134,10 +221,6 @@ def swapAt! (a : Array α) (i : Nat) (v : α) : α × Array α :=
     have : Inhabited α := ⟨v⟩
     panic! ("index " ++ toString i ++ " out of bounds")
 
-@[extern "lean_array_pop"]
-def pop (a : Array α) : Array α where
-  toList := a.toList.dropLast
-
 def shrink (a : Array α) (n : Nat) : Array α :=
   let rec loop
     | 0,   a => a
@@ -311,7 +394,6 @@ def mapM {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (f : α
       map (i+1) (r.push (← f as[i]))
     else
       pure r
-  termination_by as.size - i
   decreasing_by simp_wf; decreasing_trivial_pre_omega
   map 0 (mkEmpty as.size)
 
@@ -384,7 +466,6 @@ def anyM {α : Type u} {m : Type → Type w} [Monad m] (p : α → m Bool) (as :
           loop (j+1)
       else
         pure false
-      termination_by stop - j
       decreasing_by simp_wf; decreasing_trivial_pre_omega
     loop start
   if h : stop ≤ as.size then
@@ -470,12 +551,22 @@ def findIdx? {α : Type u} (as : Array α) (p : α → Bool) : Option Nat :=
     if h : j < as.size then
       if p as[j] then some j else loop (j + 1)
     else none
-    termination_by as.size - j
     decreasing_by simp_wf; decreasing_trivial_pre_omega
   loop 0
 
 def getIdx? [BEq α] (a : Array α) (v : α) : Option Nat :=
-a.findIdx? fun a => a == v
+  a.findIdx? fun a => a == v
+
+def indexOfAux [BEq α] (a : Array α) (v : α) (i : Nat) : Option (Fin a.size) :=
+  if h : i < a.size then
+    let idx : Fin a.size := ⟨i, h⟩;
+    if a.get idx == v then some idx
+    else indexOfAux a v (i+1)
+  else none
+decreasing_by simp_wf; decreasing_trivial_pre_omega
+
+def indexOf? [BEq α] (a : Array α) (v : α) : Option (Fin a.size) :=
+  indexOfAux a v 0
 
 @[inline]
 def any (as : Array α) (p : α → Bool) (start := 0) (stop := as.size) : Bool :=
@@ -491,13 +582,6 @@ def contains [BEq α] (as : Array α) (a : α) : Bool :=
 def elem [BEq α] (a : α) (as : Array α) : Bool :=
   as.contains a
 
-@[inline] def getEvenElems (as : Array α) : Array α :=
-  (·.2) <| as.foldl (init := (true, Array.empty)) fun (even, r) a =>
-    if even then
-      (false, r.push a)
-    else
-      (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.toList`
 -- (the projection) to implement this functionality.
@@ -510,17 +594,6 @@ def toListImpl (as : Array α) : List α :=
 def toListAppend (as : Array α) (l : List α) : List α :=
   as.foldr List.cons l
 
-instance {α : Type u} [Repr α] : Repr (Array α) where
-  reprPrec a _ :=
-    let _ : Std.ToFormat α := ⟨repr⟩
-    if a.size == 0 then
-      "#[]"
-    else
-      Std.Format.bracketFill "#[" (Std.Format.joinSep (toList a) ("," ++ Std.Format.line)) "]"
-
-instance [ToString α] : ToString (Array α) where
-  toString a := "#" ++ toString a.toList
-
 protected def append (as : Array α) (bs : Array α) : Array α :=
   bs.foldl (init := as) fun r v => r.push v
 
@@ -546,44 +619,13 @@ def concatMap (f : α → Array β) (as : Array α) : Array β :=
 def flatten (as : Array (Array α)) : Array α :=
   as.foldl (init := empty) fun r a => r ++ a
 
-end Array
-
-export Array (mkArray)
-
-syntax "#[" withoutPosition(sepBy(term, ", ")) "]" : term
-
-macro_rules
-  | `(#[ $elems,* ]) => `(List.toArray [ $elems,* ])
-
-namespace Array
-
--- TODO(Leo): cleanup
-@[specialize]
-def isEqvAux (a b : Array α) (hsz : a.size = b.size) (p : α → α → Bool) (i : Nat) : Bool :=
-  if h : i < a.size then
-     have : i < b.size := hsz ▸ h
-     p a[i] b[i] && isEqvAux a b hsz p (i+1)
-  else
-    true
-termination_by a.size - i
-decreasing_by simp_wf; decreasing_trivial_pre_omega
-
-@[inline] def isEqv (a b : Array α) (p : α → α → Bool) : Bool :=
-  if h : a.size = b.size then
-    isEqvAux a b h p 0
-  else
-    false
-
-instance [BEq α] : BEq (Array α) :=
-  ⟨fun a b => isEqv a b BEq.beq⟩
-
 @[inline]
 def filter (p : α → Bool) (as : Array α) (start := 0) (stop := as.size) : Array α :=
   as.foldl (init := #[]) (start := start) (stop := stop) fun r a =>
     if p a then r.push a else r
 
 @[inline]
-def filterM [Monad m] (p : α → m Bool) (as : Array α) (start := 0) (stop := as.size) : m (Array α) :=
+def filterM {α : Type} [Monad m] (p : α → m Bool) (as : Array α) (start := 0) (stop := as.size) : m (Array α) :=
   as.foldlM (init := #[]) (start := start) (stop := stop) fun r a => do
     if (← p a) then return r.push a else return r
 
@@ -618,92 +660,23 @@ def partition (p : α → Bool) (as : Array α) : Array α × Array α := Id.run
       cs := cs.push a
   return (bs, cs)
 
-theorem ext (a b : Array α)
-    (h₁ : a.size = b.size)
-    (h₂ : (i : Nat) → (hi₁ : i < a.size) → (hi₂ : i < b.size) → a[i] = b[i])
-    : a = b := by
-  let rec extAux (a b : List α)
-      (h₁ : a.length = b.length)
-      (h₂ : (i : Nat) → (hi₁ : i < a.length) → (hi₂ : i < b.length) → a.get ⟨i, hi₁⟩ = b.get ⟨i, hi₂⟩)
-      : a = b := by
-    induction a generalizing b with
-    | nil =>
-      cases b with
-      | nil       => rfl
-      | cons b bs => rw [List.length_cons] at h₁; injection h₁
-    | cons a as ih =>
-      cases b with
-      | nil => rw [List.length_cons] at h₁; injection h₁
-      | cons b bs =>
-        have hz₁ : 0 < (a::as).length := by rw [List.length_cons]; apply Nat.zero_lt_succ
-        have hz₂ : 0 < (b::bs).length := by rw [List.length_cons]; apply Nat.zero_lt_succ
-        have headEq : a = b := h₂ 0 hz₁ hz₂
-        have h₁' : as.length = bs.length := by rw [List.length_cons, List.length_cons] at h₁; injection h₁
-        have h₂' : (i : Nat) → (hi₁ : i < as.length) → (hi₂ : i < bs.length) → as.get ⟨i, hi₁⟩ = bs.get ⟨i, hi₂⟩ := by
-          intro i hi₁ hi₂
-          have hi₁' : i+1 < (a::as).length := by rw [List.length_cons]; apply Nat.succ_lt_succ; assumption
-          have hi₂' : i+1 < (b::bs).length := by rw [List.length_cons]; apply Nat.succ_lt_succ; assumption
-          have : (a::as).get ⟨i+1, hi₁'⟩ = (b::bs).get ⟨i+1, hi₂'⟩ := h₂ (i+1) hi₁' hi₂'
-          apply this
-        have tailEq : as = bs := ih bs h₁' h₂'
-        rw [headEq, tailEq]
-  cases a; cases b
-  apply congrArg
-  apply extAux
-  assumption
-  assumption
-
-theorem extLit {n : Nat}
-    (a b : Array α)
-    (hsz₁ : a.size = n) (hsz₂ : b.size = n)
-    (h : (i : Nat) → (hi : i < n) → a.getLit i hsz₁ hi = b.getLit i hsz₂ hi) : a = b :=
-  Array.ext a b (hsz₁.trans hsz₂.symm) fun i hi₁ _ => h i (hsz₁ ▸ hi₁)
-
-end Array
-
--- CLEANUP the following code
-namespace Array
-
-def indexOfAux [BEq α] (a : Array α) (v : α) (i : Nat) : Option (Fin a.size) :=
-  if h : i < a.size then
-    let idx : Fin a.size := ⟨i, h⟩;
-    if a.get idx == v then some idx
-    else indexOfAux a v (i+1)
-  else none
-termination_by a.size - i
-decreasing_by simp_wf; decreasing_trivial_pre_omega
-
-def indexOf? [BEq α] (a : Array α) (v : α) : Option (Fin a.size) :=
-  indexOfAux a v 0
-
-@[simp] theorem size_swap (a : Array α) (i j : Fin a.size) : (a.swap i j).size = a.size := by
-  show ((a.set i (a.get j)).set (size_set a i _ ▸ j) (a.get i)).size = a.size
-  rw [size_set, size_set]
-
-@[simp] theorem size_pop (a : Array α) : a.pop.size = a.size - 1 := by
-  match a with
-  | ⟨[]⟩ => rfl
-  | ⟨a::as⟩ => simp [pop, Nat.succ_sub_succ_eq_sub, size]
-
-theorem reverse.termination {i j : Nat} (h : i < j) : j - 1 - (i + 1) < j - i := by
-  rw [Nat.sub_sub, Nat.add_comm]
-  exact Nat.lt_of_le_of_lt (Nat.pred_le _) (Nat.sub_succ_lt_self _ _ h)
-
 def reverse (as : Array α) : Array α :=
   if h : as.size ≤ 1 then
     as
   else
     loop as 0 ⟨as.size - 1, Nat.pred_lt (mt (fun h : as.size = 0 => h ▸ by decide) h)⟩
 where
+  termination {i j : Nat} (h : i < j) : j - 1 - (i + 1) < j - i := by
+    rw [Nat.sub_sub, Nat.add_comm]
+    exact Nat.lt_of_le_of_lt (Nat.pred_le _) (Nat.sub_succ_lt_self _ _ h)
   loop (as : Array α) (i : Nat) (j : Fin as.size) :=
     if h : i < j then
-      have := reverse.termination h
+      have := termination h
       let as := as.swap ⟨i, Nat.lt_trans h j.2⟩ j
       have : j-1 < as.size := by rw [size_swap]; exact Nat.lt_of_le_of_lt (Nat.pred_le _) j.2
       loop as (i+1) ⟨j-1, this⟩
     else
       as
-termination_by j - i
 
 def popWhile (p : α → Bool) (as : Array α) : Array α :=
   if h : as.size > 0 then
@@ -713,7 +686,6 @@ def popWhile (p : α → Bool) (as : Array α) : Array α :=
       as
   else
     as
-termination_by as.size
 decreasing_by simp_wf; decreasing_trivial_pre_omega
 
 def takeWhile (p : α → Bool) (as : Array α) : Array α :=
@@ -726,7 +698,6 @@ def takeWhile (p : α → Bool) (as : Array α) : Array α :=
         r
     else
       r
-    termination_by as.size - i
     decreasing_by simp_wf; decreasing_trivial_pre_omega
   go 0 #[]
 
@@ -744,6 +715,7 @@ def feraseIdx (a : Array α) (i : Fin a.size) : Array α :=
 termination_by a.size - i.val
 decreasing_by simp_wf; exact Nat.sub_succ_lt_self _ _ i.isLt
 
+-- This is required in `Lean.Data.PersistentHashMap`.
 theorem size_feraseIdx (a : Array α) (i : Fin a.size) : (a.feraseIdx i).size = a.size - 1 := by
   induction a, i using Array.feraseIdx.induct with
   | @case1 a i h a' _ ih =>
@@ -774,7 +746,6 @@ def erase [BEq α] (as : Array α) (a : α) : Array α :=
       loop as ⟨j', by rw [size_swap]; exact j'.2⟩
     else
       as
-    termination_by j.1
     decreasing_by simp_wf; decreasing_trivial_pre_omega
   let j := as.size
   let as := as.push a
@@ -786,41 +757,6 @@ def insertAt! (as : Array α) (i : Nat) (a : α) : Array α :=
     insertAt as ⟨i, Nat.lt_succ_of_le h⟩ a
   else panic! "invalid index"
 
-def toListLitAux (a : Array α) (n : Nat) (hsz : a.size = n) : ∀ (i : Nat), i ≤ a.size → List α → List α
-  | 0,     _,  acc => acc
-  | (i+1), hi, acc => toListLitAux a n hsz i (Nat.le_of_succ_le hi) (a.getLit i hsz (Nat.lt_of_lt_of_eq (Nat.lt_of_lt_of_le (Nat.lt_succ_self i) hi) hsz) :: acc)
-
-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.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).toList = acc.toList ++ as := by
-  induction as generalizing acc <;> simp [*, List.toArrayAux, Array.push, List.append_assoc, List.concat_eq_append]
-
-@[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, 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.toList i ((id (α := as.toList.length = n) h₁) ▸ h₂) :=
-    rfl
-
-  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 :=
   if h : i < as.size then
     let a := as[i]
@@ -832,7 +768,6 @@ def isPrefixOfAux [BEq α] (as bs : Array α) (hle : as.size ≤ bs.size) (i : N
       false
   else
     true
-termination_by as.size - i
 decreasing_by simp_wf; decreasing_trivial_pre_omega
 
 /-- Return true iff `as` is a prefix of `bs`.
@@ -843,23 +778,6 @@ def isPrefixOf [BEq α] (as bs : Array α) : Bool :=
   else
     false
 
-private def allDiffAuxAux [BEq α] (as : Array α) (a : α) : forall (i : Nat), i < as.size → Bool
-  | 0,   _ => true
-  | i+1, h =>
-    have : i < as.size := Nat.lt_trans (Nat.lt_succ_self _) h;
-    a != as[i] && allDiffAuxAux as a i this
-
-private def allDiffAux [BEq α] (as : Array α) (i : Nat) : Bool :=
-  if h : i < as.size then
-    allDiffAuxAux as as[i] i h && allDiffAux as (i+1)
-  else
-    true
-termination_by as.size - i
-decreasing_by simp_wf; decreasing_trivial_pre_omega
-
-def allDiff [BEq α] (as : Array α) : Bool :=
-  allDiffAux as 0
-
 @[specialize] def zipWithAux (f : α → β → γ) (as : Array α) (bs : Array β) (i : Nat) (cs : Array γ) : Array γ :=
   if h : i < as.size then
     let a := as[i]
@@ -870,7 +788,6 @@ def allDiff [BEq α] (as : Array α) : Bool :=
       cs
   else
     cs
-termination_by as.size - i
 decreasing_by simp_wf; decreasing_trivial_pre_omega
 
 @[inline] def zipWith (as : Array α) (bs : Array β) (f : α → β → γ) : Array γ :=
@@ -886,4 +803,47 @@ def split (as : Array α) (p : α → Bool) : Array α × Array α :=
   as.foldl (init := (#[], #[])) fun (as, bs) a =>
     if p a then (as.push a, bs) else (as, bs.push a)
 
+/-! ### Auxiliary functions used in metaprogramming.
+
+We do not intend to provide verification theorems for these functions.
+-/
+
+private def allDiffAuxAux [BEq α] (as : Array α) (a : α) : forall (i : Nat), i < as.size → Bool
+  | 0,   _ => true
+  | i+1, h =>
+    have : i < as.size := Nat.lt_trans (Nat.lt_succ_self _) h;
+    a != as[i] && allDiffAuxAux as a i this
+
+private def allDiffAux [BEq α] (as : Array α) (i : Nat) : Bool :=
+  if h : i < as.size then
+    allDiffAuxAux as as[i] i h && allDiffAux as (i+1)
+  else
+    true
+decreasing_by simp_wf; decreasing_trivial_pre_omega
+
+def allDiff [BEq α] (as : Array α) : Bool :=
+  allDiffAux as 0
+
+@[inline] def getEvenElems (as : Array α) : Array α :=
+  (·.2) <| as.foldl (init := (true, Array.empty)) fun (even, r) a =>
+    if even then
+      (false, r.push a)
+    else
+      (true, r)
+
+/-! ### Repr and ToString -/
+
+instance {α : Type u} [Repr α] : Repr (Array α) where
+  reprPrec a _ :=
+    let _ : Std.ToFormat α := ⟨repr⟩
+    if a.size == 0 then
+      "#[]"
+    else
+      Std.Format.bracketFill "#[" (Std.Format.joinSep (toList a) ("," ++ Std.Format.line)) "]"
+
+instance [ToString α] : ToString (Array α) where
+  toString a := "#" ++ toString a.toList
+
 end Array
+
+export Array (mkArray)

src/Init/Data/Array/GetLit.lean

@@ -0,0 +1,46 @@
+/-
+Copyright (c) 2018 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+
+prelude
+import Init.Data.Array.Basic
+
+namespace Array
+
+/-! ### getLit -/
+
+-- auxiliary declaration used in the equation compiler when pattern matching array literals.
+abbrev getLit {α : Type u} {n : Nat} (a : Array α) (i : Nat) (h₁ : a.size = n) (h₂ : i < n) : α :=
+  have := h₁.symm ▸ h₂
+  a[i]
+
+theorem extLit {n : Nat}
+    (a b : Array α)
+    (hsz₁ : a.size = n) (hsz₂ : b.size = n)
+    (h : (i : Nat) → (hi : i < n) → a.getLit i hsz₁ hi = b.getLit i hsz₂ hi) : a = b :=
+  Array.ext a b (hsz₁.trans hsz₂.symm) fun i hi₁ _ => h i (hsz₁ ▸ hi₁)
+
+def toListLitAux (a : Array α) (n : Nat) (hsz : a.size = n) : ∀ (i : Nat), i ≤ a.size → List α → List α
+  | 0,     _,  acc => acc
+  | (i+1), hi, acc => toListLitAux a n hsz i (Nat.le_of_succ_le hi) (a.getLit i hsz (Nat.lt_of_lt_of_eq (Nat.lt_of_lt_of_le (Nat.lt_succ_self i) hi) hsz) :: acc)
+
+def toArrayLit (a : Array α) (n : Nat) (hsz : a.size = n) : Array α :=
+  List.toArray <| toListLitAux a n hsz n (hsz ▸ Nat.le_refl _) []
+
+theorem toArrayLit_eq (as : Array α) (n : Nat) (hsz : as.size = n) : as = toArrayLit as n hsz := by
+  apply ext'
+  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.toList i ((id (α := as.toList.length = n) h₁) ▸ h₂) :=
+    rfl
+  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, *]
+
+end Array

src/Init/Data/Array/Lemmas.lean

@@ -271,6 +271,9 @@ termination_by n - i
 
 /-- # mkArray -/
 
+@[simp] theorem size_mkArray (n : Nat) (v : α) : (mkArray n v).size = n :=
+  List.length_replicate ..
+
 @[simp] theorem toList_mkArray (n : Nat) (v : α) : (mkArray n v).toList = List.replicate n v := rfl
 
 @[deprecated toList_mkArray (since := "2024-09-09")]
@@ -495,7 +498,6 @@ abbrev size_eq_length_data := @size_eq_length_toList
   let rec go (as : Array α) (i j) : (reverse.loop as i j).size = as.size := by
     rw [reverse.loop]
     if h : i < j then
-      have := reverse.termination h
       simp [(go · (i+1) ⟨j-1, ·⟩), h]
     else simp [h]
     termination_by j - i
@@ -527,9 +529,8 @@ set_option linter.deprecated false in
       (H : ∀ k, as.toList.get? k = if i ≤ k ∧ k ≤ j then a.toList.get? k else a.toList.reverse.get? k)
       (k) : (reverse.loop as i ⟨j, hj⟩).toList.get? k = a.toList.reverse.get? k := by
     rw [reverse.loop]; dsimp; split <;> rename_i h₁
-    · have p := reverse.termination h₁
-      match j with | j+1 => ?_
-      simp only [Nat.add_sub_cancel] at p ⊢
+    · match j with | j+1 => ?_
+      simp only [Nat.add_sub_cancel]
       rw [(go · (i+1) j)]
       · rwa [Nat.add_right_comm i]
       · simp [size_swap, h₂]
@@ -1113,5 +1114,4 @@ theorem swap_comm (a : Array α) {i j : Fin a.size} : a.swap i j = a.swap j i :=
     · split <;> simp_all
     · split <;> simp_all
 
-
 end Array

src/Init/Data/List/Attach.lean

@@ -308,6 +308,46 @@ theorem getElem_attach {xs : List α} {i : Nat} (h : i < xs.attach.length) :
     xs.attach.tail = xs.tail.attach.map (fun ⟨x, h⟩ => ⟨x, mem_of_mem_tail h⟩) := by
   cases xs <;> simp
 
+theorem foldl_pmap (l : List α) {P : α → Prop} (f : (a : α) → P a → β)
+  (H : ∀ (a : α), a ∈ l → P a) (g : γ → β → γ) (x : γ) :
+    (l.pmap f H).foldl g x = l.attach.foldl (fun acc a => g acc (f a.1 (H _ a.2))) x := by
+  rw [pmap_eq_map_attach, foldl_map]
+
+theorem foldr_pmap (l : List α) {P : α → Prop} (f : (a : α) → P a → β)
+  (H : ∀ (a : α), a ∈ l → P a) (g : β → γ → γ) (x : γ) :
+    (l.pmap f H).foldr g x = l.attach.foldr (fun a acc => g (f a.1 (H _ a.2)) acc) x := by
+  rw [pmap_eq_map_attach, foldr_map]
+
+/--
+If we fold over `l.attach` with a function that ignores the membership predicate,
+we get the same results as folding over `l` directly.
+
+This is useful when we need to use `attach` to show termination.
+
+Unfortunately this can't be applied by `simp` because of the higher order unification problem,
+and even when rewriting we need to specify the function explicitly.
+-/
+theorem foldl_attach (l : List α) (f : β → α → β) (b : β) :
+    l.attach.foldl (fun acc t => f acc t.1) b = l.foldl f b := by
+  induction l generalizing b with
+  | nil => simp
+  | cons a l ih => rw [foldl_cons, attach_cons, foldl_cons, foldl_map, ih]
+
+/--
+If we fold over `l.attach` with a function that ignores the membership predicate,
+we get the same results as folding over `l` directly.
+
+This is useful when we need to use `attach` to show termination.
+
+Unfortunately this can't be applied by `simp` because of the higher order unification problem,
+and even when rewriting we need to specify the function explicitly.
+-/
+theorem foldr_attach (l : List α) (f : α → β → β) (b : β) :
+    l.attach.foldr (fun t acc => f t.1 acc) b = l.foldr f b := by
+  induction l generalizing b with
+  | nil => simp
+  | cons a l ih => rw [foldr_cons, attach_cons, foldr_cons, foldr_map, ih]
+
 theorem attach_map {l : List α} (f : α → β) :
     (l.map f).attach = l.attach.map (fun ⟨x, h⟩ => ⟨f x, mem_map_of_mem f h⟩) := by
   induction l <;> simp [*]

src/Init/Data/List/Lemmas.lean

@@ -1282,16 +1282,11 @@ theorem map_eq_iff : map f l = l' ↔ ∀ i : Nat, l'[i]? = l[i]?.map f := by
 theorem map_eq_foldr (f : α → β) (l : List α) : map f l = foldr (fun a bs => f a :: bs) [] l := by
   induction l <;> simp [*]
 
-@[simp] theorem map_set {f : α → β} {l : List α} {i : Nat} {a : α} :
-    (l.set i a).map f = (l.map f).set i (f a) := by
-  induction l generalizing i with
-  | nil => simp
-  | cons b l ih => cases i <;> simp_all
-
-@[deprecated "Use the reverse direction of `map_set`." (since := "2024-09-20")]
-theorem set_map {f : α → β} {l : List α} {n : Nat} {a : α} :
+@[simp] theorem set_map {f : α → β} {l : List α} {n : Nat} {a : α} :
     (map f l).set n (f a) = map f (l.set n a) := by
-  simp
+  induction l generalizing n with
+  | nil => simp
+  | cons b l ih => cases n <;> simp_all
 
 @[simp] theorem head_map (f : α → β) (l : List α) (w) :
     head (map f l) w = f (head l (by simpa using w)) := by

src/Init/Data/List/Nat/Basic.lean

@@ -119,6 +119,53 @@ theorem minimum?_cons' {a : Nat} {l : List Nat} :
         specialize le b h
         split <;> omega
 
+theorem foldl_min
+    {α : Type _} [Min α] [Std.IdempotentOp (min : α → α → α)] [Std.Associative (min : α → α → α)]
+    {l : List α} {a : α} :
+    l.foldl (init := a) min = min a (l.minimum?.getD a) := by
+  cases l with
+  | nil => simp [Std.IdempotentOp.idempotent]
+  | cons b l =>
+    simp only [minimum?]
+    induction l generalizing a b with
+    | nil => simp
+    | cons c l ih => simp [ih, Std.Associative.assoc]
+
+theorem foldl_min_right {α β : Type _}
+    [Min β] [Std.IdempotentOp (min : β → β → β)] [Std.Associative (min : β → β → β)]
+    {l : List α} {b : β} {f : α → β} :
+    (l.foldl (init := b) fun acc a => min acc (f a)) = min b ((l.map f).minimum?.getD b) := by
+  rw [← foldl_map, foldl_min]
+
+theorem foldl_min_le {l : List Nat} {a : Nat} : l.foldl (init := a) min ≤ a := by
+  induction l generalizing a with
+  | nil => simp
+  | cons c l ih =>
+    simp only [foldl_cons]
+    exact Nat.le_trans ih (Nat.min_le_left _ _)
+
+theorem foldl_min_min_of_le {l : List Nat} {a b : Nat} (h : a ≤ b) :
+    l.foldl (init := a) min ≤ b :=
+  Nat.le_trans (foldl_min_le) h
+
+theorem minimum?_getD_le_of_mem {l : List Nat} {a k : Nat} (h : a ∈ l) :
+    l.minimum?.getD k ≤ a := by
+  cases l with
+  | nil => simp at h
+  | cons b l =>
+    simp [minimum?_cons]
+    simp at h
+    rcases h with (rfl | h)
+    · exact foldl_min_le
+    · induction l generalizing b with
+      | nil => simp_all
+      | cons c l ih =>
+        simp only [foldl_cons]
+        simp at h
+        rcases h with (rfl | h)
+        · exact foldl_min_min_of_le (Nat.min_le_right _ _)
+        · exact ih _ h
+
 /-! ### maximum? -/
 
 -- A specialization of `maximum?_eq_some_iff` to Nat.
@@ -152,4 +199,51 @@ theorem maximum?_cons' {a : Nat} {l : List Nat} :
         specialize le b h
         split <;> omega
 
+theorem foldl_max
+    {α : Type _} [Max α] [Std.IdempotentOp (max : α → α → α)] [Std.Associative (max : α → α → α)]
+    {l : List α} {a : α} :
+    l.foldl (init := a) max = max a (l.maximum?.getD a) := by
+  cases l with
+  | nil => simp [Std.IdempotentOp.idempotent]
+  | cons b l =>
+    simp only [maximum?]
+    induction l generalizing a b with
+    | nil => simp
+    | cons c l ih => simp [ih, Std.Associative.assoc]
+
+theorem foldl_max_right {α β : Type _}
+    [Max β] [Std.IdempotentOp (max : β → β → β)] [Std.Associative (max : β → β → β)]
+    {l : List α} {b : β} {f : α → β} :
+    (l.foldl (init := b) fun acc a => max acc (f a)) = max b ((l.map f).maximum?.getD b) := by
+  rw [← foldl_map, foldl_max]
+
+theorem le_foldl_max {l : List Nat} {a : Nat} : a ≤ l.foldl (init := a) max := by
+  induction l generalizing a with
+  | nil => simp
+  | cons c l ih =>
+    simp only [foldl_cons]
+    exact Nat.le_trans (Nat.le_max_left _ _) ih
+
+theorem le_foldl_max_of_le {l : List Nat} {a b : Nat} (h : a ≤ b) :
+    a ≤ l.foldl (init := b) max :=
+  Nat.le_trans h (le_foldl_max)
+
+theorem le_maximum?_getD_of_mem {l : List Nat} {a k : Nat} (h : a ∈ l) :
+    a ≤ l.maximum?.getD k := by
+  cases l with
+  | nil => simp at h
+  | cons b l =>
+    simp [maximum?_cons]
+    simp at h
+    rcases h with (rfl | h)
+    · exact le_foldl_max
+    · induction l generalizing b with
+      | nil => simp_all
+      | cons c l ih =>
+        simp only [foldl_cons]
+        simp at h
+        rcases h with (rfl | h)
+        · exact le_foldl_max_of_le (Nat.le_max_right b a)
+        · exact ih _ h
+
 end List

src/Init/Meta.lean

@@ -7,7 +7,7 @@ Additional goodies for writing macros
 -/
 prelude
 import Init.MetaTypes
-import Init.Data.Array.Basic
+import Init.Data.Array.GetLit
 import Init.Data.Option.BasicAux
 
 namespace Lean

src/Init/Tactics.lean

@@ -773,8 +773,9 @@ macro_rules
 macro "refine_lift' " e:term : tactic => `(tactic| focus (refine' no_implicit_lambda% $e; rotate_right))
 /-- Similar to `have`, but using `refine'` -/
 macro "have' " d:haveDecl : tactic => `(tactic| refine_lift' have $d:haveDecl; ?_)
-/-- Similar to `have`, but using `refine'` -/
+set_option linter.missingDocs false in -- OK, because `tactic_alt` causes inheritance of docs
 macro (priority := high) "have'" x:ident " := " p:term : tactic => `(tactic| have' $x:ident : _ := $p)
+attribute [tactic_alt tacticHave'_] «tacticHave'_:=_»
 /-- Similar to `let`, but using `refine'` -/
 macro "let' " d:letDecl : tactic => `(tactic| refine_lift' let $d:letDecl; ?_)
 

src/Lean/Elab/InfoTree/Main.lean

@@ -183,7 +183,7 @@ def UserWidgetInfo.format (info : UserWidgetInfo) : Format :=
   f!"UserWidget {info.id}\n{Std.ToFormat.format <| info.props.run' {}}"
 
 def FVarAliasInfo.format (info : FVarAliasInfo) : Format :=
-  f!"FVarAlias {info.userName.eraseMacroScopes}"
+  f!"FVarAlias {info.userName.eraseMacroScopes}: {info.id.name} -> {info.baseId.name}"
 
 def FieldRedeclInfo.format (ctx : ContextInfo) (info : FieldRedeclInfo) : Format :=
   f!"FieldRedecl @ {formatStxRange ctx info.stx}"

src/Lean/Linter/UnusedVariables.lean

@@ -447,7 +447,10 @@ def unusedVariables : Linter where
     let fvarAliases : Std.HashMap FVarId FVarId := s.fvarAliases.fold (init := {}) fun m id baseId =>
       m.insert id (followAliases s.fvarAliases baseId)
 
+    let getCanonVar (id : FVarId) : FVarId := fvarAliases.getD id id
+
     -- Collect all non-alias fvars corresponding to `fvarUses` by resolving aliases in the list.
+    -- Unlike `s.fvarUses`, `fvarUsesRef` is guaranteed to contain no aliases.
     let fvarUsesRef ← IO.mkRef <| fvarAliases.fold (init := s.fvarUses) fun fvarUses id baseId =>
       if fvarUses.contains id then fvarUses.insert baseId else fvarUses
 
@@ -461,7 +464,7 @@ def unusedVariables : Linter where
       let fvarUses ← fvarUsesRef.get
       -- If any of the `fvar`s corresponding to this declaration is (an alias of) a variable in
       -- `fvarUses`, then it is used
-      if aliases.any fun id => fvarUses.contains (fvarAliases.getD id id) then continue
+      if aliases.any fun id => fvarUses.contains (getCanonVar id) then continue
       -- If this is a global declaration then it is (potentially) used after the command
       if s.constDecls.contains range then continue
 
@@ -493,10 +496,12 @@ def unusedVariables : Linter where
       if !initializedMVars then
         -- collect additional `fvarUses` from tactic assignments
         visitAssignments (← IO.mkRef {}) fvarUsesRef s.assignments
+        -- Resolve potential aliases again to preserve `fvarUsesRef` invariant
+        fvarUsesRef.modify fun fvarUses => fvarUses.fold (·.insert <| getCanonVar ·) {}
         initializedMVars := true
         let fvarUses ← fvarUsesRef.get
         -- Redo the initial check because `fvarUses` could be bigger now
-        if aliases.any fun id => fvarUses.contains (fvarAliases.getD id id) then continue
+        if aliases.any fun id => fvarUses.contains (getCanonVar id) then continue
 
       -- If we made it this far then the variable is unused and not ignored
       unused := unused.push (declStx, userName)

tests/lean/1018unknowMVarIssue.lean.expected.out

@@ -55,8 +55,8 @@ a : α
         • Fam2.any : Fam2 α α @ ⟨9, 4⟩†-⟨9, 12⟩†
           • α : Type @ ⟨9, 4⟩†-⟨9, 12⟩†
         • a (isBinder := true) : α @ ⟨8, 2⟩†-⟨10, 19⟩†
-        • FVarAlias a
-        • FVarAlias α
+        • FVarAlias a: _uniq.636 -> _uniq.312
+        • FVarAlias α: _uniq.635 -> _uniq.310
         • ?m x α a : α @ ⟨9, 18⟩-⟨9, 19⟩ @ Lean.Elab.Term.elabHole
         • [.] Fam2.nat : none @ ⟨10, 4⟩-⟨10, 12⟩
         • Fam2.nat : Nat → Fam2 Nat Nat @ ⟨10, 4⟩-⟨10, 12⟩
@@ -70,8 +70,8 @@ a : α
         • Fam2.nat n : Fam2 Nat Nat @ ⟨10, 4⟩†-⟨10, 14⟩
           • n (isBinder := true) : Nat @ ⟨10, 13⟩-⟨10, 14⟩
         • a (isBinder := true) : Nat @ ⟨8, 2⟩†-⟨10, 19⟩†
-        • FVarAlias a
-        • FVarAlias n
+        • FVarAlias a: _uniq.667 -> _uniq.312
+        • FVarAlias n: _uniq.666 -> _uniq.310
         • n : Nat @ ⟨10, 18⟩-⟨10, 19⟩ @ Lean.Elab.Term.elabIdent
           • [.] n : some Nat @ ⟨10, 18⟩-⟨10, 19⟩
           • n : Nat @ ⟨10, 18⟩-⟨10, 19⟩

tests/lean/linterUnusedVariables.lean

@@ -250,6 +250,17 @@ example [ord : Ord β] (f : α → β) (x y : α) : Ordering := compare (f x) (f
 example {α β} [ord : Ord β] (f : α → β) (x y : α) : Ordering := compare (f x) (f y)
 example {h : Decidable True} (t e : α) : ite True t e = t := if_pos trivial
 
+inductive A where
+  | intro : Nat → A
+
+def A.out : A → Nat
+  | .intro n => n
+
+/-! `h` is used indirectly via an alias introduced by `match` that is used only via the mvar ctx -/
+theorem problematicAlias (n : A) (i : Nat) (h : i ≤ n.out) : i ≤ n.out :=
+  match n with
+  | .intro _ => by assumption
+
 /-!
 The wildcard pattern introduces a copy of `x` that should not be linted as it is in an
 inaccessible annotation.