feat: change Array.set to take a Nat and a tactic provided bound

Author: kim-em

src/Init/Data/Array/Basic.lean

@@ -30,7 +30,8 @@ namespace Array
 
 /-! ### Preliminary theorems -/
 
-@[simp] theorem size_set (a : Array α) (i : Fin a.size) (v : α) : (set a i v).size = a.size :=
+@[simp] theorem size_set (a : Array α) (i : Nat) (v : α) (h : i < a.size) :
+    (set a i v h).size = a.size :=
   List.length_set ..
 
 @[simp] theorem size_push (a : Array α) (v : α) : (push a v).size = a.size + 1 :=
@@ -142,7 +143,7 @@ def uget (a : @& Array α) (i : USize) (h : i.toNat < a.size) : α :=
    `fset` may be slightly slower than `uset`. -/
 @[extern "lean_array_uset"]
 def uset (a : Array α) (i : USize) (v : α) (h : i.toNat < a.size) : Array α :=
-  a.set ⟨i.toNat, h⟩ v
+  a.set i.toNat v h
 
 @[extern "lean_array_pop"]
 def pop (a : Array α) : Array α where
@@ -168,10 +169,10 @@ def swap (a : Array α) (i j : @& Fin a.size) : Array α :=
   let v₁ := a.get i
   let v₂ := a.get j
   let a'  := a.set i v₂
-  a'.set (size_set a i v₂ ▸ j) v₁
+  a'.set j v₁ (Nat.lt_of_lt_of_eq j.isLt (size_set a i v₂ _).symm)
 
 @[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
+  show ((a.set i (a.get j)).set j (a.get i) (Nat.lt_of_lt_of_eq j.isLt (size_set a i (a.get j) _).symm)).size = a.size
   rw [size_set, size_set]
 
 /--
@@ -279,7 +280,7 @@ unsafe def modifyMUnsafe [Monad m] (a : Array α) (i : Nat) (f : α → m α) :
     -- of the element type, and that it is valid to store `box(0)` in any array.
     let a'               := a.set idx (unsafeCast ())
     let v ← f v
-    pure <| a'.set (size_set a .. ▸ idx) v
+    pure <| a'.set idx v (Nat.lt_of_lt_of_eq h (size_set a ..).symm)
   else
     pure a
 

src/Init/Data/Array/BasicAux.lean

@@ -60,7 +60,7 @@ where
       if ptrEq a b then
         go (i+1) as
       else
-        go (i+1) (as.set ⟨i, h⟩ b)
+        go (i+1) (as.set i b h)
     else
       return as
 

src/Init/Data/Array/Lemmas.lean

@@ -337,25 +337,26 @@ theorem get!_eq_getD [Inhabited α] (a : Array α) : a.get! n = a.getD n default
 
 /-! # set -/
 
-@[simp] theorem getElem_set_eq (a : Array α) (i : Fin a.size) (v : α) {j : Nat}
-      (eq : i.val = j) (p : j < (a.set i v).size) :
+@[simp] theorem getElem_set_eq (a : Array α) (i : Nat) (h : i < a.size) (v : α) {j : Nat}
+      (eq : i = j) (p : j < (a.set i v).size) :
     (a.set i v)[j]'p = v := by
   simp [set, getElem_eq_getElem_toList, ←eq]
 
-@[simp] theorem getElem_set_ne (a : Array α) (i : Fin a.size) (v : α) {j : Nat} (pj : j < (a.set i v).size)
-    (h : i.val ≠ j) : (a.set i v)[j]'pj = a[j]'(size_set a i v ▸ pj) := by
+@[simp] theorem getElem_set_ne (a : Array α) (i : Nat) (h' : i < a.size) (v : α) {j : Nat}
+    (pj : j < (a.set i v).size) (h : i ≠ j) :
+    (a.set i v)[j]'pj = a[j]'(size_set a i v _ ▸ pj) := by
   simp only [set, getElem_eq_getElem_toList, List.getElem_set_ne h]
 
-theorem getElem_set (a : Array α) (i : Fin a.size) (v : α) (j : Nat)
+theorem getElem_set (a : Array α) (i : Nat) (h' : i < a.size) (v : α) (j : Nat)
     (h : j < (a.set i v).size) :
-    (a.set i v)[j]'h = if i = j then v else a[j]'(size_set a i v ▸ h) := by
-  by_cases p : i.1 = j <;> simp [p]
+    (a.set i v)[j]'h = if i = j then v else a[j]'(size_set a i v _ ▸ h) := by
+  by_cases p : i = j <;> simp [p]
 
-@[simp] theorem getElem?_set_eq (a : Array α) (i : Fin a.size) (v : α) :
-    (a.set i v)[i.1]? = v := by simp [getElem?_lt, i.2]
+@[simp] theorem getElem?_set_eq (a : Array α) (i : Nat) (h : i < a.size) (v : α) :
+    (a.set i v)[i]? = v := by simp [getElem?_lt, h]
 
-@[simp] theorem getElem?_set_ne (a : Array α) (i : Fin a.size) {j : Nat} (v : α)
-    (ne : i.val ≠ j) : (a.set i v)[j]? = a[j]? := by
+@[simp] theorem getElem?_set_ne (a : Array α) (i : Nat) (h : i < a.size) {j : Nat} (v : α)
+    (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 -/
@@ -372,7 +373,7 @@ theorem getElem_set (a : Array α) (i : Fin a.size) (v : α) (j : Nat)
 @[simp] theorem getElem_setD_eq (a : Array α) {i : Nat} (v : α) (h : _) :
     (setD a i v)[i]'h = v := by
   simp at h
-  simp only [setD, h, dite_true, getElem_set, ite_true]
+  simp only [setD, 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
@@ -547,43 +548,43 @@ theorem getElem?_push {a : Array α} : (a.push x)[i]? = if i = a.size then some
 
 @[deprecated getElem?_size (since := "2024-10-21")] abbrev get?_size := @getElem?_size
 
-@[simp] theorem toList_set (a : Array α) (i v) : (a.set i v).toList = a.toList.set i.1 v := rfl
+@[simp] theorem toList_set (a : Array α) (i v h) : (a.set i v).toList = a.toList.set i v := rfl
 
-theorem get_set_eq (a : Array α) (i : Fin a.size) (v : α) :
-    (a.set i v)[i.1] = v := by
+theorem get_set_eq (a : Array α) (i : Nat) (v : α) (h : i < a.size) :
+    (a.set i v h)[i]'(by simp [h]) = v := by
   simp only [set, getElem_eq_getElem_toList, List.getElem_set_self]
 
-theorem get?_set_eq (a : Array α) (i : Fin a.size) (v : α) :
-    (a.set i v)[i.1]? = v := by simp [getElem?_pos, i.2]
+theorem get?_set_eq (a : Array α) (i : Nat) (v : α) (h : i < a.size) :
+    (a.set i v)[i]? = v := by simp [getElem?_pos, h]
 
-@[simp] theorem get?_set_ne (a : Array α) (i : Fin a.size) {j : Nat} (v : α)
-    (h : i.1 ≠ j) : (a.set i v)[j]? = a[j]? := by
+@[simp] theorem get?_set_ne (a : Array α) (i : Nat) (h' : i < a.size) {j : Nat} (v : α)
+    (h : i ≠ j) : (a.set i v)[j]? = a[j]? := by
   by_cases j < a.size <;> simp [getElem?_pos, getElem?_neg, *]
 
-theorem get?_set (a : Array α) (i : Fin a.size) (j : Nat) (v : α) :
-    (a.set i v)[j]? = if i.1 = j then some v else a[j]? := by
-  if h : i.1 = j then subst j; simp [*] else simp [*]
+theorem get?_set (a : Array α) (i : Nat) (h : i < a.size) (j : Nat) (v : α) :
+    (a.set i v)[j]? = if i = j then some v else a[j]? := by
+  if h : i = j then subst j; simp [*] else simp [*]
 
-theorem get_set (a : Array α) (i : Fin a.size) (j : Nat) (hj : j < a.size) (v : α) :
+theorem get_set (a : Array α) (i : Nat) (hi : i < a.size) (j : Nat) (hj : j < a.size) (v : α) :
     (a.set i v)[j]'(by simp [*]) = if i = j then v else a[j] := by
-  if h : i.1 = j then subst j; simp [*] else simp [*]
+  if h : i = j then subst j; simp [*] else simp [*]
 
-@[simp] theorem get_set_ne (a : Array α) (i : Fin a.size) {j : Nat} (v : α) (hj : j < a.size)
-    (h : i.1 ≠ j) : (a.set i v)[j]'(by simp [*]) = a[j] := by
+@[simp] theorem get_set_ne (a : Array α) (i : Nat) (hi : i < a.size) {j : Nat} (v : α) (hj : j < a.size)
+    (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
   simp at h
-  simp only [setD, h, dite_true, get_set, ite_true]
+  simp only [setD, h, ↓reduceDIte, getElem_set_eq]
 
-theorem set_set (a : Array α) (i : Fin a.size) (v v' : α) :
-    (a.set i v).set ⟨i, by simp [i.2]⟩ v' = a.set i v' := by simp [set, List.set_set]
+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]
 
 private theorem fin_cast_val (e : n = n') (i : Fin n) : e ▸ i = ⟨i.1, e ▸ i.2⟩ := by cases e; rfl
 
 theorem swap_def (a : Array α) (i j : Fin a.size) :
-    a.swap i j = (a.set i (a.get j)).set ⟨j.1, by simp [j.2]⟩ (a.get i) := by
+    a.swap i j = (a.set i (a.get j)).set j (a.get i) := by
   simp [swap, fin_cast_val]
 
 @[simp] theorem toList_swap (a : Array α) (i j : Fin a.size) :
@@ -601,7 +602,7 @@ theorem getElem?_swap (a : Array α) (i j : Fin a.size) (k : Nat) : (a.swap i j)
 
 @[simp]
 theorem swapAt!_def (a : Array α) (i : Nat) (v : α) (h : i < a.size) :
-    a.swapAt! i v = (a[i], a.set ⟨i, h⟩ v) := by simp [swapAt!, h]
+    a.swapAt! i v = (a[i], a.set i v) := by simp [swapAt!, h]
 
 @[simp] theorem size_swapAt! (a : Array α) (i : Nat) (v : α) :
     (a.swapAt! i v).2.size = a.size := by
@@ -966,7 +967,7 @@ 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]
   split
-  · simp only [Id.bind_eq, get_set _ _ _ (by simpa using h)]; split <;> simp [*]
+  · 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))]
 
 @[simp] theorem toList_modify (as : Array α) (f : α → α) :
@@ -1406,30 +1407,15 @@ instance [DecidableEq α] (a : α) (as : Array α) : Decidable (a ∈ as) :=
 
 open Fin
 
-@[simp] theorem getElem_swap_right (a : Array α) {i j : Fin a.size} : (a.swap i j)[j.val] = a[i] :=
-  by simp only [swap, fin_cast_val, get_eq_getElem, getElem_set_eq, getElem_fin]
+@[simp] theorem getElem_swap_right (a : Array α) {i j : Fin a.size} : (a.swap i j)[j.1] = a[i] := by
+  simp [swap_def, getElem_set]
 
-@[simp] theorem getElem_swap_left (a : Array α) {i j : Fin a.size} : (a.swap i j)[i.val] = a[j] :=
-  if he : ((Array.size_set _ _ _).symm ▸ j).val = i.val then by
-    simp only [←he, fin_cast_val, getElem_swap_right, getElem_fin]
-  else by
-    apply Eq.trans
-    · apply Array.get_set_ne
-      · simp only [size_set, Fin.isLt]
-      · assumption
-    · simp [get_set_ne]
+@[simp] theorem getElem_swap_left (a : Array α) {i j : Fin a.size} : (a.swap i j)[i.1] = a[j] := by
+  simp +contextual [swap_def, getElem_set]
 
 @[simp] theorem getElem_swap_of_ne (a : Array α) {i j : Fin a.size} (hp : p < a.size)
     (hi : p ≠ i) (hj : p ≠ j) : (a.swap i j)[p]'(a.size_swap .. |>.symm ▸ hp) = a[p] := by
-  apply Eq.trans
-  · have : ((a.size_set i (a.get j)).symm ▸ j).val = j.val := by simp only [fin_cast_val]
-    apply Array.get_set_ne
-    · simp only [this]
-      apply Ne.symm
-      · assumption
-  · apply Array.get_set_ne
-    · apply Ne.symm
-      · assumption
+  simp [swap_def, getElem_set, hi.symm, hj.symm]
 
 theorem getElem_swap' (a : Array α) (i j : Fin a.size) (k : Nat) (hk : k < a.size) :
     (a.swap i j)[k]'(by simp_all) = if k = i then a[j] else if k = j then a[i] else a[k] := by

src/Init/Data/Array/Set.lean

@@ -14,8 +14,8 @@ This will perform the update destructively provided that `a` has a reference
 count of 1 when called.
 -/
 @[extern "lean_array_fset"]
-def Array.set (a : Array α) (i : @& Fin a.size) (v : α) : Array α where
-  toList := a.toList.set i.val v
+def Array.set (a : Array α) (i : @& Nat) (v : α) (h : i < a.size := by get_elem_tactic): Array α where
+  toList := a.toList.set i v
 
 /--
 Set an element in an array, or do nothing if the index is out of bounds.
@@ -24,7 +24,7 @@ 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 α :=
-  dite (LT.lt i a.size) (fun h => a.set ⟨i, h⟩ v) (fun _ => a)
+  dite (LT.lt i a.size) (fun h => a.set i v h) (fun _ => a)
 
 /--
 Set an element in an array, or panic if the index is out of bounds.

src/Init/Data/ByteArray/Basic.lean

@@ -65,7 +65,7 @@ def set! : ByteArray → (@& Nat) → UInt8 → ByteArray
 
 @[extern "lean_byte_array_fset"]
 def set : (a : ByteArray) → (@& Fin a.size) → UInt8 → ByteArray
-  | ⟨bs⟩, i, b => ⟨bs.set i b⟩
+  | ⟨bs⟩, i, b => ⟨bs.set i.1 b i.2⟩
 
 @[extern "lean_byte_array_uset"]
 def uset : (a : ByteArray) → (i : USize) → UInt8 → i.toNat < a.size → ByteArray

src/Init/Data/FloatArray/Basic.lean

@@ -71,7 +71,7 @@ def uset : (a : FloatArray) → (i : USize) → Float → i.toNat < a.size → F
 
 @[extern "lean_float_array_fset"]
 def set : (ds : FloatArray) → (@& Fin ds.size) → Float → FloatArray
-  | ⟨ds⟩, i, d => ⟨ds.set i d⟩
+  | ⟨ds⟩, i, d => ⟨ds.set i.1 d i.2⟩
 
 @[extern "lean_float_array_set"]
 def set! : FloatArray → (@& Nat) → Float → FloatArray

src/Init/Meta.lean

@@ -443,7 +443,7 @@ def unsetTrailing (stx : Syntax) : Syntax :=
   if h : i < a.size then
     let v := a[i]
     match f v with
-    | some v => some <| a.set ⟨i, h⟩ v
+    | some v => some <| a.set i v h
     | none   => updateFirst a f (i+1)
   else
     none

src/Lean/Data/PersistentArray.lean

@@ -159,7 +159,7 @@ partial def popLeaf : PersistentArrayNode α → Option (Array α) × Array (Per
           let cs' := cs'.pop
           if cs'.isEmpty then (some l, emptyArray) else (some l, cs')
         else
-          (some l, cs'.set (Array.size_set cs idx _ ▸ idx) (node newLast))
+          (some l, cs'.set idx (node newLast) (by simp only [cs', Array.size_set]; omega))
     else
       (none, emptyArray)
   | leaf vs   => (some vs, emptyArray)

src/Lean/Elab/Inductive.lean

@@ -740,10 +740,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 :=
-  if h : i < mask.size then
-    mask.set ⟨i, h⟩ false
-  else
-    mask
+  mask.setD i false
 
 /--
   Compute a bit-mask that for `indType`. The size of the resulting array `result` is the arity of `indType`.

src/Lean/Environment.lean

@@ -328,7 +328,7 @@ private def invalidExtMsg := "invalid environment extension has been accessed"
 
 unsafe def setState {σ} (ext : Ext σ) (exts : Array EnvExtensionState) (s : σ) : Array EnvExtensionState :=
   if h : ext.idx < exts.size then
-    exts.set ⟨ext.idx, h⟩ (unsafeCast s)
+    exts.set ext.idx (unsafeCast s)
   else
     have : Inhabited (Array EnvExtensionState) := ⟨exts⟩
     panic! invalidExtMsg

src/Lean/Meta/Closure.lean

@@ -226,7 +226,7 @@ partial def pickNextToProcessAux (lctx : LocalContext) (i : Nat) (toProcess : Ar
   if h : i < toProcess.size then
     let elem' := toProcess.get ⟨i, h⟩
     if (lctx.get! elem.fvarId).index < (lctx.get! elem'.fvarId).index then
-      pickNextToProcessAux lctx (i+1) (toProcess.set ⟨i, h⟩ elem) elem'
+      pickNextToProcessAux lctx (i+1) (toProcess.set i elem) elem'
     else
       pickNextToProcessAux lctx (i+1) toProcess elem
   else

src/Lean/Meta/DiscrTree.lean

@@ -460,7 +460,7 @@ where
   loop (i : Nat) : Array α :=
     if h : i < vs.size then
       if v == vs[i] then
-        vs.set ⟨i,h⟩ v
+        vs.set i v
       else
         loop (i+1)
     else

src/Lean/Meta/ExprDefEq.lean

@@ -1205,7 +1205,7 @@ private partial def processAssignment (mvarApp : Expr) (v : Expr) : MetaM Bool :
       if h : i < args.size then
         let arg := args.get ⟨i, h⟩
         let arg ← simpAssignmentArg arg
-        let args := args.set ⟨i, h⟩ arg
+        let args := args.set i arg
         match arg with
         | Expr.fvar fvarId =>
           if args[0:i].any fun prevArg => prevArg == arg then

src/Lean/Meta/GeneralizeTelescope.lean

@@ -23,7 +23,7 @@ partial def updateTypes (e eNew : Expr) (entries : Array Entry) (i : Nat) : Meta
       let typeAbst ← kabstract type e
       if typeAbst.hasLooseBVars then do
         let typeNew := typeAbst.instantiate1 eNew
-        let entries := entries.set ⟨i, h⟩ { entry with type := typeNew, modified := true }
+        let entries := entries.set i { entry with type := typeNew, modified := true }
         updateTypes e eNew entries (i+1)
       else
         updateTypes e eNew entries (i+1)

src/Lean/Meta/Match/MatcherApp/Transform.lean

@@ -29,7 +29,7 @@ private partial def updateAlts (unrefinedArgType : Expr) (typeNew : Expr) (altNu
           else
             pure <| !(← isDefEq unrefinedArgType (← inferType x[0]!))
           return (← mkLambdaFVars xs alt, refined)
-      updateAlts unrefinedArgType (b.instantiate1 alt) (altNumParams.set! i (numParams+1)) (alts.set ⟨i, h⟩ alt) refined (i+1)
+      updateAlts unrefinedArgType (b.instantiate1 alt) (altNumParams.set! i (numParams+1)) (alts.set i alt) refined (i+1)
     | _ => throwError "unexpected type at MatcherApp.addArg"
   else
     if refined then

src/Lean/Meta/SynthInstance.lean

@@ -671,7 +671,7 @@ private partial def preprocessArgs (type : Expr) (i : Nat) (args : Array Expr) (
       If an instance implicit argument depends on an `outParam`, it is treated as an `outParam` too.
       -/
       let arg ← if outParamsPos.contains i then mkFreshExprMVar d else pure arg
-      let args := args.set ⟨i, h⟩ arg
+      let args := args.set i arg
       preprocessArgs (b.instantiate1 arg) (i+1) args outParamsPos
     | _ =>
       throwError "type class resolution failed, insufficient number of arguments" -- TODO improve error message

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

@@ -115,7 +115,7 @@ theorem toListModel_foldl_reinsertAux [BEq α] [Hashable α] [PartialEquivBEq α
 theorem expand.go_pos [Hashable α] {i : Nat} {source : Array (AssocList α β)}
     {target : { d : Array (AssocList α β) // 0 < d.size }} (h : i < source.size) :
     expand.go i source target = go (i + 1)
-      (source.set ⟨i, h⟩ .nil) ((source.get ⟨i, h⟩).foldl (reinsertAux hash) target) := by
+      (source.set i .nil) ((source.get ⟨i, h⟩).foldl (reinsertAux hash) target) := by
   rw [expand.go]
   simp only [h, dite_true]