feat: rename Array.setD to setIfInBounds (#6195)

This PR renames `Array.setD` to `Array.setIfInBounds`.

src/Init/Data/Array/Lemmas.lean

@@ -551,10 +551,10 @@ theorem getElem?_len_le (a : Array α) {i : Nat} (h : a.size ≤ i) : a[i]? = no
 theorem getD_get? (a : Array α) (i : Nat) (d : α) :
   Option.getD a[i]? d = if p : i < a.size then a[i]'p else d := by
   if h : i < a.size then
-    simp [setD, h, getElem?_def]
+    simp [setIfInBounds, h, getElem?_def]
   else
     have p : i ≥ a.size := Nat.le_of_not_gt h
-    simp [setD, getElem?_len_le _ p, h]
+    simp [setIfInBounds, getElem?_len_le _ p, h]
 
 @[simp] theorem getD_eq_get? (a : Array α) (n d) : a.getD n d = (a[n]?).getD d := by
   simp only [getD, get_eq_getElem, get?_eq_getElem?]; split <;> simp [getD_get?, *]
@@ -590,31 +590,32 @@ theorem getElem_set (a : Array α) (i : Nat) (h' : i < a.size) (v : α) (j : Nat
     (ne : i ≠ j) : (a.set i v)[j]? = a[j]? := by
   by_cases h : j < a.size <;> simp [getElem?_lt, getElem?_ge, Nat.ge_of_not_lt, ne, h]
 
-/-! # setD -/
+/-! # setIfInBounds -/
 
-@[simp] theorem set!_is_setD : @set! = @setD := rfl
+@[simp] theorem set!_is_setIfInBounds : @set! = @setIfInBounds := rfl
 
-@[simp] theorem size_setD (a : Array α) (index : Nat) (val : α) :
-    (Array.setD a index val).size = a.size := by
+@[simp] theorem size_setIfInBounds (a : Array α) (index : Nat) (val : α) :
+    (Array.setIfInBounds a index val).size = a.size := by
   if h : index < a.size  then
-    simp [setD, h]
+    simp [setIfInBounds, h]
   else
-    simp [setD, h]
+    simp [setIfInBounds, h]
 
-@[simp] theorem getElem_setD_eq (a : Array α) {i : Nat} (v : α) (h : _) :
-    (setD a i v)[i]'h = v := by
+@[simp] theorem getElem_setIfInBounds_eq (a : Array α) {i : Nat} (v : α) (h : _) :
+    (setIfInBounds a i v)[i]'h = v := by
   simp at h
-  simp only [setD, h, ↓reduceDIte, getElem_set_eq]
+  simp only [setIfInBounds, h, ↓reduceDIte, getElem_set_eq]
 
 @[simp]
-theorem getElem?_setD_eq (a : Array α) {i : Nat} (p : i < a.size) (v : α) : (a.setD i v)[i]? = some v := by
+theorem getElem?_setIfInBounds_eq (a : Array α) {i : Nat} (p : i < a.size) (v : α) :
+    (a.setIfInBounds i v)[i]? = some v := by
   simp [getElem?_lt, p]
 
 /-- Simplifies a normal form from `get!` -/
-@[simp] theorem getD_get?_setD (a : Array α) (i : Nat) (v d : α) :
-    Option.getD (setD a i v)[i]? d = if i < a.size then v else d := by
+@[simp] theorem getD_get?_setIfInBounds (a : Array α) (i : Nat) (v d : α) :
+    Option.getD (setIfInBounds a i v)[i]? d = if i < a.size then v else d := by
   by_cases h : i < a.size <;>
-    simp [setD, Nat.not_lt_of_le, h,  getD_get?]
+    simp [setIfInBounds, Nat.not_lt_of_le, h,  getD_get?]
 
 /-! # ofFn -/
 
@@ -806,10 +807,10 @@ theorem get_set (a : Array α) (i : Nat) (hi : i < a.size) (j : Nat) (hj : j < a
     (h : i ≠ j) : (a.set i v)[j]'(by simp [*]) = a[j] := by
   simp only [set, getElem_eq_getElem_toList, List.getElem_set_ne h]
 
-theorem getElem_setD (a : Array α) (i : Nat) (v : α) (h : i < (setD a i v).size) :
-    (setD a i v)[i] = v := by
+theorem getElem_setIfInBounds (a : Array α) (i : Nat) (v : α) (h : i < (setIfInBounds a i v).size) :
+    (setIfInBounds a i v)[i] = v := by
   simp at h
-  simp only [setD, h, ↓reduceDIte, getElem_set_eq]
+  simp only [setIfInBounds, h, ↓reduceDIte, getElem_set_eq]
 
 theorem set_set (a : Array α) (i : Nat) (h) (v v' : α) :
     (a.set i v h).set i v' (by simp [h]) = a.set i v' := by simp [set, List.set_set]
@@ -1790,10 +1791,10 @@ Our goal is to have `simp` "pull `List.toArray` outwards" as much as possible.
   apply ext'
   simp
 
-@[simp] theorem setD_toArray (l : List α) (i : Nat) (a : α) :
-    l.toArray.setD i a  = (l.set i a).toArray := by
+@[simp] theorem setIfInBounds_toArray (l : List α) (i : Nat) (a : α) :
+    l.toArray.setIfInBounds i a  = (l.set i a).toArray := by
   apply ext'
-  simp only [setD]
+  simp only [setIfInBounds]
   split
   · simp
   · simp_all [List.set_eq_of_length_le]
@@ -2145,6 +2146,8 @@ theorem toArray_concat {as : List α} {x : α} :
 
 @[deprecated back!_toArray (since := "2024-10-31")] abbrev back_toArray := @back!_toArray
 
+@[deprecated setIfInBounds_toArray (since := "2024-11-24")] abbrev setD_toArray := @setIfInBounds_toArray
+
 end List
 
 namespace Array
@@ -2290,4 +2293,11 @@ abbrev get_swap' := @getElem_swap'
 @[deprecated eq_push_pop_back!_of_size_ne_zero (since := "2024-10-31")]
 abbrev eq_push_pop_back_of_size_ne_zero := @eq_push_pop_back!_of_size_ne_zero
 
+@[deprecated set!_is_setIfInBounds (since := "2024-11-24")] abbrev set_is_setIfInBounds := @set!_is_setIfInBounds
+@[deprecated size_setIfInBounds (since := "2024-11-24")] abbrev size_setD := @size_setIfInBounds
+@[deprecated getElem_setIfInBounds_eq (since := "2024-11-24")] abbrev getElem_setD_eq := @getElem_setIfInBounds_eq
+@[deprecated getElem?_setIfInBounds_eq (since := "2024-11-24")] abbrev get?_setD_eq := @getElem?_setIfInBounds_eq
+@[deprecated getD_get?_setIfInBounds (since := "2024-11-24")] abbrev getD_setD := @getD_get?_setIfInBounds
+@[deprecated getElem_setIfInBounds (since := "2024-11-24")] abbrev getElem_setD := @getElem_setIfInBounds
+
 end Array

src/Init/Data/Array/Set.lean

@@ -25,9 +25,11 @@ Set an element in an array, or do nothing if the index is out of bounds.
 This will perform the update destructively provided that `a` has a reference
 count of 1 when called.
 -/
-@[inline] def Array.setD (a : Array α) (i : Nat) (v : α) : Array α :=
+@[inline] def Array.setIfInBounds (a : Array α) (i : Nat) (v : α) : Array α :=
   dite (LT.lt i a.size) (fun h => a.set i v h) (fun _ => a)
 
+@[deprecated Array.setIfInBounds (since := "2024-11-24")] abbrev Array.setD := @Array.setIfInBounds
+
 /--
 Set an element in an array, or panic if the index is out of bounds.
 
@@ -36,4 +38,4 @@ count of 1 when called.
 -/
 @[extern "lean_array_set"]
 def Array.set! (a : Array α) (i : @& Nat) (v : α) : Array α :=
-  Array.setD a i v
+  Array.setIfInBounds a i v

src/Init/Syntax.lean

@@ -30,7 +30,7 @@ Does nothing for non-`node` nodes, or if `i` is out of bounds of the node list.
 -/
 def setArg (stx : Syntax) (i : Nat) (arg : Syntax) : Syntax :=
   match stx with
-  | node info k args => node info k (args.setD i arg)
+  | node info k args => node info k (args.setIfInBounds i arg)
   | stx              => stx
 
 end Lean.Syntax

src/Lean/Elab/MutualInductive.lean

@@ -377,7 +377,7 @@ private def getArity (indType : InductiveType) : MetaM Nat :=
   forallTelescopeReducing indType.type fun xs _ => return xs.size
 
 private def resetMaskAt (mask : Array Bool) (i : Nat) : Array Bool :=
-  mask.setD i false
+  mask.setIfInBounds i false
 
 /--
 Compute a bit-mask that for `indType`. The size of the resulting array `result` is the arity of `indType`.

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

@@ -481,7 +481,7 @@ theorem deleteOne_preserves_strongAssignmentsInvariant {n : Nat} (f : DefaultFor
           exists_eq_right, List.mem_map, Prod.exists, Bool.exists_bool]
         rcases hf with hf | hf
         · apply Or.inl
-          simp only [Array.set!, Array.setD]
+          simp only [Array.set!, Array.setIfInBounds]
           split
           · rcases List.getElem_of_mem hf with ⟨idx, hbound, hidx⟩
             simp only [← hidx, Array.toList_set]
@@ -514,7 +514,7 @@ theorem deleteOne_preserves_strongAssignmentsInvariant {n : Nat} (f : DefaultFor
           exists_eq_right, List.mem_map, Prod.exists, Bool.exists_bool]
         rcases hf with hf | hf
         · apply Or.inl
-          simp only [Array.set!, Array.setD]
+          simp only [Array.set!, Array.setIfInBounds]
           split
           · rcases List.getElem_of_mem hf with ⟨idx, hbound, hidx⟩
             simp only [← hidx, Array.toList_set]
@@ -574,7 +574,7 @@ theorem deleteOne_preserves_strongAssignmentsInvariant {n : Nat} (f : DefaultFor
           exists_eq_right, List.mem_map, Prod.exists, Bool.exists_bool]
         rcases hf with hf | hf
         · apply Or.inl
-          simp only [Array.set!, Array.setD]
+          simp only [Array.set!, Array.setIfInBounds]
           split
           · rcases List.getElem_of_mem hf with ⟨idx, hbound, hidx⟩
             simp only [← hidx, Array.toList_set]
@@ -644,7 +644,7 @@ theorem deleteOne_subset (f : DefaultFormula n) (id : Nat) (c : DefaultClause n)
     · apply Or.inl
       simp only [List.mem_filterMap, id_eq, exists_eq_right] at h1
       simp only [List.mem_filterMap, id_eq, exists_eq_right]
-      rw [Array.set!, Array.setD] at h1
+      rw [Array.set!, Array.setIfInBounds] at h1
       split at h1
       · simp only [Array.toList_set] at h1
         rcases List.getElem_of_mem h1 with ⟨i, h, h4⟩

tests/lean/simpArrayIdx.lean

@@ -10,13 +10,13 @@ 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.setD i v)[i]!
+#check_simp (a.set! i v).get! 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
 
 -- Checks with different index values.
-#check_simp (a.set! i v)[j]'j_lt  ~> (a.setD i v)[j]'_
-#check_simp (a.setD i v)[j]'j_lt !~>
+#check_simp (a.set! i v)[j]'j_lt  ~> (a.setIfInBounds i v)[j]'_
+#check_simp (a.setIfInBounds i v)[j]'j_lt !~>
 
 section
 variable (p : i < a.size)