fix: make Array.size not reducible (#8513)

This PR removes the `@[reducible]` annotation on `Array.size`. This is
probably best gone anyway in order to keep separation between the `List`
and `Array` APIs, but it also helps avoid uselessly instantiating
`Array` theorems when `grind` is working on `List` problems.

Author: kim-em

src/Init/Data/Array/Basic.lean

@@ -91,7 +91,8 @@ theorem ext' {xs ys : Array α} (h : xs.toList = ys.toList) : xs = ys := by
 @[simp, grind =] theorem getElem_toList {xs : Array α} {i : Nat} (h : i < xs.size) : xs.toList[i] = xs[i] := rfl
 
 @[simp, grind =] theorem getElem?_toList {xs : Array α} {i : Nat} : xs.toList[i]? = xs[i]? := by
-  simp [getElem?_def]
+  simp only [getElem?_def, getElem_toList]
+  simp only [Array.size]
 
 /-- `a ∈ as` is a predicate which asserts that `a` is in the array `as`. -/
 -- NB: This is defined as a structure rather than a plain def so that a lemma

src/Init/Data/Array/Bootstrap.lean

@@ -78,7 +78,8 @@ theorem foldrM_eq_reverse_foldlM_toList [Monad m] {f : α → β → m β} {init
   have : xs = #[] ∨ 0 < xs.size :=
     match xs with | ⟨[]⟩ => .inl rfl | ⟨a::l⟩ => .inr (Nat.zero_lt_succ _)
   match xs, this with | _, .inl rfl => simp [foldrM] | xs, .inr h => ?_
-  simp [foldrM, h, ← foldrM_eq_reverse_foldlM_toList.aux, List.take_length]
+  simp only [foldrM, h, ← foldrM_eq_reverse_foldlM_toList.aux]
+  simp [Array.size]
 
 @[simp, grind =] theorem foldrM_toList [Monad m]
     {f : α → β → m β} {init : β} {xs : Array α} :

src/Init/Data/Array/Count.lean

@@ -105,6 +105,7 @@ theorem boole_getElem_le_countP {xs : Array α} {i : Nat} (h : i < xs.size) :
 theorem countP_set {xs : Array α} {i : Nat} {a : α} (h : i < xs.size) :
     (xs.set i a).countP p = xs.countP p - (if p xs[i] then 1 else 0) + (if p a then 1 else 0) := by
   rcases xs with ⟨xs⟩
+  simp at h
   simp [List.countP_set, h]
 
 theorem countP_filter {xs : Array α} :

src/Init/Data/Array/DecidableEq.lean

@@ -69,7 +69,7 @@ theorem isEqv_eq_decide (xs ys : Array α) (r) :
     simpa [isEqv_iff_rel] using h'
 
 @[simp, grind =] theorem isEqv_toList [BEq α] (xs ys : Array α) : (xs.toList.isEqv ys.toList r) = (xs.isEqv ys r) := by
-  simp [isEqv_eq_decide, List.isEqv_eq_decide]
+  simp [isEqv_eq_decide, List.isEqv_eq_decide, Array.size]
 
 theorem eq_of_isEqv [DecidableEq α] (xs ys : Array α) (h : Array.isEqv xs ys (fun x y => x = y)) : xs = ys := by
   have ⟨h, h'⟩ := rel_of_isEqv h
@@ -100,7 +100,7 @@ theorem beq_eq_decide [BEq α] (xs ys : Array α) :
   simp [BEq.beq, isEqv_eq_decide]
 
 @[simp, grind =] theorem beq_toList [BEq α] (xs ys : Array α) : (xs.toList == ys.toList) = (xs == ys) := by
-  simp [beq_eq_decide, List.beq_eq_decide]
+  simp [beq_eq_decide, List.beq_eq_decide, Array.size]
 
 end Array
 

src/Init/Data/Array/Find.lean

@@ -655,21 +655,22 @@ theorem findFinIdx?_append {xs ys : Array α} {p : α → Bool} :
 theorem isSome_findFinIdx? {xs : Array α} {p : α → Bool} :
     (xs.findFinIdx? p).isSome = xs.any p := by
   rcases xs with ⟨xs⟩
-  simp
+  simp [Array.size]
 
 @[simp]
 theorem isNone_findFinIdx? {xs : Array α} {p : α → Bool} :
     (xs.findFinIdx? p).isNone = xs.all (fun x => ¬ p x) := by
   rcases xs with ⟨xs⟩
-  simp
+  simp [Array.size]
 
 @[simp] theorem findFinIdx?_subtype {p : α → Prop} {xs : Array { x // p x }}
     {f : { x // p x } → Bool} {g : α → Bool} (hf : ∀ x h, f ⟨x, h⟩ = g x) :
     xs.findFinIdx? f = (xs.unattach.findFinIdx? g).map (fun i => i.cast (by simp)) := by
   cases xs
   simp only [List.findFinIdx?_toArray, hf, List.findFinIdx?_subtype]
   rw [findFinIdx?_congr List.unattach_toArray]
-  simp [Function.comp_def]
+  simp only [Option.map_map, Function.comp_def, Fin.cast_trans]
+  simp [Array.size]
 
 /-! ### idxOf
 
@@ -733,18 +734,19 @@ theorem finIdxOf?_empty [BEq α] : (#[] : Array α).finIdxOf? a = none := by sim
 @[simp] theorem finIdxOf?_eq_none_iff [BEq α] [LawfulBEq α] {xs : Array α} {a : α} :
     xs.finIdxOf? a = none ↔ a ∉ xs := by
   rcases xs with ⟨xs⟩
-  simp [List.finIdxOf?_eq_none_iff]
+  simp [List.finIdxOf?_eq_none_iff, Array.size]
 
 @[simp] theorem finIdxOf?_eq_some_iff [BEq α] [LawfulBEq α] {xs : Array α} {a : α} {i : Fin xs.size} :
     xs.finIdxOf? a = some i ↔ xs[i] = a ∧ ∀ j (_ : j < i), ¬xs[j] = a := by
   rcases xs with ⟨xs⟩
+  unfold Array.size at i ⊢
   simp [List.finIdxOf?_eq_some_iff]
 
 @[simp]
 theorem isSome_finIdxOf? [BEq α] [LawfulBEq α] {xs : Array α} {a : α} :
     (xs.finIdxOf? a).isSome ↔ a ∈ xs := by
   rcases xs with ⟨xs⟩
-  simp
+  simp [Array.size]
 
 theorem isNone_finIdxOf? [BEq α] [LawfulBEq α] {xs : Array α} {a : α} :
     (xs.finIdxOf? a).isNone = ¬ a ∈ xs := by

src/Init/Data/Array/InsertIdx.lean

@@ -44,6 +44,7 @@ theorem insertIdx_zero {xs : Array α} {x : α} : xs.insertIdx 0 x = #[x] ++ xs
 
 @[simp] theorem size_insertIdx {xs : Array α} (h : i ≤ xs.size) : (xs.insertIdx i a).size = xs.size + 1 := by
   rcases xs with ⟨xs⟩
+  simp at h
   simp [List.length_insertIdx, h]
 
 theorem eraseIdx_insertIdx {i : Nat} {xs : Array α} (h : i ≤ xs.size) :

src/Init/Data/Array/Lemmas.lean

@@ -75,7 +75,7 @@ theorem ne_empty_of_size_pos (h : 0 < xs.size) : xs ≠ #[] := by
   cases xs
   simpa using List.ne_nil_of_length_pos h
 
-theorem size_eq_zero_iff : xs.size = 0 ↔ xs = #[] :=
+@[simp] theorem size_eq_zero_iff : xs.size = 0 ↔ xs = #[] :=
   ⟨eq_empty_of_size_eq_zero, fun h => h ▸ rfl⟩
 
 @[deprecated size_eq_zero_iff (since := "2025-02-24")]
@@ -169,6 +169,7 @@ theorem getD_getElem? {xs : Array α} {i : Nat} {d : α} :
 theorem getElem_push_lt {xs : Array α} {x : α} {i : Nat} (h : i < xs.size) :
     have : i < (xs.push x).size := by simp [*, Nat.lt_succ_of_le, Nat.le_of_lt]
     (xs.push x)[i] = xs[i] := by
+  rw [Array.size] at h
   simp only [push, ← getElem_toList, List.concat_eq_append, List.getElem_append_left, h]
 
 @[simp] theorem getElem_push_eq {xs : Array α} {x : α} : (xs.push x)[xs.size] = x := by
@@ -1858,7 +1859,7 @@ theorem getElem_append_right {xs ys : Array α} {h : i < (xs ++ ys).size} (hle :
     (xs ++ ys)[i] = ys[i - xs.size]'(Nat.sub_lt_left_of_lt_add hle (size_append .. ▸ h)) := by
   simp only [← getElem_toList]
   have h' : i < (xs.toList ++ ys.toList).length := by rwa [← length_toList, toList_append] at h
-  conv => rhs; rw [← List.getElem_append_right (h₁ := hle) (h₂ := h')]
+  conv => rhs; unfold Array.size; rw [← List.getElem_append_right (h₁ := hle) (h₂ := h')]
   apply List.get_of_eq; rw [toList_append]
 
 theorem getElem?_append_left {xs ys : Array α} {i : Nat} (hn : i < xs.size) :
@@ -2025,7 +2026,7 @@ theorem append_eq_append_iff {ws xs ys zs : Array α} :
         xs ++ ys.set (i - xs.size) x (by simp at h; omega) := by
   rcases xs with ⟨s⟩
   rcases ys with ⟨t⟩
-  simp only [List.append_toArray, List.set_toArray, List.set_append]
+  simp only [List.append_toArray, List.set_toArray, List.set_append, Array.size]
   split <;> simp
 
 @[simp] theorem set_append_left {xs ys : Array α} {i : Nat} {x : α} (h : i < xs.size)  :
@@ -2045,7 +2046,7 @@ theorem append_eq_append_iff {ws xs ys zs : Array α} :
         xs ++ ys.setIfInBounds (i - xs.size) x := by
   rcases xs with ⟨s⟩
   rcases ys with ⟨t⟩
-  simp only [List.append_toArray, List.setIfInBounds_toArray, List.set_append]
+  simp only [List.append_toArray, List.setIfInBounds_toArray, List.set_append, Array.size]
   split <;> simp
 
 @[simp] theorem setIfInBounds_append_left {xs ys : Array α} {i : Nat} {x : α} (h : i < xs.size) :
@@ -4500,6 +4501,7 @@ abbrev contains_def [DecidableEq α] {a : α} {xs : Array α} : xs.contains a 
 @[simp] theorem size_zipWith {xs : Array α} {ys : Array β} {f : α → β → γ} :
     (zipWith f xs ys).size = min xs.size ys.size := by
   rw [size_eq_length_toList, toList_zipWith, List.length_zipWith]
+  simp only [Array.size]
 
 @[simp] theorem size_zip {xs : Array α} {ys : Array β} :
     (zip xs ys).size = min xs.size ys.size :=
@@ -4572,7 +4574,7 @@ theorem toListRev_toArray {l : List α} : l.toArray.toListRev = l.reverse := by
   | nil => simp
   | cons a l ih =>
     simp only [foldlM_toArray] at ih
-    rw [size_toArray, mapM'_cons, foldlM_toArray]
+    rw [size_toArray, mapM'_cons]
     simp [ih]
 
 theorem uset_toArray {l : List α} {i : USize} {a : α} {h : i.toNat < l.toArray.size} :

src/Init/Data/Array/MapIdx.lean

@@ -192,15 +192,16 @@ theorem mapFinIdx_empty {f : (i : Nat) → α → (h : i < 0) → β} : mapFinId
 theorem mapFinIdx_eq_ofFn {xs : Array α} {f : (i : Nat) → α → (h : i < xs.size) → β} :
     xs.mapFinIdx f = Array.ofFn fun i : Fin xs.size => f i xs[i] i.2 := by
   cases xs
-  simp [List.mapFinIdx_eq_ofFn]
+  simp only [List.mapFinIdx_toArray, List.mapFinIdx_eq_ofFn, Fin.getElem_fin, List.getElem_toArray]
+  simp [Array.size]
 
 theorem mapFinIdx_append {xs ys : Array α} {f : (i : Nat) → α → (h : i < (xs ++ ys).size) → β} :
     (xs ++ ys).mapFinIdx f =
       xs.mapFinIdx (fun i a h => f i a (by simp; omega)) ++
         ys.mapFinIdx (fun i a h => f (i + xs.size) a (by simp; omega)) := by
   cases xs
   cases ys
-  simp [List.mapFinIdx_append]
+  simp [List.mapFinIdx_append, Array.size]
 
 @[simp]
 theorem mapFinIdx_push {xs : Array α} {a : α} {f : (i : Nat) → α → (h : i < (xs.push a).size) → β} :
@@ -264,12 +265,12 @@ theorem mapFinIdx_eq_append_iff {xs : Array α} {f : (i : Nat) → α → (h : i
     toArray_eq_append_iff]
   constructor
   · rintro ⟨l₁, l₂, rfl, rfl, rfl⟩
-    refine ⟨l₁.toArray, l₂.toArray, by simp_all⟩
+    refine ⟨l₁.toArray, l₂.toArray, by simp_all [Array.size]⟩
   · rintro ⟨⟨l₁⟩, ⟨l₂⟩, rfl, h₁, h₂⟩
     simp [← toList_inj] at h₁ h₂
     obtain rfl := h₁
     obtain rfl := h₂
-    refine ⟨l₁, l₂, by simp_all⟩
+    refine ⟨l₁, l₂, by simp_all [Array.size]⟩
 
 theorem mapFinIdx_eq_push_iff {xs : Array α} {b : β} {f : (i : Nat) → α → (h : i < xs.size) → β} :
     xs.mapFinIdx f = ys.push b ↔
@@ -307,7 +308,7 @@ abbrev mapFinIdx_eq_mkArray_iff := @mapFinIdx_eq_replicate_iff
 @[simp] theorem mapFinIdx_reverse {xs : Array α} {f : (i : Nat) → α → (h : i < xs.reverse.size) → β} :
     xs.reverse.mapFinIdx f = (xs.mapFinIdx (fun i a h => f (xs.size - 1 - i) a (by simp; omega))).reverse := by
   rcases xs with ⟨l⟩
-  simp [List.mapFinIdx_reverse]
+  simp [List.mapFinIdx_reverse, Array.size]
 
 /-! ### mapIdx -/
 
@@ -486,7 +487,7 @@ namespace List
     | x :: xs => simp only [mapFinIdxM.go, mapIdxM.go, go]
   unfold Array.mapIdxM
   rw [mapFinIdxM_toArray]
-  simp only [mapFinIdxM, mapIdxM]
+  simp only [mapFinIdxM, mapIdxM, Array.size]
   rw [go]
 
 end List

src/Init/Data/Array/Monadic.lean

@@ -310,7 +310,7 @@ namespace List
 @[simp] theorem filterM_toArray' [Monad m] [LawfulMonad m] {l : List α} {p : α → m Bool} (w : stop = l.length) :
     l.toArray.filterM p 0 stop = toArray <$> l.filterM p := by
   subst w
-  rw [filterM_toArray]
+  simp [← filterM_toArray]
 
 @[grind =] theorem filterRevM_toArray [Monad m] [LawfulMonad m] {l : List α} {p : α → m Bool} :
     l.toArray.filterRevM p = toArray <$> l.filterRevM p := by
@@ -322,7 +322,7 @@ namespace List
 @[simp] theorem filterRevM_toArray' [Monad m] [LawfulMonad m] {l : List α} {p : α → m Bool} (w : start = l.length) :
     l.toArray.filterRevM p start 0 = toArray <$> l.filterRevM p := by
   subst w
-  rw [filterRevM_toArray]
+  simp [← filterRevM_toArray]
 
 @[grind =] theorem filterMapM_toArray [Monad m] [LawfulMonad m] {l : List α} {f : α → m (Option β)} :
     l.toArray.filterMapM f = toArray <$> l.filterMapM f := by
@@ -340,7 +340,7 @@ namespace List
 @[simp] theorem filterMapM_toArray' [Monad m] [LawfulMonad m] {l : List α} {f : α → m (Option β)} (w : stop = l.length) :
     l.toArray.filterMapM f 0 stop = toArray <$> l.filterMapM f := by
   subst w
-  rw [filterMapM_toArray]
+  simp [← filterMapM_toArray]
 
 @[simp, grind =] theorem flatMapM_toArray [Monad m] [LawfulMonad m] {l : List α} {f : α → m (Array β)} :
     l.toArray.flatMapM f = toArray <$> l.flatMapM (fun a => Array.toList <$> f a) := by

src/Init/Data/List/Impl.lean

@@ -550,7 +550,7 @@ def zipIdxTR (l : List α) (n : Nat := 0) : List (α × Nat) :=
   (as.foldr (fun a (n, acc) => (n-1, (a, n-1) :: acc)) (n + as.size, [])).2
 
 @[csimp] theorem zipIdx_eq_zipIdxTR : @zipIdx = @zipIdxTR := by
-  funext α l n; simp only [zipIdxTR, size_toArray]
+  funext α l n; simp only [zipIdxTR]
   let f := fun (a : α) (n, acc) => (n-1, (a, n-1) :: acc)
   let rec go : ∀ l i, l.foldr f (i + l.length, []) = (i, zipIdx l i)
     | [], n => rfl
@@ -571,7 +571,7 @@ def enumFromTR (n : Nat) (l : List α) : List (Nat × α) :=
 set_option linter.deprecated false in
 @[deprecated zipIdx_eq_zipIdxTR (since := "2025-01-21"), csimp]
 theorem enumFrom_eq_enumFromTR : @enumFrom = @enumFromTR := by
-  funext α n l; simp only [enumFromTR, size_toArray]
+  funext α n l; simp only [enumFromTR]
   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