script to count libraries by toolchain

script/count_versions.sh

@@ -0,0 +1,21 @@
+#!/bin/bash
+# Must be run in a copy of the `lean4` repository, and you'll need to login with `gh auth` first.
+for v in $(gh release list | cut -f1) nightly stable
+do
+  sleep 15 # Don't exceed API rate limits!
+  echo -n $v" "
+  count=$(gh search code --filename lean-toolchain -L 1000 "leanprover/lean4:$v" | wc -l)
+  
+  # Check if version number begins with a 'v'
+  if [[ $v == v* ]]; then
+    sleep 5 # Don't exceed API rate limits!
+    # Remove the leading 'v'
+    v_no_v=${v:1}
+    count_no_v=$(gh search code --filename lean-toolchain -L 1000 "leanprover/lean4:$v_no_v" | wc -l)
+    # Sum the two counts
+    total_count=$(($count + $count_no_v))
+    echo $total_count
+  else
+    echo $count
+  fi
+done | awk '{ printf "%-12s %s\n", $1, $2 }'

script/plot_count_versions.py

@@ -0,0 +1,50 @@
+import matplotlib.pyplot as plt
+import pandas as pd
+import numpy as np
+import sys
+from io import StringIO
+
+# Reading data from stdin
+input_data = sys.stdin.read()
+
+# Using StringIO to simulate a file-like object for pandas
+data_io = StringIO(input_data)
+
+# Reading data into DataFrame
+df = pd.read_csv(data_io, sep="\s+", names=['Version', 'Count'])
+
+# Splitting versions into prefix and suffix
+df['Prefix'] = df['Version'].apply(lambda x: x.split('-')[0])
+df['Suffix'] = df['Version'].apply(lambda x: '-'.join(x.split('-')[1:]) if '-' in x else '')
+
+# Grouping and summing by prefix
+grouped = df.groupby('Prefix').sum().reset_index()
+
+# Setting the color map
+color_map = {'': 'blue'}  # Default color for versions without suffix
+suffixes = df['Suffix'].unique()
+greens = plt.cm.Greens(np.linspace(0.3, 0.9, len(suffixes)))
+
+for i, suffix in enumerate(suffixes):
+    if suffix:  # Assign green shades to versions with suffixes
+        color_map[suffix] = greens[i]
+
+# Plotting the bar chart with new color scheme
+plt.figure(figsize=(10, 6))
+for prefix in grouped['Prefix']:
+    subset = df[df['Prefix'] == prefix]
+    bottom = 0
+    for _, row in subset.iterrows():
+        color = color_map[row['Suffix']]
+        plt.bar(prefix, row['Count'], bottom=bottom, label=row['Version'], color=color)
+        bottom += row['Count']
+
+plt.title('Version Contributions with Distinctive Colors')
+plt.xlabel('Version Prefix')
+plt.ylabel('Count')
+plt.xticks(rotation=45)
+plt.legend(title='Version', bbox_to_anchor=(1.05, 1), loc='upper left')
+
+# Save to a file
+output_file_path = 'version_contribution_chart_colored.png'
+plt.savefig(output_file_path)

src/Init/Core.lean

@@ -1382,11 +1382,6 @@ gen_injective_theorems% EStateM.Result
 gen_injective_theorems% Lean.Name
 gen_injective_theorems% Lean.Syntax
 
-/-- Replacement for `Array.mk.injEq`; we avoid mentioning the constructor and prefer `List.toArray`. -/
-abbrev List.toArray_inj := @Array.mk.injEq
-
-attribute [deprecated List.toArray_inj (since := "2024-09-09")] Array.mk.injEq
-
 theorem Nat.succ.inj {m n : Nat} : m.succ = n.succ → m = n :=
   fun x => Nat.noConfusion x id
 

src/Init/Data/Array/Basic.lean

@@ -162,16 +162,19 @@ instance : Inhabited (Array α) where
 @[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) (_ : i ≤ a.size), Bool
-  | 0, _ => true
-  | i+1, h =>
-    p a[i] (b[i]'(hsz ▸ h)) && isEqvAux a b hsz p i (Nat.le_trans (Nat.le_add_right i 1) h)
+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 a.size (Nat.le_refl a.size)
+    isEqvAux a b h p 0
   else
     false
 
@@ -185,10 +188,9 @@ 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)]` -/
-  @[semireducible] -- This is otherwise irreducible because it uses well-founded recursion.
   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
+decreasing_by simp_wf; decreasing_trivial_pre_omega
 
 /-- The array `#[0, 1, ..., n - 1]`. -/
 def range (n : Nat) : Array Nat :=
@@ -387,12 +389,11 @@ unsafe def mapMUnsafe {α : Type u} {β : Type v} {m : Type v → Type w} [Monad
 def mapM {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (f : α → m β) (as : Array α) : m (Array β) :=
   -- Note: we cannot use `foldlM` here for the reference implementation because this calls
   -- `bind` and `pure` too many times. (We are not assuming `m` is a `LawfulMonad`)
-  let rec @[semireducible] -- This is otherwise irreducible because it uses well-founded recursion.
-    map (i : Nat) (r : Array β) : m (Array β) := do
-      if hlt : i < as.size then
-        map (i+1) (r.push (← f as[i]))
-      else
-        pure r
+  let rec map (i : Nat) (r : Array β) : m (Array β) := do
+    if hlt : i < as.size then
+      map (i+1) (r.push (← f as[i]))
+    else
+      pure r
   decreasing_by simp_wf; decreasing_trivial_pre_omega
   map 0 (mkEmpty as.size)
 
@@ -456,8 +457,7 @@ unsafe def anyMUnsafe {α : Type u} {m : Type → Type w} [Monad m] (p : α →
 @[implemented_by anyMUnsafe]
 def anyM {α : Type u} {m : Type → Type w} [Monad m] (p : α → m Bool) (as : Array α) (start := 0) (stop := as.size) : m Bool :=
   let any (stop : Nat) (h : stop ≤ as.size) :=
-    let rec @[semireducible] -- This is otherwise irreducible because it uses well-founded recursion.
-    loop (j : Nat) : m Bool := do
+    let rec loop (j : Nat) : m Bool := do
       if hlt : j < stop then
         have : j < as.size := Nat.lt_of_lt_of_le hlt h
         if (← p as[j]) then
@@ -547,8 +547,7 @@ def findRev? {α : Type} (as : Array α) (p : α → Bool) : Option α :=
 
 @[inline]
 def findIdx? {α : Type u} (as : Array α) (p : α → Bool) : Option Nat :=
-  let rec @[semireducible] -- This is otherwise irreducible because it uses well-founded recursion.
-  loop (j : Nat) :=
+  let rec loop (j : Nat) :=
     if h : j < as.size then
       if p as[j] then some j else loop (j + 1)
     else none
@@ -558,7 +557,6 @@ def findIdx? {α : Type u} (as : Array α) (p : α → Bool) : Option Nat :=
 def getIdx? [BEq α] (a : Array α) (v : α) : Option Nat :=
   a.findIdx? fun a => a == v
 
-@[semireducible] -- This is otherwise irreducible because it uses well-founded recursion.
 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⟩;
@@ -680,7 +678,6 @@ where
     else
       as
 
-@[semireducible] -- This is otherwise irreducible because it uses well-founded recursion.
 def popWhile (p : α → Bool) (as : Array α) : Array α :=
   if h : as.size > 0 then
     if p (as.get ⟨as.size - 1, Nat.sub_lt h (by decide)⟩) then
@@ -692,8 +689,7 @@ def popWhile (p : α → Bool) (as : Array α) : Array α :=
 decreasing_by simp_wf; decreasing_trivial_pre_omega
 
 def takeWhile (p : α → Bool) (as : Array α) : Array α :=
-  let rec @[semireducible] -- This is otherwise irreducible because it uses well-founded recursion.
-  go (i : Nat) (r : Array α) : Array α :=
+  let rec go (i : Nat) (r : Array α) : Array α :=
     if h : i < as.size then
       let a := as.get ⟨i, h⟩
       if p a then
@@ -709,7 +705,6 @@ def takeWhile (p : α → Bool) (as : Array α) : Array α :=
 
   This function takes worst case O(n) time because
   it has to backshift all elements at positions greater than `i`.-/
-@[semireducible] -- This is otherwise irreducible because it uses well-founded recursion.
 def feraseIdx (a : Array α) (i : Fin a.size) : Array α :=
   if h : i.val + 1 < a.size then
     let a' := a.swap ⟨i.val + 1, h⟩ i
@@ -744,8 +739,7 @@ def erase [BEq α] (as : Array α) (a : α) : Array α :=
 
 /-- Insert element `a` at position `i`. -/
 @[inline] def insertAt (as : Array α) (i : Fin (as.size + 1)) (a : α) : Array α :=
-  let rec @[semireducible] -- This is otherwise irreducible because it uses well-founded recursion.
-  loop (as : Array α) (j : Fin as.size) :=
+  let rec loop (as : Array α) (j : Fin as.size) :=
     if i.1 < j then
       let j' := ⟨j-1, Nat.lt_of_le_of_lt (Nat.pred_le _) j.2⟩
       let as := as.swap j' j
@@ -763,7 +757,6 @@ def insertAt! (as : Array α) (i : Nat) (a : α) : Array α :=
     insertAt as ⟨i, Nat.lt_succ_of_le h⟩ a
   else panic! "invalid index"
 
-@[semireducible] -- This is otherwise irreducible because it uses well-founded recursion.
 def isPrefixOfAux [BEq α] (as bs : Array α) (hle : as.size ≤ bs.size) (i : Nat) : Bool :=
   if h : i < as.size then
     let a := as[i]
@@ -785,8 +778,7 @@ def isPrefixOf [BEq α] (as bs : Array α) : Bool :=
   else
     false
 
-@[semireducible, specialize] -- This is otherwise irreducible because it uses well-founded recursion.
-def zipWithAux (f : α → β → γ) (as : Array α) (bs : Array β) (i : Nat) (cs : Array γ) : Array γ :=
+@[specialize] def zipWithAux (f : α → β → γ) (as : Array α) (bs : Array β) (i : Nat) (cs : Array γ) : Array γ :=
   if h : i < as.size then
     let a := as[i]
     if h : i < bs.size then
@@ -822,7 +814,6 @@ private def allDiffAuxAux [BEq α] (as : Array α) (a : α) : forall (i : Nat),
     have : i < as.size := Nat.lt_trans (Nat.lt_succ_self _) h;
     a != as[i] && allDiffAuxAux as a i this
 
-@[semireducible] -- This is otherwise irreducible because it uses well-founded recursion.
 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)

src/Init/Data/Array/BasicAux.lean

@@ -9,7 +9,7 @@ import Init.Data.Nat.Linear
 import Init.NotationExtra
 
 theorem Array.of_push_eq_push {as bs : Array α} (h : as.push a = bs.push b) : as = bs ∧ a = b := by
-  simp only [push, List.toArray_inj] at h
+  simp only [push, mk.injEq] at h
   have ⟨h₁, h₂⟩ := List.of_concat_eq_concat h
   cases as; cases bs
   simp_all

src/Init/Data/Array/DecidableEq.lean

@@ -9,37 +9,37 @@ import Init.ByCases
 
 namespace Array
 
-theorem eq_of_isEqvAux
-    [DecidableEq α] (a b : Array α) (hsz : a.size = b.size) (i : Nat) (hi : i ≤ a.size)
-    (heqv : Array.isEqvAux a b hsz (fun x y => x = y) i hi)
-    (j : Nat) (hj : j < i) : a[j]'(Nat.lt_of_lt_of_le hj hi) = b[j]'(Nat.lt_of_lt_of_le hj (hsz ▸ hi)) := by
-  induction i with
-  | zero => contradiction
-  | succ i ih =>
-    simp only [Array.isEqvAux, Bool.and_eq_true, decide_eq_true_eq] at heqv
-    by_cases hj' : j < i
-    next =>
-      exact ih _ heqv.right hj'
-    next =>
-      replace hj' : j = i := Nat.eq_of_le_of_lt_succ (Nat.not_lt.mp hj') hj
-      subst hj'
-      exact heqv.left
+theorem eq_of_isEqvAux [DecidableEq α] (a b : Array α) (hsz : a.size = b.size) (i : Nat) (hi : i ≤ a.size) (heqv : Array.isEqvAux a b hsz (fun x y => x = y) i) (j : Nat) (low : i ≤ j) (high : j < a.size) : a[j] = b[j]'(hsz ▸ high) := by
+  by_cases h : i < a.size
+  · unfold Array.isEqvAux at heqv
+    simp [h] at heqv
+    have hind := eq_of_isEqvAux a b hsz (i+1) (Nat.succ_le_of_lt h) heqv.2
+    by_cases heq : i = j
+    · subst heq; exact heqv.1
+    · exact hind j (Nat.succ_le_of_lt (Nat.lt_of_le_of_ne low heq)) high
+  · have heq : i = a.size := Nat.le_antisymm hi (Nat.ge_of_not_lt h)
+    subst heq
+    exact absurd (Nat.lt_of_lt_of_le high low) (Nat.lt_irrefl j)
+termination_by a.size - i
+decreasing_by decreasing_trivial_pre_omega
+
 
 theorem eq_of_isEqv [DecidableEq α] (a b : Array α) : Array.isEqv a b (fun x y => x = y) → a = b := by
   simp [Array.isEqv]
   split
   next hsz =>
    intro h
-   have aux := eq_of_isEqvAux a b hsz a.size (Nat.le_refl ..) h
-   exact ext a b hsz fun i h _ => aux i h
+   have aux := eq_of_isEqvAux a b hsz 0 (Nat.zero_le ..) h
+   exact ext a b hsz fun i h _ => aux i (Nat.zero_le ..) _
   next => intro; contradiction
 
-theorem isEqvAux_self [DecidableEq α] (a : Array α) (i : Nat) (h : i ≤ a.size) :
-    Array.isEqvAux a a rfl (fun x y => x = y) i h = true := by
-  induction i with
-  | zero => simp [Array.isEqvAux]
-  | succ i ih =>
-    simp_all only [isEqvAux, decide_True, Bool.and_self]
+theorem isEqvAux_self [DecidableEq α] (a : Array α) (i : Nat) : Array.isEqvAux a a rfl (fun x y => x = y) i = true := by
+  unfold Array.isEqvAux
+  split
+  next h => simp [h, isEqvAux_self a (i+1)]
+  next h => simp [h]
+termination_by a.size - i
+decreasing_by decreasing_trivial_pre_omega
 
 theorem isEqv_self [DecidableEq α] (a : Array α) : Array.isEqv a a (fun x y => x = y) = true := by
   simp [isEqv, isEqvAux_self]

src/Init/Data/Array/Lemmas.lean

@@ -19,14 +19,24 @@ This file contains some theorems about `Array` and `List` needed for `Init.Data.
 
 namespace Array
 
-/-- We avoid mentioning the constructor `Array.mk` directly, preferring `List.toArray`. -/
-@[simp] theorem mk_eq_toArray (as : List α) : Array.mk as = as.toArray := by
-  apply ext'
-  simp
+attribute [simp] uset
 
-@[simp] theorem getElem_toList {a : Array α} {i : Nat} (h : i < a.size) : a.toList[i] = a[i] := rfl
+@[simp] theorem singleton_def (v : α) : singleton v = #[v] := rfl
 
-@[simp] theorem getElem_mk {xs : List α} {i : Nat} (h : i < xs.length) : (Array.mk xs)[i] = xs[i] := rfl
+@[simp] theorem toArray_toList : (a : Array α) → a.toList.toArray = a
+  | ⟨l⟩ => ext' (toList_toArray l)
+
+@[deprecated toArray_toList (since := "2024-09-09")]
+abbrev toArray_data := @toArray_toList
+
+@[simp] theorem toList_length {l : Array α} : l.toList.length = l.size := rfl
+
+@[deprecated toList_length (since := "2024-09-09")]
+abbrev data_length := @toList_length
+
+@[simp] theorem mkEmpty_eq (α n) : @mkEmpty α n = #[] := rfl
+
+@[simp] theorem size_mk (as : List α) : (Array.mk as).size = as.length := by simp [size]
 
 theorem getElem_eq_toList_getElem (a : Array α) (h : i < a.size) : a[i] = a.toList[i] := by
   by_cases i < a.size <;> (try simp [*]) <;> rfl
@@ -36,7 +46,27 @@ abbrev getElem_eq_data_getElem := @getElem_eq_toList_getElem
 
 @[deprecated getElem_eq_toList_getElem (since := "2024-06-12")]
 theorem getElem_eq_toList_get (a : Array α) (h : i < a.size) : a[i] = a.toList.get ⟨i, h⟩ := by
-  simp
+  simp [getElem_eq_toList_getElem]
+
+theorem foldrM_push [Monad m] (f : α → β → m β) (init : β) (arr : Array α) (a : α) :
+    (arr.push a).foldrM f init = f a init >>= arr.foldrM f := by
+  simp [foldrM_eq_reverse_foldlM_toList, -size_push]
+
+@[simp] theorem foldrM_push' [Monad m] (f : α → β → m β) (init : β) (arr : Array α) (a : α) :
+    (arr.push a).foldrM f init (start := arr.size + 1) = f a init >>= arr.foldrM f := by
+  simp [← foldrM_push]
+
+theorem foldr_push (f : α → β → β) (init : β) (arr : Array α) (a : α) :
+    (arr.push a).foldr f init = arr.foldr f (f a init) := foldrM_push ..
+
+@[simp] theorem foldr_push' (f : α → β → β) (init : β) (arr : Array α) (a : α) :
+    (arr.push a).foldr f init (start := arr.size + 1) = arr.foldr f (f a init) := foldrM_push' ..
+
+/-- A more efficient version of `arr.toList.reverse`. -/
+@[inline] def toListRev (arr : Array α) : List α := arr.foldl (fun l t => t :: l) []
+
+@[simp] theorem toListRev_eq (arr : Array α) : arr.toListRev = arr.toList.reverse := by
+  rw [toListRev, foldl_eq_foldl_toList, ← List.foldr_reverse, List.foldr_cons_nil]
 
 theorem get_push_lt (a : Array α) (x : α) (i : Nat) (h : i < a.size) :
     have : i < (a.push x).size := by simp [*, Nat.lt_succ_of_le, Nat.le_of_lt]
@@ -54,78 +84,6 @@ theorem get_push (a : Array α) (x : α) (i : Nat) (h : i < (a.push x).size) :
   · simp at h
     simp [get_push_lt, Nat.le_antisymm (Nat.le_of_lt_succ h) (Nat.ge_of_not_lt h')]
 
-end Array
-
-namespace List
-
-open Array
-
-/-! ### Lemmas about `List.toArray`. -/
-
-@[simp] theorem toArray_size (as : List α) : as.toArray.size = as.length := by simp [size]
-
-@[simp] theorem toArrayAux_size {a : List α} {b : Array α} :
-    (a.toArrayAux b).size = b.size + a.length := by
-  simp [size]
-
-@[simp] theorem toArray_toList : (a : Array α) → a.toList.toArray = a
-  | ⟨l⟩ => ext' (toList_toArray l)
-
-@[simp] theorem getElem_toArray {a : List α} {i : Nat} (h : i < a.toArray.size) :
-    a.toArray[i] = a[i]'(by simpa using h) := by
-  have h₁ := mk_eq_toArray a
-  have h₂ := getElem_mk (by simpa using h)
-  simpa [h₁] using h₂
-
-@[simp] theorem toArray_concat {as : List α} {x : α} :
-    (as ++ [x]).toArray = as.toArray.push x := by
-  apply ext'
-  simp
-
-end List
-
-namespace Array
-
-attribute [simp] uset
-
-@[simp] theorem singleton_def (v : α) : singleton v = #[v] := rfl
-
-@[deprecated List.toArray_toList (since := "2024-09-09")]
-abbrev toArray_data := @List.toArray_toList
-@[deprecated List.toArray_toList (since := "2024-09-09")]
-abbrev toArray_toList := @List.toArray_toList
-
-@[simp] theorem toList_length {l : Array α} : l.toList.length = l.size := rfl
-
-@[deprecated toList_length (since := "2024-09-09")]
-abbrev data_length := @toList_length
-
-@[simp] theorem mkEmpty_eq (α n) : @mkEmpty α n = #[] := rfl
-
-@[simp] theorem size_mk (as : List α) : (Array.mk as).size = as.length := by simp [size]
-
-theorem foldrM_push [Monad m] (f : α → β → m β) (init : β) (arr : Array α) (a : α) :
-    (arr.push a).foldrM f init = f a init >>= arr.foldrM f := by
-  simp [foldrM_eq_reverse_foldlM_toList, -size_push]
-
-/-- Variant of `foldrM_push` with the `start := arr.size + 1` rather than `(arr.push a).size`. -/
-@[simp] theorem foldrM_push' [Monad m] (f : α → β → m β) (init : β) (arr : Array α) (a : α) :
-    (arr.push a).foldrM f init (start := arr.size + 1) = f a init >>= arr.foldrM f := by
-  simp [← foldrM_push]
-
-theorem foldr_push (f : α → β → β) (init : β) (arr : Array α) (a : α) :
-    (arr.push a).foldr f init = arr.foldr f (f a init) := foldrM_push ..
-
-/-- Variant of `foldr_push` with the `start := arr.size + 1` rather than `(arr.push a).size`. -/
-@[simp] theorem foldr_push' (f : α → β → β) (init : β) (arr : Array α) (a : α) :
-    (arr.push a).foldr f init (start := arr.size + 1) = arr.foldr f (f a init) := foldrM_push' ..
-
-/-- A more efficient version of `arr.toList.reverse`. -/
-@[inline] def toListRev (arr : Array α) : List α := arr.foldl (fun l t => t :: l) []
-
-@[simp] theorem toListRev_eq (arr : Array α) : arr.toListRev = arr.toList.reverse := by
-  rw [toListRev, foldl_eq_foldl_toList, ← List.foldr_reverse, List.foldr_cons_nil]
-
 theorem mapM_eq_foldlM [Monad m] [LawfulMonad m] (f : α → m β) (arr : Array α) :
     arr.mapM f = arr.foldlM (fun bs a => bs.push <$> f a) #[] := by
   rw [mapM, aux, foldlM_eq_foldlM_toList]; rfl
@@ -387,7 +345,7 @@ theorem getElem_mem_toList (a : Array α) (h : i < a.size) : a[i] ∈ a.toList :
 abbrev getElem_mem_data := @getElem_mem_toList
 
 theorem getElem?_eq_toList_get? (a : Array α) (i : Nat) : a[i]? = a.toList.get? i := by
-  by_cases i < a.size <;> simp_all [getElem?_pos, getElem?_neg, List.get?_eq_get, eq_comm]
+  by_cases i < a.size <;> simp_all [getElem?_pos, getElem?_neg, List.get?_eq_get, eq_comm]; rfl
 
 @[deprecated getElem?_eq_toList_get? (since := "2024-09-09")]
 abbrev getElem?_eq_data_get? := @getElem?_eq_toList_get?
@@ -647,12 +605,12 @@ theorem foldr_induction
   simp only [mem_def, map_toList, List.mem_map]
 
 theorem mapM_eq_mapM_toList [Monad m] [LawfulMonad m] (f : α → m β) (arr : Array α) :
-    arr.mapM f = return (← arr.toList.mapM f).toArray := by
+    arr.mapM f = return mk (← arr.toList.mapM f) := by
   rw [mapM_eq_foldlM, foldlM_eq_foldlM_toList, ← List.foldrM_reverse]
   conv => rhs; rw [← List.reverse_reverse arr.toList]
   induction arr.toList.reverse with
-  | nil => simp
-  | cons a l ih => simp [ih]; simp [map_eq_pure_bind]
+  | nil => simp; rfl
+  | cons a l ih => simp [ih]; simp [map_eq_pure_bind, push]
 
 @[deprecated mapM_eq_mapM_toList (since := "2024-09-09")]
 abbrev mapM_eq_mapM_data := @mapM_eq_mapM_toList

src/Init/Data/Array/TakeDrop.lean

@@ -12,7 +12,6 @@ namespace Array
 theorem exists_of_uset (self : Array α) (i d h) :
     ∃ l₁ l₂, self.toList = l₁ ++ self[i] :: l₂ ∧ List.length l₁ = i.toNat ∧
       (self.uset i d h).toList = l₁ ++ d :: l₂ := by
-  simpa only [ugetElem_eq_getElem, getElem_eq_toList_getElem, uset, toList_set] using
-    List.exists_of_set _
+  simpa [Array.getElem_eq_toList_getElem] using List.exists_of_set _
 
 end Array

src/Init/Data/List/Lemmas.lean

@@ -1314,16 +1314,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/Repr.lean

@@ -51,12 +51,6 @@ instance [Repr α] : Repr (id α) :=
 instance [Repr α] : Repr (Id α) :=
   inferInstanceAs (Repr α)
 
-/-
-This instance allows us to use `Empty` as a type parameter without causing instance synthesis to fail.
--/
-instance : Repr Empty where
-  reprPrec := nofun
-
 instance : Repr Bool where
   reprPrec
     | true, _  => "true"
@@ -163,7 +157,7 @@ protected def _root_.USize.repr (n : @& USize) : String :=
 
 /-- We statically allocate and memoize reprs for small natural numbers. -/
 private def reprArray : Array String := Id.run do
-  List.range 128 |>.map (·.toUSize.repr) |> List.toArray
+  List.range 128 |>.map (·.toUSize.repr) |> Array.mk
 
 private def reprFast (n : Nat) : String :=
   if h : n < 128 then Nat.reprArray.get ⟨n, h⟩ else

src/Init/Prelude.lean

@@ -2709,10 +2709,7 @@ def Array.extract (as : Array α) (start stop : Nat) : Array α :=
   let sz' := Nat.sub (min stop as.size) start
   loop sz' start (mkEmpty sz')
 
-/--
-Auxiliary definition for `List.toArray`.
-`List.toArrayAux as r = r ++ as.toArray`
--/
+/-- Auxiliary definition for `List.toArray`. -/
 @[inline_if_reduce]
 def List.toArrayAux : List α → Array α → Array α
   | nil,       r => r

src/Lean/Compiler/LCNF/Simp/ConstantFold.lean

@@ -180,7 +180,7 @@ let _x.26 := @Array.push _ _x.24 z
 def foldArrayLiteral : Folder := fun args => do
   let #[_, .fvar fvarId] := args | return none
   let some (list, typ, level) ← getPseudoListLiteral fvarId | return none
-  let arr := list.toArray
+  let arr := Array.mk list
   let lit ← mkPseudoArrayLiteral arr typ level
   return some lit
 

src/Lean/Elab/PatternVar.lean

@@ -156,11 +156,9 @@ private def processVar (idStx : Syntax) : M Syntax := do
   modify fun s => { s with vars := s.vars.push idStx, found := s.found.insert id }
   return idStx
 
-private def samePatternsVariables (startingAt : Nat) (s₁ s₂ : State) : Bool := Id.run do
-  if h₁ : s₁.vars.size = s₂.vars.size then
-    for h₂ : i in [startingAt:s₁.vars.size] do
-      if s₁.vars[i] != s₂.vars[i]'(by obtain ⟨_, y⟩ := h₂; simp_all) then return false
-    true
+private def samePatternsVariables (startingAt : Nat) (s₁ s₂ : State) : Bool :=
+  if h : s₁.vars.size = s₂.vars.size then
+    Array.isEqvAux s₁.vars s₂.vars h (.==.) startingAt
   else
     false
 

src/Std/Tactic/BVDecide/LRAT/Internal/Convert.lean

@@ -61,7 +61,7 @@ theorem CNF.Clause.mem_lrat_of_mem (clause : CNF.Clause (PosFin n)) (h1 : l ∈
   | nil => cases h1
   | cons hd tl ih =>
     unfold DefaultClause.ofArray at h2
-    rw [Array.foldr_eq_foldr_toList, List.toArray_toList] at h2
+    rw [Array.foldr_eq_foldr_toList, Array.toArray_toList] at h2
     dsimp only [List.foldr] at h2
     split at h2
     · cases h2
@@ -77,7 +77,7 @@ theorem CNF.Clause.mem_lrat_of_mem (clause : CNF.Clause (PosFin n)) (h1 : l ∈
             · assumption
             · next heq _ _ =>
               unfold DefaultClause.ofArray
-              rw [Array.foldr_eq_foldr_toList, List.toArray_toList]
+              rw [Array.foldr_eq_foldr_toList, Array.toArray_toList]
               exact heq
         · cases h1
           · simp only [← Option.some.inj h2]
@@ -89,7 +89,7 @@ theorem CNF.Clause.mem_lrat_of_mem (clause : CNF.Clause (PosFin n)) (h1 : l ∈
             apply ih
             assumption
             unfold DefaultClause.ofArray
-            rw [Array.foldr_eq_foldr_toList, List.toArray_toList]
+            rw [Array.foldr_eq_foldr_toList, Array.toArray_toList]
             exact heq
 
 theorem CNF.Clause.convertLRAT_sat_of_sat (clause : CNF.Clause (PosFin n))

src/Std/Tactic/BVDecide/LRAT/Internal/Formula/Lemmas.lean

@@ -500,7 +500,8 @@ theorem deleteOne_preserves_strongAssignmentsInvariant {n : Nat} (f : DefaultFor
             · next id_eq_idx =>
               exfalso
               have idx_in_bounds2 : idx < f.clauses.size := by
-                conv => rhs; rw [Array.size_mk]
+                have f_clauses_rw : f.clauses = { toList := f.clauses.toList } := rfl
+                conv => rhs; rw [f_clauses_rw, Array.size_mk]
                 exact hbound
               simp only [getElem!, id_eq_idx, Array.toList_length, idx_in_bounds2, ↓reduceDIte,
                 Fin.eta, Array.get_eq_getElem, Array.getElem_eq_toList_getElem, decidableGetElem?] at heq
@@ -533,7 +534,8 @@ theorem deleteOne_preserves_strongAssignmentsInvariant {n : Nat} (f : DefaultFor
             · next id_eq_idx =>
               exfalso
               have idx_in_bounds2 : idx < f.clauses.size := by
-                conv => rhs; rw [Array.size_mk]
+                have f_clauses_rw : f.clauses = { toList := f.clauses.toList } := rfl
+                conv => rhs; rw [f_clauses_rw, Array.size_mk]
                 exact hbound
               simp only [getElem!, id_eq_idx, Array.toList_length, idx_in_bounds2, ↓reduceDIte,
                 Fin.eta, Array.get_eq_getElem, Array.getElem_eq_toList_getElem, decidableGetElem?] at heq
@@ -593,7 +595,8 @@ theorem deleteOne_preserves_strongAssignmentsInvariant {n : Nat} (f : DefaultFor
             · next id_eq_idx =>
               exfalso
               have idx_in_bounds2 : idx < f.clauses.size := by
-                conv => rhs; rw [Array.size_mk]
+                have f_clauses_rw : f.clauses = { toList := f.clauses.toList } := rfl
+                conv => rhs; rw [f_clauses_rw, Array.size_mk]
                 exact hbound
               simp only [getElem!, id_eq_idx, Array.toList_length, idx_in_bounds2, ↓reduceDIte,
                 Fin.eta, Array.get_eq_getElem, Array.getElem_eq_toList_getElem, decidableGetElem?] at heq

src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddResult.lean

@@ -1112,7 +1112,7 @@ theorem nodup_derivedLits {n : Nat} (f : DefaultFormula n)
     (derivedLits : CNF.Clause (PosFin n))
     (derivedLits_satisfies_invariant:
       DerivedLitsInvariant f f_assignments_size (performRupCheck f rupHints).fst.assignments f'_assignments_size derivedLits)
-    (derivedLits_arr : Array (Literal (PosFin n))) (derivedLits_arr_def : derivedLits_arr = { toList := derivedLits })
+    (derivedLits_arr : Array (Literal (PosFin n))) (derivedLits_arr_def: derivedLits_arr = { toList := derivedLits })
     (i j : Fin (Array.size derivedLits_arr)) (i_ne_j : i ≠ j) :
     derivedLits_arr[i] ≠ derivedLits_arr[j] := by
   intro li_eq_lj

src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddSound.lean

@@ -543,8 +543,8 @@ theorem reduce_fold_fn_preserves_induction_motive {c_arr : Array (Literal (PosFi
 theorem reduce_postcondition {n : Nat} (c : DefaultClause n) (assignment : Array Assignment) :
     (reduce c assignment = reducedToEmpty → Incompatible (PosFin n) c assignment) ∧
     (∀ l : Literal (PosFin n), reduce c assignment = reducedToUnit l → ∀ (p : (PosFin n) → Bool), p ⊨ assignment → p ⊨ c → p ⊨ l) := by
-  let c_arr := c.clause.toArray
-  have c_clause_rw : c.clause = c_arr.toList := by simp [c_arr]
+  let c_arr := Array.mk c.clause
+  have c_clause_rw : c.clause = c_arr.toList := rfl
   rw [reduce, c_clause_rw, ← Array.foldl_eq_foldl_toList]
   let motive := ReducePostconditionInductionMotive c_arr assignment
   have h_base : motive 0 reducedToEmpty := by

tests/lean/run/2670.lean

@@ -12,12 +12,12 @@ def enumFromTR' (n : Nat) (l : List α) : List (Nat × α) :=
 
 open List in
 theorem enumFrom_eq_enumFromTR' : @enumFrom = @enumFromTR' := by
-  funext α n l; simp only [enumFromTR']
+  funext α n l; simp [enumFromTR', -Array.size_toArray]
   let f := fun (a : α) (n, acc) => (n-1, (n-1, a) :: acc)
   let rec go : ∀ l n, l.foldr f (n + l.length, []) = (n, enumFrom n l)
     | [], n => rfl
     | a::as, n => by
       rw [← show _ + as.length = n + (a::as).length from Nat.succ_add .., List.foldr, go as]
       simp [enumFrom, f]
-  rw [Array.foldr_eq_foldr_toList]
+  rw [Array.foldr_eq_foldr_data]
   simp [go] -- Should close the goal

tests/lean/run/array_isEqvAux.lean

@@ -1,45 +0,0 @@
-
-/-!
-Because `Array.isEqvAux` was defined by well-founded recursion, this used to fail with
-```
-tactic 'decide' failed for proposition
-  #[0, 1] = #[0, 1]
-since its 'Decidable' instance
-  #[0, 1].instDecidableEq #[0, 1]
-did not reduce to 'isTrue' or 'isFalse'.
-
-After unfolding the instances 'instDecidableEqNat', 'Array.instDecidableEq' and 'Nat.decEq', reduction got stuck at the 'Decidable' instance
-  match h : #[0, 1].isEqv #[0, 1] fun a b => decide (a = b) with
-  | true => isTrue ⋯
-  | false => isFalse ⋯
-```
--/
-
-example : #[0, 1] = #[0, 1] := by decide
-
-/-!
-There are other `Array` functions that use well-founded recursion,
-which we've marked as `@[semireducible]`. We test that `decide` can unfold them here.
--/
-
-example : Array.ofFn (id : Fin 2 → Fin 2) = #[0, 1] := by decide
-
-example : #[0, 1].map (· + 1) = #[1, 2] := by decide
-
-example : #[0, 1].any (· % 2 = 0) := by decide
-
-example : #[0, 1].findIdx? (· % 2 = 0) = some 0 := by decide
-
-example : #[0, 1, 2].popWhile (· % 2 = 0) = #[0, 1] := by decide
-
-example : #[0, 1, 2].takeWhile (· % 2 = 0) = #[0] := by decide
-
-example : #[0, 1, 2].feraseIdx ⟨1, by decide⟩ = #[0, 2] := by decide
-
-example : #[0, 1, 2].insertAt ⟨1, by decide⟩ 3 = #[0, 3, 1, 2] := by decide
-
-example : #[0, 1, 2].isPrefixOf #[0, 1, 2, 3] = true := by decide
-
-example : #[0, 1, 2].zipWith #[3, 4, 5] (· + ·) = #[3, 5, 7] := by decide
-
-example : #[0, 1, 2].allDiff = true := by decide

tests/lean/run/overAndPartialAppsAtWF.lean

@@ -1,17 +1,7 @@
-@[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
-
-theorem eq_of_isEqvAux [DecidableEq α] (a b : Array α) (hsz : a.size = b.size) (i : Nat) (hi : i ≤ a.size) (heqv : isEqvAux a b hsz (fun x y => x = y) i) : ∀ (j : Nat) (hl : i ≤ j) (hj : j < a.size), a.get ⟨j, hj⟩ = b.get ⟨j, hsz ▸ hj⟩ := by
+theorem eq_of_isEqvAux [DecidableEq α] (a b : Array α) (hsz : a.size = b.size) (i : Nat) (hi : i ≤ a.size) (heqv : Array.isEqvAux a b hsz (fun x y => x = y) i) : ∀ (j : Nat) (hl : i ≤ j) (hj : j < a.size), a.get ⟨j, hj⟩ = b.get ⟨j, hsz ▸ hj⟩ := by
   intro j low high
   by_cases h : i < a.size
-  · unfold isEqvAux at heqv
+  · unfold Array.isEqvAux at heqv
     simp [h] at heqv
     have hind := eq_of_isEqvAux a b hsz (i+1) (Nat.succ_le_of_lt h) heqv.2
     by_cases heq : i = j

tests/lean/run/repr_empty.lean

@@ -1,29 +0,0 @@
-/-!
-# Validation of `Repr Empty` instance
-
-While it may seem unnecessary to have Repr, it prevents the automatic derivation
-of Repr for other types when `Empty` is used as a type parameter.
-
-This is a simplified version of an example from the "Functional Programming in Lean" book.
-The Empty type is used to exlude the `other` constructor from the `Prim` type.
--/
-
-inductive Prim (special : Type) where
-  | plus
-  | minus
-  | other : special → Prim special
-deriving Repr
-
-/-!
-Check that both Repr's work
--/
-
-/-- info: Prim.plus -/
-#guard_msgs in
-open Prim in
-#eval (plus : Prim Int)
-
-/-- info: Prim.minus -/
-#guard_msgs in
-open Prim in
-#eval (minus : Prim Empty)