chore: deprecate Array.get

fix test

src/Init/Data/Array/Bootstrap.lean

@@ -15,6 +15,29 @@ This file contains some theorems about `Array` and `List` needed for `Init.Data.
 
 namespace Array
 
+/--
+Use the indexing notation `a[i]` instead.
+
+Access an element from an array without needing a runtime bounds checks,
+using a `Nat` index and a proof that it is in bounds.
+
+This function does not use `get_elem_tactic` to automatically find the proof that
+the index is in bounds. This is because the tactic itself needs to look up values in
+arrays.
+-/
+@[deprecated "Use indexing notation `as[i]` instead" (since := "2025-02-17")]
+def get {α : Type u} (a : @& Array α) (i : @& Nat) (h : LT.lt i a.size) : α :=
+  a.toList.get ⟨i, h⟩
+
+/--
+Use the indexing notation `a[i]!` instead.
+
+Access an element from an array, or panic if the index is out of bounds.
+-/
+@[deprecated "Use indexing notation `as[i]!` instead" (since := "2025-02-17")]
+def get! {α : Type u} [Inhabited α] (a : @& Array α) (i : @& Nat) : α :=
+  Array.getD a i default
+
 theorem foldlM_toList.aux [Monad m]
     (f : β → α → m β) (arr : Array α) (i j) (H : arr.size ≤ i + j) (b) :
     foldlM.loop f arr arr.size (Nat.le_refl _) i j b = (arr.toList.drop j).foldlM f b := by

src/Init/Data/Array/Lemmas.lean

@@ -3239,22 +3239,23 @@ theorem getElem?_len_le (a : Array α) {i : Nat} (h : a.size ≤ i) : a[i]? = no
 @[deprecated getD_getElem? (since := "2024-12-11")] abbrev getD_get? := @getD_getElem?
 
 @[simp] theorem getD_eq_getD_getElem? (a : Array α) (i d) : a.getD i d = a[i]?.getD d := by
-  simp only [getD, get_eq_getElem]; split <;> simp [getD_getElem?, *]
+  simp only [getD]; split <;> simp [getD_getElem?, *]
 
 @[deprecated getD_eq_getD_getElem? (since := "2025-02-12")] abbrev getD_eq_get? := @getD_eq_getD_getElem?
 
 theorem getElem!_eq_getD [Inhabited α] (a : Array α) : a[i]! = a.getD i default := by
-  simp only [← get!_eq_getElem!]
   rfl
 
+set_option linter.deprecated false in
 @[deprecated getElem!_eq_getD (since := "2025-02-12")]
 theorem get!_eq_getD [Inhabited α] (a : Array α) : a.get! n = a.getD n default := rfl
 
+set_option linter.deprecated false in
 @[deprecated "Use `a[i]!` instead of `a.get! i`." (since := "2025-02-12")]
 theorem get!_eq_getD_getElem? [Inhabited α] (a : Array α) (i : Nat) :
     a.get! i = a[i]?.getD default := by
   by_cases p : i < a.size <;>
-  simp only [get!_eq_getElem!, getElem!_eq_getD, getD_eq_getD_getElem?, getD_getElem?, p]
+  simp [get!, getElem!_eq_getD, getD_eq_getD_getElem?, getD_getElem?, p]
 
 set_option linter.deprecated false in
 @[deprecated get!_eq_getD_getElem? (since := "2025-02-12")] abbrev get!_eq_getElem? := @get!_eq_getD_getElem?
@@ -3573,7 +3574,7 @@ theorem map_spec (as : Array α) (f : α → β) (p : Fin as.size → β → Pro
 
 theorem getElem_modify {as : Array α} {x i} (h : i < (as.modify x f).size) :
     (as.modify x f)[i] = if x = i then f (as[i]'(by simpa using h)) else as[i]'(by simpa using h) := by
-  simp only [modify, modifyM, get_eq_getElem, Id.run, Id.pure_eq]
+  simp only [modify, modifyM, Id.run, Id.pure_eq]
   split
   · simp only [Id.bind_eq, get_set _ _ _ _ (by simpa using h)]; split <;> simp [*]
   · rw [if_neg (mt (by rintro rfl; exact h) (by simp_all))]

src/Init/Data/Array/Mem.lean

@@ -14,7 +14,7 @@ theorem sizeOf_lt_of_mem [SizeOf α] {as : Array α} (h : a ∈ as) : sizeOf a <
   cases as with | _ as =>
   exact Nat.lt_trans (List.sizeOf_lt_of_mem h.val) (by simp +arith)
 
-theorem sizeOf_get [SizeOf α] (as : Array α) (i : Nat) (h : i < as.size) : sizeOf (as.get i h) < sizeOf as := by
+theorem sizeOf_get [SizeOf α] (as : Array α) (i : Nat) (h : i < as.size) : sizeOf as[i] < sizeOf as := by
   cases as with | _ as =>
   simpa using Nat.lt_trans (List.sizeOf_get _ ⟨i, h⟩) (by simp +arith)
 

src/Init/Data/FloatArray/Basic.lean

@@ -47,7 +47,7 @@ def uget : (a : @& FloatArray) → (i : USize) → i.toNat < a.size → Float
 
 @[extern "lean_float_array_fget"]
 def get : (ds : @& FloatArray) → (i : @& Nat) → (h : i < ds.size := by get_elem_tactic) → Float
-  | ⟨ds⟩, i, h => ds.get i h
+  | ⟨ds⟩, i, h => ds[i]
 
 @[extern "lean_float_array_get"]
 def get! : (@& FloatArray) → (@& Nat) → Float

src/Init/Data/List/Notation.lean

@@ -49,7 +49,7 @@ macro_rules
       match i, skip with
       | 0,   _     => pure result
       | i+1, true  => expandListLit i false result
-      | i+1, false => expandListLit i true  (← ``(List.cons $(⟨elems.elemsAndSeps.get! i⟩) $result))
+      | i+1, false => expandListLit i true  (← ``(List.cons $(⟨elems.elemsAndSeps.get!Internal i⟩) $result))
     let size := elems.elemsAndSeps.size
     if size < 64 then
       expandListLit size (size % 2 == 0) (← ``(List.nil))

src/Init/Data/List/ToArray.lean

@@ -68,7 +68,7 @@ theorem toArray_cons (a : α) (l : List α) : (a :: l).toArray = #[a] ++ l.toArr
 @[simp] theorem toArray_singleton (a : α) : (List.singleton a).toArray = Array.singleton a := rfl
 
 @[simp] theorem back!_toArray [Inhabited α] (l : List α) : l.toArray.back! = l.getLast! := by
-  simp only [back!, size_toArray, Array.get!_eq_getElem!, getElem!_toArray, getLast!_eq_getElem!]
+  simp only [back!, size_toArray, getElem!_toArray, getLast!_eq_getElem!]
 
 @[simp] theorem back?_toArray (l : List α) : l.toArray.back? = l.getLast? := by
   simp [back?, List.getLast?_eq_getElem?]
@@ -460,7 +460,7 @@ theorem zipWithAll_go_toArray (as : List α) (bs : List β) (f : Option α → O
 theorem takeWhile_go_succ (p : α → Bool) (a : α) (l : List α) (i : Nat) :
     takeWhile.go p (a :: l).toArray (i+1) r = takeWhile.go p l.toArray i r := by
   rw [takeWhile.go, takeWhile.go]
-  simp only [size_toArray, length_cons, Nat.add_lt_add_iff_right, Array.get_eq_getElem,
+  simp only [size_toArray, length_cons, Nat.add_lt_add_iff_right,
     getElem_toArray, getElem_cons_succ]
   split
   rw [takeWhile_go_succ]
@@ -477,7 +477,7 @@ theorem takeWhile_go_toArray (p : α → Bool) (l : List α) (i : Nat) :
       simp [takeWhile_go_succ, ih, takeWhile_cons]
       split <;> simp
     | succ i =>
-      simp only [size_toArray, length_cons, Nat.add_lt_add_iff_right, Array.get_eq_getElem,
+      simp only [size_toArray, length_cons, Nat.add_lt_add_iff_right,
         getElem_toArray, getElem_cons_succ, drop_succ_cons]
       split <;> rename_i h₁
       · rw [takeWhile_go_succ, ih]

src/Init/Data/Repr.lean

@@ -162,7 +162,7 @@ private def reprArray : Array String := Id.run do
   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
+  if h : n < 128 then Nat.reprArray.getInternal n h else
   if h : n < USize.size then (USize.ofNatLT n h).repr
   else (toDigits 10 n).asString
 

src/Init/GetElem.lean

@@ -313,26 +313,28 @@ end List
 namespace Array
 
 instance : GetElem (Array α) Nat α fun xs i => i < xs.size where
-  getElem xs i h := xs.get i h
+  getElem xs i h := xs.getInternal i h
 
 -- We provide a `GetElem?` instance, rather than using the low priority instance,
--- so that we use the `@[extern]` definition of `get!`.
+-- so that we use the `@[extern]` definition of `get!Internal`.
 instance : GetElem? (Array α) Nat α fun xs i => i < xs.size where
   getElem? xs i := decidableGetElem? xs i
-  getElem! xs i := xs.get! i
+  getElem! xs i := xs.get!Internal i
 
 instance : LawfulGetElem (Array α) Nat α fun xs i => i < xs.size where
   getElem?_def xs i h := by
     simp only [getElem?, decidableGetElem?]
     split <;> rfl
   getElem!_def xs i := by
-    simp only [getElem!, getElem?, decidableGetElem?, get!, getD, getElem]
+    simp only [getElem!, getElem?, decidableGetElem?, get!Internal, getD, getElem]
     split <;> rfl
 
-@[simp] theorem get_eq_getElem (a : Array α) (i : Nat) (h) : a.get i h = a[i] := rfl
+@[simp] theorem getInternal_eq_getElem (a : Array α) (i : Nat) (h) :
+    a.getInternal i h = a[i] := rfl
 
-@[simp] theorem get!_eq_getElem! [Inhabited α] (a : Array α) (i : Nat) : a.get! i = a[i]! := by
-  simp only [get!, getD, get_eq_getElem, getElem!_def]
+@[simp] theorem get!Internal_eq_getElem! [Inhabited α] (a : Array α) (i : Nat) :
+    a.get!Internal i = a[i]! := by
+  simp only [get!Internal, getD, getInternal_eq_getElem, getElem!_def]
   split <;> simp_all [getElem?_pos, getElem?_neg]
 
 end Array

src/Init/Prelude.lean

@@ -2673,12 +2673,12 @@ the index is in bounds. This is because the tactic itself needs to look up value
 arrays.
 -/
 @[extern "lean_array_fget"]
-def Array.get {α : Type u} (a : @& Array α) (i : @& Nat) (h : LT.lt i a.size) : α :=
+def Array.getInternal {α : Type u} (a : @& Array α) (i : @& Nat) (h : LT.lt i a.size) : α :=
   a.toList.get ⟨i, h⟩
 
 /-- Access an element from an array, or return `v₀` if the index is out of bounds. -/
 @[inline] abbrev Array.getD (a : Array α) (i : Nat) (v₀ : α) : α :=
-  dite (LT.lt i a.size) (fun h => a.get i h) (fun _ => v₀)
+  dite (LT.lt i a.size) (fun h => a.getInternal i h) (fun _ => v₀)
 
 /--
 Use the indexing notation `a[i]!` instead.
@@ -2686,7 +2686,7 @@ Use the indexing notation `a[i]!` instead.
 Access an element from an array, or panic if the index is out of bounds.
 -/
 @[extern "lean_array_get"]
-def Array.get! {α : Type u} [Inhabited α] (a : @& Array α) (i : @& Nat) : α :=
+def Array.get!Internal {α : Type u} [Inhabited α] (a : @& Array α) (i : @& Nat) : α :=
   Array.getD a i default
 
 /--
@@ -2740,7 +2740,7 @@ protected def Array.appendCore {α : Type u}  (as : Array α) (bs : Array α) :
       (fun hlt =>
         match i with
         | 0           => as
-        | Nat.succ i' => loop i' (hAdd j 1) (as.push (bs.get j hlt)))
+        | Nat.succ i' => loop i' (hAdd j 1) (as.push (bs.getInternal j hlt)))
       (fun _ => as)
   loop bs.size 0 as
 
@@ -2755,7 +2755,7 @@ def Array.extract (as : Array α) (start : Nat := 0) (stop : Nat := as.size) : A
       (fun hlt =>
         match i with
         | 0           => bs
-        | Nat.succ i' => loop i' (hAdd j 1) (bs.push (as.get j hlt)))
+        | Nat.succ i' => loop i' (hAdd j 1) (bs.push (as.getInternal j hlt)))
       (fun _ => bs)
   let sz' := Nat.sub (min stop as.size) start
   loop sz' start (mkEmpty sz')
@@ -3958,7 +3958,7 @@ if it parsed something and `none` otherwise.
 def getOptional? (stx : Syntax) : Option Syntax :=
   match stx with
   | Syntax.node _ k args => match and (beq k nullKind) (beq args.size 1) with
-    | true  => some (args.get! 0)
+    | true  => some (args.get!Internal 0)
     | false => none
   | _                    => none
 
@@ -3995,7 +3995,7 @@ partial def getHeadInfo? : Syntax → Option SourceInfo
   | node SourceInfo.none _ args   =>
     let rec loop (i : Nat) : Option SourceInfo :=
       match decide (LT.lt i args.size) with
-      | true => match getHeadInfo? (args.get! i) with
+      | true => match getHeadInfo? (args.get!Internal i) with
          | some info => some info
          | none      => loop (hAdd i 1)
       | false => none
@@ -4036,7 +4036,7 @@ partial def getTailPos? (stx : Syntax) (canonicalOnly := false) : Option String.
   | node _ _ args, _ =>
     let rec loop (i : Nat) : Option String.Pos :=
       match decide (LT.lt i args.size) with
-      | true => match getTailPos? (args.get! ((args.size.sub i).sub 1)) canonicalOnly with
+      | true => match getTailPos? (args.get!Internal ((args.size.sub i).sub 1)) canonicalOnly with
          | some info => some info
          | none      => loop (hAdd i 1)
       | false => none

src/Std/Data/DHashMap/Internal/WF.lean

@@ -215,7 +215,7 @@ theorem expand.go_eq [BEq α] [Hashable α] [PartialEquivBEq α] (source : Array
     simp only [newSource, newTarget, es] at *
     rw [expand.go_pos hi]
     refine ih.trans ?_
-    simp only [Array.get_eq_getElem, AssocList.foldl_eq, Array.toList_set]
+    simp only [AssocList.foldl_eq, Array.toList_set]
     rw [List.drop_eq_getElem_cons hi, List.flatMap_cons, List.foldl_append,
       List.drop_set_of_lt _ _ (by omega), Array.getElem_toList]
   · next i source target hi =>

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

@@ -529,7 +529,7 @@ theorem clear_insert_inductive_case {n : Nat} (f : DefaultFormula n) (f_assignme
     ⟨j1, j1_ge_idx, j2, j2_ge_idx, i_gt_zero, ih1, ih2, ih3, ih4, ih5⟩
   · apply Or.inl
     constructor
-    · simp only [clearUnit, Fin.getElem_fin, Array.get_eq_getElem]
+    · simp only [clearUnit, Array.getInternal_eq_getElem]
       specialize ih2 idx (Nat.le_refl idx.val)
       have i_in_bounds : i.1 < assignments.size := by
         rw [hsize]
@@ -544,7 +544,7 @@ theorem clear_insert_inductive_case {n : Nat} (f : DefaultFormula n) (f_assignme
     · next idx_eq_j =>
       apply Or.inl
       constructor
-      · simp only [clearUnit, idx_eq_j, Array.get_eq_getElem, ih1]
+      · simp only [clearUnit, idx_eq_j, Array.getInternal_eq_getElem, ih1]
         rw [Array.getElem_modify_self, ih2, remove_add_cancel]
         exact ih3
       · intro k k_ge_idx_add_one
@@ -564,7 +564,7 @@ theorem clear_insert_inductive_case {n : Nat} (f : DefaultFormula n) (f_assignme
       · constructor
         · exact ih1
         · constructor
-          · simp only [clearUnit, Array.get_eq_getElem]
+          · simp only [clearUnit, Array.getInternal_eq_getElem]
             specialize ih4 idx (Nat.le_refl idx.1) idx_ne_j
             rw [Array.getElem_modify_of_ne ih4]
             exact ih2
@@ -589,7 +589,7 @@ theorem clear_insert_inductive_case {n : Nat} (f : DefaultFormula n) (f_assignme
         · simp only [Fin.getElem_fin]
           exact ih2
         · constructor
-          · simp only [clearUnit, idx_eq_j1, Array.get_eq_getElem, ih1]
+          · simp only [clearUnit, idx_eq_j1, Array.getInternal_eq_getElem, ih1]
             rw [Array.getElem_modify_self, ih3, ih4]
             decide
           · constructor
@@ -625,7 +625,7 @@ theorem clear_insert_inductive_case {n : Nat} (f : DefaultFormula n) (f_assignme
           · simp only [Fin.getElem_fin]
             exact ih1
           · constructor
-            · simp only [clearUnit, idx_eq_j2, Array.get_eq_getElem, ih2]
+            · simp only [clearUnit, idx_eq_j2, Array.getInternal_eq_getElem, ih2]
               rw [Array.getElem_modify_self, ih3, ih4]
               decide
             · constructor
@@ -669,7 +669,7 @@ theorem clear_insert_inductive_case {n : Nat} (f : DefaultFormula n) (f_assignme
               · simp only [Fin.getElem_fin]
                 exact ih2
               · constructor
-                · simp only [clearUnit, Array.get_eq_getElem]
+                · simp only [clearUnit, Array.getInternal_eq_getElem]
                   have idx_res_ne_i : units[idx.1].1.1 ≠ i.1 := by
                     intro h1
                     by_cases units[idx.1].2

src/Std/Time/Date/Unit/Month.lean

@@ -242,8 +242,8 @@ def days (leap : Bool) (month : Ordinal) : Day.Ordinal :=
   else
     let ⟨months, p⟩ := monthSizesNonLeap
     let index : Fin 12 := (month.sub 1).toFin (by decide)
-    let idx := (index.cast (by rw [p]))
-    months.get idx.val idx.isLt
+    let idx : Fin months.size := index.cast (by rw [p])
+    months[idx]
 
 theorem days_gt_27 (leap : Bool) (i : Month.Ordinal) : days leap i > 27 := by
   match i with
@@ -262,7 +262,7 @@ def cumulativeDays (leap : Bool) (month : Ordinal) : Day.Offset := by
   let ⟨months, p⟩ := cumulativeSizes
   let index : Fin 12 := (month.sub 1).toFin (by decide)
   rw [← p] at index
-  let res := months.get index.val index.isLt
+  let res := months[index]
   exact res + (if leap ∧ month.val > 2 then 1 else 0)
 
 theorem cumulativeDays_le (leap : Bool) (month : Month.Ordinal) : cumulativeDays leap month ≥ 0 ∧ cumulativeDays leap month ≤ 334 + (if leap then 1 else 0) := by

tests/lean/simpArrayIdx.lean

@@ -9,8 +9,8 @@ variable (j_lt : j < (a.set! i v).size)
 
 #check_simp (i + 0) ~> i
 
-#check_simp (a.set! i v).get i g ~> v
-#check_simp (a.set! i v).get! i ~> (a.setIfInBounds i v)[i]!
+#check_simp (a.set! i v)[i] ~> v
+#check_simp (a.set! i v)[i]! ~> (a.setIfInBounds i v)[i]!
 #check_simp (a.set! i v).getD i d ~> if i < a.size then v else d
 #check_simp (a.set! i v)[i] ~> v