chore: switch obvious cases of array "bang"[]! indexing to rely on …

…hypothesis (#5552)

Update certain uses of `arr[i]!` to use the "provably correct" version
`arr[i]`, in order to use "best practices".

Some motivation and discussion on
[Zulip](https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Lean.20compiler.2Felaborator.20development.20question/near/472934715)

src/Lean/Compiler/IR/SimpCase.lean

@@ -20,18 +20,18 @@ def ensureHasDefault (alts : Array Alt) : Array Alt :=
 private def getOccsOf (alts : Array Alt) (i : Nat) : Nat := Id.run do
   let aBody := (alts.get! i).body
   let mut n := 1
-  for j in [i+1:alts.size] do
-    if alts[j]!.body == aBody then
+  for h: j in [i+1:alts.size] do
+    if alts[j].body == aBody then
       n := n+1
   return n
 
 private def maxOccs (alts : Array Alt) : Alt × Nat := Id.run do
   let mut maxAlt := alts[0]!
   let mut max    := getOccsOf alts 0
-  for i in [1:alts.size] do
+  for h: i in [1:alts.size] do
     let curr := getOccsOf alts i
     if curr > max then
-       maxAlt := alts[i]!
+       maxAlt := alts[i]
        max    := curr
   return (maxAlt, max)
 

src/Lean/Compiler/LCNF/Check.lean

@@ -110,8 +110,8 @@ def isCtorParam (f : Expr) (i : Nat) : CoreM Bool := do
 def checkAppArgs (f : Expr) (args : Array Arg) : CheckM Unit := do
   let mut fType ← inferType f
   let mut j := 0
-  for i in [:args.size] do
-    let arg := args[i]!
+  for h: i in [:args.size] do
+    let arg := args[i]
     if fType.isErased then
       return ()
     fType := fType.headBeta

src/Lean/Compiler/LCNF/ElimDeadBranches.lean

@@ -505,8 +505,8 @@ ones. Return whether any `Value` got updated in the process.
 -/
 def inferStep : InterpM Bool := do
   let ctx ← read
-  for idx in [0:ctx.decls.size] do
-    let decl := ctx.decls[idx]!
+  for h: idx in [0:ctx.decls.size] do
+    let decl := ctx.decls[idx]
     if !decl.safe then
       continue
 

src/Lean/Compiler/LCNF/MonoTypes.lean

@@ -48,8 +48,8 @@ def hasTrivialStructure? (declName : Name) : CoreM (Option TrivialStructureInfo)
   let [ctorName] := info.ctors | return none
   let mask ← getRelevantCtorFields ctorName
   let mut result := none
-  for i in [:mask.size] do
-    if mask[i]! then
+  for h: i in [:mask.size] do
+    if mask[i] then
       if result.isSome then return none
       result := some { ctorName, fieldIdx := i, numParams := info.numParams }
   return result
@@ -129,4 +129,4 @@ def getOtherDeclMonoType (declName : Name) : CoreM Expr := do
     modifyEnv fun env => monoTypeExt.modifyState env fun s => { s with mono := s.mono.insert declName type }
     return type
 
-end Lean.Compiler.LCNF
+end Lean.Compiler.LCNF

src/Lean/Compiler/LCNF/PullFunDecls.lean

@@ -96,9 +96,9 @@ where
     unless (← visited i) do
       modify fun (k, visited) => (k, visited.set! i true)
       let pi := ps[i]!
-      for j in [:ps.size] do
+      for h: j in [:ps.size] do
         unless (← visited j) do
-          let pj := ps[j]!
+          let pj := ps[j]
           if pj.used.contains pi.decl.fvarId then
             visit j
       modify fun (k, visited) => (pi.attach k, visited)

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

@@ -18,10 +18,10 @@ or not.
 private def getMaxOccs (alts : Array Alt) : Alt × Nat := Id.run do
   let mut maxAlt := alts[0]!
   let mut max    := getNumOccsOf alts 0
-  for i in [1:alts.size] do
+  for h: i in [1:alts.size] do
     let curr := getNumOccsOf alts i
     if curr > max then
-       maxAlt := alts[i]!
+       maxAlt := alts[i]
        max    := curr
   return (maxAlt, max)
 where
@@ -34,8 +34,8 @@ where
   getNumOccsOf (alts : Array Alt) (i : Nat) : Nat := Id.run do
     let code := alts[i]!.getCode
     let mut n := 1
-    for j in [i+1:alts.size] do
-      if Code.alphaEqv alts[j]!.getCode code then
+    for h: j in [i+1:alts.size] do
+      if Code.alphaEqv alts[j].getCode code then
         n := n+1
     return n
 

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

@@ -121,8 +121,8 @@ where
     let mut paramsNew := #[]
     let singleton : FVarIdSet := ({} : FVarIdSet).insert params[targetParamIdx]!.fvarId
     let dependsOnDiscr := k.dependsOn singleton || decls.any (·.dependsOn singleton)
-    for i in [:params.size] do
-      let param := params[i]!
+    for h: i in [:params.size] do
+      let param := params[i]
       if targetParamIdx == i then
         if dependsOnDiscr then
           paramsNew := paramsNew.push (← internalizeParam param)
@@ -300,4 +300,3 @@ builtin_initialize
   registerTraceClass `Compiler.simp.jpCases
 
 end Lean.Compiler.LCNF
-

src/Lean/Compiler/LCNF/SpecInfo.lean

@@ -129,9 +129,9 @@ See comment at `.fixedNeutral`.
 -/
 private def hasFwdDeps (decl : Decl) (paramsInfo : Array SpecParamInfo) (j : Nat) : Bool := Id.run do
   let param := decl.params[j]!
-  for k in [j+1 : decl.params.size] do
+  for h: k in [j+1 : decl.params.size] do
     if paramsInfo[k]! matches .user | .fixedHO | .fixedInst then
-      let param' := decl.params[k]!
+      let param' := decl.params[k]
       if param'.type.containsFVar param.fvarId then
         return true
   return false
@@ -214,4 +214,3 @@ builtin_initialize
   registerTraceClass `Compiler.specialize.info
 
 end Lean.Compiler.LCNF
-

src/Lean/Compiler/LCNF/ToDecl.lean

@@ -50,9 +50,9 @@ partial def inlineMatchers (e : Expr) : CoreM Expr :=
       let numAlts := info.numAlts
       let altNumParams := info.altNumParams
       let rec inlineMatcher (i : Nat) (args : Array Expr) (letFVars : Array Expr) : MetaM Expr := do
-        if i < numAlts then
+        if h: i < numAlts then
           let altIdx := i + info.getFirstAltPos
-          let numParams := altNumParams[i]!
+          let numParams := altNumParams[i]
           let alt ← normalizeAlt args[altIdx]! numParams
           Meta.withLetDecl (← mkFreshUserName `_alt) (← Meta.inferType alt) alt fun altFVar =>
             inlineMatcher (i+1) (args.set! altIdx altFVar) (letFVars.push altFVar)

src/Lean/Elab/App.lean

@@ -421,8 +421,8 @@ private def findNamedArgDependsOnCurrent? : M (Option NamedArg) := do
   else
     forallTelescopeReducing s.fType fun xs _ => do
       let curr := xs[0]!
-      for i in [1:xs.size] do
-        let xDecl ← xs[i]!.fvarId!.getDecl
+      for h: i in [1:xs.size] do
+        let xDecl ← xs[i].fvarId!.getDecl
         if let some arg := s.namedArgs.find? fun arg => arg.name == xDecl.userName then
           /- Remark: a default value at `optParam` does not count as a dependency -/
           if (← exprDependsOn xDecl.type.cleanupAnnotations curr.fvarId!) then
@@ -800,8 +800,8 @@ def getElabElimExprInfo (elimExpr : Expr) : MetaM ElabElimInfo := do
         return s
     /- Collect the major parameter positions -/
     let mut majorsPos := #[]
-    for i in [:xs.size] do
-      let x := xs[i]!
+    for h: i in [:xs.size] do
+      let x := xs[i]
       unless motivePos == i do
         let xType ← x.fvarId!.getType
         /-
@@ -1301,8 +1301,8 @@ private def addLValArg (baseName : Name) (fullName : Name) (e : Expr) (args : Ar
   forallTelescopeReducing fType fun xs _ => do
     let mut argIdx := 0 -- position of the next explicit argument
     let mut remainingNamedArgs := namedArgs
-    for i in [:xs.size] do
-      let x := xs[i]!
+    for h: i in [:xs.size] do
+      let x := xs[i]
       let xDecl ← x.fvarId!.getDecl
       /- If there is named argument with name `xDecl.userName`, then we skip it. -/
       match remainingNamedArgs.findIdx? (fun namedArg => namedArg.name == xDecl.userName) with

src/Lean/Elab/BuiltinNotation.lean

@@ -55,8 +55,8 @@ open Meta
             let cinfo ← getConstInfoCtor ctor
             let numExplicitFields ← forallTelescopeReducing cinfo.type fun xs _ => do
               let mut n := 0
-              for i in [cinfo.numParams:xs.size] do
-                if (← getFVarLocalDecl xs[i]!).binderInfo.isExplicit then
+              for h: i in [cinfo.numParams:xs.size] do
+                if (← getFVarLocalDecl xs[i]).binderInfo.isExplicit then
                   n := n + 1
               return n
             let args := args.getElems

src/Lean/Elab/DeclNameGen.lean

@@ -64,13 +64,13 @@ private partial def winnowExpr (e : Expr) : MetaM Expr := do
         let mut fty ← inferType f
         let mut j := 0
         let mut e' ← visit f
-        for i in [0:args.size] do
+        for h: i in [0:args.size] do
           unless fty.isForall do
             fty ← withTransparency .all <| whnf <| fty.instantiateRevRange j i args
             j := i
           let .forallE _ _ fty' bi := fty | failure
           fty := fty'
-          let arg := args[i]!
+          let arg := args[i]
           if ← pure bi.isExplicit <||> (pure !arg.isSort <&&> isTypeFormer arg) then
             unless (← isProof arg) do
               e' := .app e' (← visit arg)

src/Lean/Elab/Deriving/Inhabited.lean

@@ -86,8 +86,8 @@ where
       addLocalInstancesForParams xs[:ctorVal.numParams] fun localInst2Index => do
         let mut usedInstIdxs := {}
         let mut ok := true
-        for i in [ctorVal.numParams:xs.size] do
-          let x := xs[i]!
+        for h: i in [ctorVal.numParams:xs.size] do
+          let x := xs[i]
           let instType ← mkAppM `Inhabited #[(← inferType x)]
           trace[Elab.Deriving.inhabited] "checking {instType} for '{ctorName}'"
           match (← trySynthInstance instType) with

src/Lean/Elab/Deriving/Repr.lean

@@ -29,8 +29,8 @@ def mkBodyForStruct (header : Header) (indVal : InductiveVal) : TermElabM Term :
     let mut fields ← `(Format.nil)
     if xs.size != numParams + fieldNames.size then
       throwError "'deriving Repr' failed, unexpected number of fields in structure"
-    for i in [:fieldNames.size] do
-      let fieldName := fieldNames[i]!
+    for h: i in [:fieldNames.size] do
+      let fieldName := fieldNames[i]
       let fieldNameLit := Syntax.mkStrLit (toString fieldName)
       let x := xs[numParams + i]!
       if i != 0 then
@@ -59,10 +59,10 @@ where
         let mut ctorArgs := #[]
         let mut rhs : Term := Syntax.mkStrLit (toString ctorInfo.name)
         rhs ← `(Format.text $rhs)
-        for i in [:xs.size] do
+        for h: i in [:xs.size] do
           -- Note: some inductive parameters are explicit if they were promoted from indices,
           -- so we process all constructor arguments in the same loop.
-          let x := xs[i]!
+          let x := xs[i]
           let a ← mkIdent <$> if i < indVal.numParams then pure header.argNames[i]! else mkFreshUserName `a
           if i < indVal.numParams then
             -- add `_` for inductive parameters, they are inaccessible

src/Lean/Elab/Inductive.lean

@@ -168,8 +168,8 @@ private def checkHeader (r : ElabHeaderResult) (numParams : Nat) (firstType? : O
 
 -- Auxiliary function for checking whether the types in mutually inductive declaration are compatible.
 private partial def checkHeaders (rs : Array ElabHeaderResult) (numParams : Nat) (i : Nat) (firstType? : Option Expr) : TermElabM Unit := do
-  if i < rs.size then
-    let type ← checkHeader rs[i]! numParams firstType?
+  if h: i < rs.size then
+    let type ← checkHeader rs[i] numParams firstType?
     checkHeaders rs numParams (i+1) type
 
 private def elabHeader (views : Array InductiveView) : TermElabM (Array ElabHeaderResult) := do
@@ -222,11 +222,11 @@ private def replaceArrowBinderNames (type : Expr) (newNames : Array Name) : Expr
   go type 0
 where
   go (type : Expr) (i : Nat) : Expr :=
-    if i < newNames.size then
+    if h: i < newNames.size then
       match type with
       | .forallE n d b bi =>
         if n.hasMacroScopes then
-          mkForall newNames[i]! bi d (go b (i+1))
+          mkForall newNames[i] bi d (go b (i+1))
         else
           mkForall n bi d (go b (i+1))
       | _ => type

src/Lean/Elab/Match.lean

@@ -330,8 +330,8 @@ private def elabPatterns (patternStxs : Array Syntax) (matchType : Expr) : Excep
   withReader (fun ctx => { ctx with implicitLambda := false }) do
     let mut patterns  := #[]
     let mut matchType := matchType
-    for idx in [:patternStxs.size] do
-      let patternStx := patternStxs[idx]!
+    for h: idx in [:patternStxs.size] do
+      let patternStx := patternStxs[idx]
       matchType ← whnf matchType
       match matchType with
       | Expr.forallE _ d b _ =>

src/Lean/Elab/MutualDef.lean

@@ -406,9 +406,9 @@ private def elabFunValues (headers : Array DefViewElabHeader) (vars : Array Expr
       (if header.kind.isTheorem && !deprecated.oldSectionVars.get (← getOptions) then withHeaderSecVars vars sc #[header] else fun x => x #[]) fun vars => do
       forallBoundedTelescope header.type header.numParams fun xs type => do
         -- Add new info nodes for new fvars. The server will detect all fvars of a binder by the binder's source location.
-        for i in [0:header.binderIds.size] do
+        for h: i in [0:header.binderIds.size] do
           -- skip auto-bound prefix in `xs`
-          addLocalVarInfo header.binderIds[i]! xs[header.numParams - header.binderIds.size + i]!
+          addLocalVarInfo header.binderIds[i] xs[header.numParams - header.binderIds.size + i]!
         let val ← withReader ({ · with tacSnap? := header.tacSnap? }) do
           -- synthesize mvars here to force the top-level tactic block (if any) to run
           elabTermEnsuringType valStx type <* synthesizeSyntheticMVarsNoPostponing

src/Lean/Elab/PreDefinition/Nonrec/Eqns.lean

@@ -77,9 +77,9 @@ def mkEqns (declName : Name) (info : DefinitionVal) : MetaM (Array Name) :=
     withReducible do
       mkEqnTypes #[] goal.mvarId!
   let mut thmNames := #[]
-  for i in [: eqnTypes.size] do
-    let type := eqnTypes[i]!
-    trace[Elab.definition.eqns] "eqnType[{i}]: {eqnTypes[i]!}"
+  for h: i in [: eqnTypes.size] do
+    let type := eqnTypes[i]
+    trace[Elab.definition.eqns] "eqnType[{i}]: {eqnTypes[i]}"
     let name := (Name.str baseName eqnThmSuffixBase).appendIndexAfter (i+1)
     thmNames := thmNames.push name
     let value ← mkProof declName type

src/Lean/Elab/PreDefinition/Structural/Eqns.lean

@@ -67,8 +67,8 @@ def mkEqns (info : EqnInfo) : MetaM (Array Name) :=
     mkEqnTypes info.declNames goal.mvarId!
   let baseName := info.declName
   let mut thmNames := #[]
-  for i in [: eqnTypes.size] do
-    let type := eqnTypes[i]!
+  for h: i in [: eqnTypes.size] do
+    let type := eqnTypes[i]
     trace[Elab.definition.structural.eqns] "eqnType {i}: {type}"
     let name := (Name.str baseName eqnThmSuffixBase).appendIndexAfter (i+1)
     thmNames := thmNames.push name

src/Lean/Elab/PreDefinition/WF/Eqns.lean

@@ -83,9 +83,9 @@ def mkEqns (declName : Name) (info : EqnInfo) : MetaM (Array Name) :=
     withReducible do
       mkEqnTypes info.declNames goal.mvarId!
   let mut thmNames := #[]
-  for i in [: eqnTypes.size] do
-    let type := eqnTypes[i]!
-    trace[Elab.definition.wf.eqns] "{eqnTypes[i]!}"
+  for h: i in [: eqnTypes.size] do
+    let type := eqnTypes[i]
+    trace[Elab.definition.wf.eqns] "{eqnTypes[i]}"
     let name := (Name.str baseName eqnThmSuffixBase).appendIndexAfter (i+1)
     thmNames := thmNames.push name
     let value ← mkProof declName type

src/Lean/Elab/Quotation.lean

@@ -655,9 +655,9 @@ The parameter `alts` provides position information for alternatives.
 -/
 private def checkUnusedAlts (stx : Syntax) (alts : Array Syntax) (altIdxMap : NameMap Nat) (ignoreIfUnused : IdxSet) : TermElabM Syntax := do
   let (stx, used) ← findUsedAlts stx altIdxMap
-  for i in [:alts.size] do
+  for h: i in [:alts.size] do
     unless used.contains i || ignoreIfUnused.contains i do
-      logErrorAt alts[i]! s!"redundant alternative #{i+1}"
+      logErrorAt alts[i] s!"redundant alternative #{i+1}"
   return stx
 
 def match_syntax.expand (stx : Syntax) : TermElabM Syntax := do

src/Lean/Elab/SyntheticMVars.lean

@@ -257,8 +257,8 @@ private def throwStuckAtUniverseCnstr : TermElabM Unit := do
     unless found.contains (lhs, rhs) do
       found := found.insert (lhs, rhs)
       uniqueEntries := uniqueEntries.push entry
-  for i in [1:uniqueEntries.size] do
-    logErrorAt uniqueEntries[i]!.ref (← mkLevelStuckErrorMessage uniqueEntries[i]!)
+  for h: i in [1:uniqueEntries.size] do
+    logErrorAt uniqueEntries[i].ref (← mkLevelStuckErrorMessage uniqueEntries[i]!)
   throwErrorAt uniqueEntries[0]!.ref (← mkLevelStuckErrorMessage uniqueEntries[0]!)
 
 /--

src/Lean/Elab/Tactic/Induction.lean

@@ -205,8 +205,8 @@ private def isWildcard (altStx : Syntax) : Bool :=
   getAltName altStx == `_
 
 private def checkAltNames (alts : Array Alt) (altsSyntax : Array Syntax) : TacticM Unit :=
-  for i in [:altsSyntax.size] do
-    let altStx := altsSyntax[i]!
+  for h: i in [:altsSyntax.size] do
+    let altStx := altsSyntax[i]
     if getAltName altStx == `_ && i != altsSyntax.size - 1 then
       withRef altStx <| throwError "invalid occurrence of wildcard alternative, it must be the last alternative"
     let altName := getAltName altStx
@@ -236,8 +236,8 @@ private def saveAltVarsInfo (altMVarId : MVarId) (altStx : Syntax) (fvarIds : Ar
     let altVars := getAltVars altStx
     for fvarId in fvarIds do
       if !useNamesForExplicitOnly || (← fvarId.getDecl).binderInfo.isExplicit then
-        if i < altVars.size then
-          Term.addLocalVarInfo altVars[i]! (mkFVar fvarId)
+        if h: i < altVars.size then
+          Term.addLocalVarInfo altVars[i] (mkFVar fvarId)
           i := i + 1
 
 open Language in
@@ -320,8 +320,8 @@ where
     2- The errors are produced in the same order the appear in the code above. This is not super
     important when using IDEs.
     -/
-    for altStxIdx in [0:altStxs.size] do
-      let altStx := altStxs[altStxIdx]!
+    for h: altStxIdx in [0:altStxs.size] do
+      let altStx := altStxs[altStxIdx]
       let altName := getAltName altStx
       if let some i := alts.findIdx? (·.1 == altName) then
         -- cover named alternative

src/Lean/Elab/Tactic/Omega/Core.lean

@@ -513,13 +513,13 @@ def fourierMotzkinSelect (data : Array FourierMotzkinData) : MetaM FourierMotzki
   if bestSize = 0 then
     trace[omega] "Selected variable {data[0]!.var}."
     return data[0]!
-  for i in [1:data.size] do
-    let exact := data[i]!.exact
-    let size := data[i]!.size
+  for h: i in [1:data.size] do
+    let exact := data[i].exact
+    let size := data[i].size
     if size = 0 || !bestExact && exact || (bestExact == exact) && size < bestSize then
       if size = 0 then
-        trace[omega] "Selected variable {data[i]!.var}"
-        return data[i]!
+        trace[omega] "Selected variable {data[i].var}"
+        return data[i]
       bestIdx := i
       bestExact := exact
       bestSize := size