Update to v4.14.0

Auto/Embedding/LamConv.lean

@@ -1965,7 +1965,7 @@ section UnsafeOps
 
   /-- Turn `ts[i]` into `.bvar i` -/
   def LamTerm.abstractsImp (t : LamTerm) (ts : Array LamTerm) :=
-    let ts := ts.mapIdx (fun i x => (x, LamTerm.bvar i.val))
+    let ts := ts.mapIdx (fun i x => (x, LamTerm.bvar i))
     let tmap := @Std.HashMap.ofList _ _ inferInstance inferInstance ts.toList
     t.replace (fun x => tmap.get? x) 0
 

Auto/EvaluateAuto/ConstAnalysis.lean

@@ -39,8 +39,11 @@ def Name.isTheorem (name : Name) : CoreM Bool := do
   declaration range. Roughly speaking, a constant have a declaration
   range iff it is defined (presumably by a human) in a `.lean` file
 -/
-def Name.isHumanTheorem (name : Name) : CoreM Bool :=
-  return (← Lean.findDeclarationRanges? name).isSome && (← Name.isTheorem name)
+def Name.isHumanTheorem (name : Name) : CoreM Bool := do
+  let hasDeclRange := (← Lean.findDeclarationRanges? name).isSome
+  let isTheorem ← Name.isTheorem name
+  let notProjFn := !(← Lean.isProjectionFn name)
+  return hasDeclRange && isTheorem && notProjFn
 
 def allHumanTheorems : CoreM (Array Name) := do
   let allConsts := (← getEnv).constants.toList.map Prod.fst

Auto/EvaluateAuto/TestCode.lean

@@ -66,8 +66,8 @@ instance : ToString EvalConfig where
   Premises which only contain logic constants are filtered because they
     are assumed to be known by the prover
 -/
-private def runAutoOnAutoLemmaMeta (declName? : Option Name) (lem : Auto.Lemma) : MetaM Result := do
-  if !(← Meta.isProp lem.type) then
+private def runAutoOnAutoLemma (declName? : Option Name) (lem : Auto.Lemma) : CoreM Result := do
+  if !(← Meta.MetaM.run' <| Meta.isProp lem.type) then
     return .nonProp
   -- **TODO: Aux theorem like those ending in `.proof_1`**
   let usedThmNames ← (← Expr.getUsedTheorems lem.proof).filterM (fun name =>
@@ -83,20 +83,19 @@ private def runAutoOnAutoLemmaMeta (declName? : Option Name) (lem : Auto.Lemma)
       Meta.mkLambdaFVars #[negGoalFVar] proofOfFalse
     let goal := mkApp2 (.const ``Classical.byContradiction []) body negGoalImpFalse
     Meta.mkLambdaFVars bs goal
-  let mut autoProof : Expr := Expr.sort .zero
-  try
-    autoProof ← autoProofFn
-  catch e =>
-    return .autoException e
-  match Kernel.check (← getEnv) {} autoProof with
-  | Except.ok autoProofType =>
-    match Kernel.isDefEq (← getEnv) {} autoProofType lem.type with
-    | Except.ok true => return .success
-    | _ => return .typeUnequal
-  | Except.error _ => return .typeCheckFail
-
-def runAutoOnAutoLemma (declName? : Option Name) (lem : Auto.Lemma) : CoreM Result := do
-  (runAutoOnAutoLemmaMeta declName? lem).run'
+  let result : Expr ⊕ Exception ←
+    Lean.Core.tryCatchRuntimeEx
+      (do let autoProof ← Meta.MetaM.run' autoProofFn; return .inl autoProof)
+      (fun e => return .inr e)
+  match result with
+  | .inl autoProof =>
+    match Kernel.check (← getEnv) {} autoProof with
+    | Except.ok autoProofType =>
+      match Kernel.isDefEq (← getEnv) {} autoProofType lem.type with
+      | Except.ok true => return .success
+      | _ => return .typeUnequal
+    | Except.error _ => return .typeCheckFail
+  | .inr e => return .autoException e
 
 /--
   Run `Lean-auto` on the type of ``name``, using premises collected

Auto/LemDB.lean

@@ -28,7 +28,7 @@ initialize lemDBExt : LemDBExtension ← registerPersistentEnvExtension {
   addEntryFn      := fun s n => s.insert n.1 n.2
   -- **Note** We suppose that, if module `a` imports module `b`,
   --   then the index of `a` within the `arr` is greater than the index of `b` in `arr`
-  addImportedFn   := fun arr => pure <| Std.HashMap.ofList (arr.concatMap id).toList,
+  addImportedFn   := fun arr => pure <| Std.HashMap.ofList (arr.flatMap id).toList,
   exportEntriesFn := fun s => s.toArray
 }
 

Auto/Lib/ExprExtra.lean

@@ -1,6 +1,7 @@
 import Lean
 import Auto.Lib.LevelExtra
 import Auto.Lib.Containers
+import Auto.Lib.AbstractMVars
 open Lean Elab Command
 
 namespace Auto
@@ -229,6 +230,33 @@ def Expr.whnfIfNotForall (e : Expr) : MetaM Expr := do
   else
     return (← Meta.whnf e)
 
+/--
+  Given expression `e₁, e₂`, attempt to find variables `x₁, ⋯, xₗ`,
+  terms `t₁, ⋯, tₖ` and a `m ≤ l` such that `∀ x₁ ⋯ xₗ. e₁ x₁ ⋯ xₘ = e₂ t₁ ⋯ tₖ`
+  Note that universe polymorphism is not supported
+
+  If successful, return
+    `(fun x₁ ⋯ xₗ => Eq.refl (e₁ x₁ ⋯ xₘ), ∀ x₁ ⋯ xₗ. e₁ x₁ ⋯ xₘ = e₂ t₁ ⋯ tₖ)`\
+  Otherwise, return `.none`
+-/
+def Expr.instanceOf? (e₁ e₂ : Expr) : MetaM (Option (Expr × Expr)) := do
+  let ty₁ ← Meta.inferType e₁
+  let ty₂ ← Meta.inferType e₂
+  Meta.forallTelescope ty₁ fun xs _ => do
+    let (ms, _, _) ← Meta.forallMetaTelescope ty₂
+    let e₁app := mkAppN e₁ xs
+    let e₂app := mkAppN e₂ ms
+    if ← Meta.isDefEq e₁app e₂app then
+      let e₂app ← instantiateMVars e₂app
+      let (e₂app, s) := AbstractMVars.abstractExprMVars e₂app { mctx := (← getMCtx), lctx := (← getLCtx), ngen := (← getNGen)}
+      setNGen s.ngen; setMCtx s.mctx
+      Meta.withLCtx s.lctx (← Meta.getLocalInstances) <| do
+        let proof ← Meta.mkLambdaFVars (xs ++ s.fvars) (← Meta.mkAppM ``Eq.refl #[e₁app])
+        let eq ← Meta.mkForallFVars (xs ++ s.fvars) (← Meta.mkAppM ``Eq #[e₁app, e₂app])
+        return (proof, eq)
+    else
+      return .none
+
 def Expr.formatWithUsername (e : Expr) : MetaM Format := do
   let fvarIds := (collectFVars {} e).fvarIds
   let names ← fvarIds.mapM (fun fid => do
@@ -338,103 +366,4 @@ open Meta in
         IO.println s!"{(← IO.monoMsNow) - startTime} ms"
   | _ => throwUnsupportedSyntax
 
-section EvalAtTermElabM
-
-  open Meta
-
-  private def mkEvalInstCore (evalClassName : Name) (e : Expr) : MetaM Expr := do
-    let α    ← inferType e
-    let u    ← getDecLevel α
-    let inst := mkApp (Lean.mkConst evalClassName [u]) α
-    try
-      synthInstance inst
-    catch _ =>
-      -- Put `α` in WHNF and try again
-      try
-        let α ← whnf α
-        synthInstance (mkApp (Lean.mkConst evalClassName [u]) α)
-      catch _ =>
-        -- Fully reduce `α` and try again
-        try
-          let α ← reduce (skipTypes := false) α
-          synthInstance (mkApp (Lean.mkConst evalClassName [u]) α)
-        catch _ =>
-          throwError "{decl_name%} :: expression{indentExpr e}\nhas type{indentExpr α}\nbut instance{indentExpr inst}\nfailed to be synthesized, this instance instructs Lean on how to display the resulting value, recall that any type implementing the `Repr` class also implements the `{evalClassName}` class"
-
-  private def mkRunMetaEval (e : Expr) : MetaM Expr :=
-    withLocalDeclD `env (mkConst ``Lean.Environment) fun env =>
-    withLocalDeclD `opts (mkConst ``Lean.Options) fun opts => do
-      let α ← inferType e
-      let u ← getDecLevel α
-      let instVal ← mkEvalInstCore ``Lean.MetaEval e
-      let e := mkAppN (mkConst ``Lean.runMetaEval [u]) #[α, instVal, env, opts, e]
-      instantiateMVars (← mkLambdaFVars #[env, opts] e)
-
-  private def mkRunEval (e : Expr) : MetaM Expr := do
-    let α ← inferType e
-    let u ← getDecLevel α
-    let instVal ← mkEvalInstCore ``Lean.Eval e
-    instantiateMVars (mkAppN (mkConst ``Lean.runEval [u]) #[α, instVal, mkSimpleThunk e])
-
-  unsafe def termElabEval (elabEvalTerm : Expr) : TermElabM Unit := do
-    let declName := `_eval
-    let addAndCompile (value : Expr) : TermElabM Unit := do
-      let value ← Term.levelMVarToParam (← instantiateMVars value)
-      let type ← inferType value
-      let us := collectLevelParams {} value |>.params
-      let value ← instantiateMVars value
-      let decl := Declaration.defnDecl {
-        name        := declName
-        levelParams := us.toList
-        type        := type
-        value       := value
-        hints       := ReducibilityHints.opaque
-        safety      := DefinitionSafety.unsafe
-      }
-      Term.ensureNoUnassignedMVars decl
-      addAndCompile decl
-    -- Elaborate `term`
-    -- Evaluate using term using `MetaEval` class.
-    let elabMetaEval : TermElabM Unit := do
-      -- act? is `some act` if elaborated `term` has type `TermElabM α`
-      let act? ← Term.withDeclName declName do
-        let e := elabEvalTerm
-        let eType ← instantiateMVars (← inferType e)
-        if eType.isAppOfArity ``TermElabM 1 then
-          let mut stx ← Term.exprToSyntax e
-          unless (← isDefEq eType.appArg! (mkConst ``Unit)) do
-            stx ← `($stx >>= fun v => IO.println (repr v))
-          let act ← Lean.Elab.Term.evalTerm (TermElabM Unit) (mkApp (mkConst ``TermElabM) (mkConst ``Unit)) stx
-          pure <| some act
-        else
-          let e ← mkRunMetaEval e
-          let env ← getEnv
-          let opts ← getOptions
-          let act ← try addAndCompile e; evalConst (Environment → Options → IO (String × Except IO.Error Environment)) declName finally setEnv env
-          let (out, res) ← act env opts -- we execute `act` using the environment
-          logInfo out
-          match res with
-          | Except.error e => throwError e.toString
-          | Except.ok env  => do setEnv env; pure none
-      let some act := act? | return ()
-      act
-    -- Evaluate using term using `Eval` class.
-    let elabEval : TermElabM Unit := Term.withDeclName declName do
-      -- fall back to non-meta eval if MetaEval hasn't been defined yet
-      -- modify e to `runEval e`
-      let e ← mkRunEval elabEvalTerm
-      let env ← getEnv
-      let act ← try addAndCompile e; evalConst (IO (String × Except IO.Error Unit)) declName finally setEnv env
-      let (out, res) ← liftM (m := IO) act
-      logInfo out
-      match res with
-      | Except.error e => throwError e.toString
-      | Except.ok _    => pure ()
-    if (← getEnv).contains ``Lean.MetaEval then do
-      elabMetaEval
-    else
-      elabEval
-
-end EvalAtTermElabM
-
 end Auto

Auto/Lib/MonadUtils.lean

@@ -116,7 +116,7 @@ where
       let fnBodyPre ← Meta.mkLambdaFVars xs fnBodyPre (usedOnly := true)
       let fnBody ← instantiateMVars fnBodyPre
       trace[auto.genMonadContext] "{getFnName}"
-      Elab.addDeclarationRanges getFnName stx
+      Elab.addDeclarationRangesFromSyntax getFnName stx
       addDefnitionValFromExpr fnBody getFnName
 
 private def elabGenMonadStateAux (m : Term) (stx : Syntax) : CommandElabM Unit := runTermElabM <| fun xs => do
@@ -149,7 +149,7 @@ where
       let fnBodyPre ← Meta.mkLambdaFVars xs fnBodyPre (usedOnly := true)
       let fnBody ← instantiateMVars fnBodyPre
       trace[auto.genMonadState] "{getFnName}"
-      Elab.addDeclarationRanges getFnName stx
+      Elab.addDeclarationRangesFromSyntax getFnName stx
       addDefnitionValFromExpr fnBody getFnName
   genMonadSets
       (xs : Array Expr) (stateTy : Expr) (stateMkExpr : Expr) (mstateInst : Expr)
@@ -170,7 +170,7 @@ where
           Meta.mkLambdaFVars #[f] modifyBody)
       let fnBody := ← instantiateMVars (← Meta.mkLambdaFVars xs fnBodyPre (usedOnly := true))
       trace[auto.genMonadState] "{setFnName}"
-      Elab.addDeclarationRanges setFnName stx
+      Elab.addDeclarationRangesFromSyntax setFnName stx
       addDefnitionValFromExpr fnBody setFnName
       fieldCnt := fieldCnt + 1
 

Auto/MathlibEmulator/DeriveToExpr.lean

@@ -167,7 +167,7 @@ def mkAuxFunction (ctx : Deriving.Context) (i : Nat) : TermElabM Command := do
     | _ => throwError "(internal error) expecting inst binder"
   let binders := header.binders.pop
     ++ (← mkToLevelBinders indVal)
-    ++ #[← addLevels header.binders.back]
+    ++ #[← addLevels header.binders.back!]
   let levels := indVal.levelParams.toArray.map mkIdent
   if ctx.usePartial then
     `(private partial def $(mkIdent auxFunName):ident.{$levels,*} $binders:bracketedBinder* :

Auto/Parser/LeanLex.lean

@@ -154,8 +154,8 @@ partial def ERE.brackets : ERE → Array EREBracket
 | .repGe e _     => e.brackets
 | .repLe e _     => e.brackets
 | .repGeLe e _ _ => e.brackets
-| .comp es       => (es.map ERE.brackets).concatMap id
-| .plus es       => (es.map ERE.brackets).concatMap id
+| .comp es       => (es.map ERE.brackets).flatMap id
+| .plus es       => (es.map ERE.brackets).flatMap id
 | .attr e s      => e.brackets
 
 partial def ERE.normalizeBrackets : ERE → ERE
@@ -236,7 +236,7 @@ section
     fun cg@⟨ngroup, all, _⟩ symbListToString =>
     let groups := cg.groups.mapIdx (
       fun idx c =>
-        s!"{idx.val} : {symbListToString c.toArray}"
+        s!"{idx} : {symbListToString c.toArray}"
     )
     let all := "CharGrouping ⦗⦗" ::
                s!"Number of groups := {ngroup}" ::
@@ -263,11 +263,11 @@ section
     fun ⟨d, cg⟩ symbListToString =>
       let dsnatS (s : Nat) (sn : _ × Nat) := s!"  ({s}, {sn.fst} → {sn.snd})"
       let dtr := d.tr.mapIdx (fun idx c => c.toArray.map (fun el => dsnatS idx el))
-      let dtr := dtr.concatMap id
+      let dtr := dtr.flatMap id
       let attrs := d.attrs.mapIdx (fun idx attrs => s!"  {idx} : {attrs.toList}")
       let cggroups := cg.groups.mapIdx (
         fun idx c =>
-          s!"  {idx.val} : {symbListToString c.toArray}"
+          s!"  {idx} : {symbListToString c.toArray}"
       )
       let cgalls := symbListToString cg.all.toArray
       let all := "ADFA ⦗⦗" ::

Auto/Parser/NDFA.lean

@@ -59,7 +59,7 @@ section NFA
       let snatS (s : Nat) (sn : _ × Array Nat) := s!"({s}, {us2s sn.fst} ↦ {sn.snd.toList})"
       let tr := n.tr.mapIdx (fun idx c =>
         c.toArray.map (fun el => snatS idx el))
-      let tr := tr.concatMap id
+      let tr := tr.flatMap id
       let attrs := n.attrs.mapIdx (fun idx attrs => s!"{idx} : {attrs.toList}")
       let all := "NFA ⦗⦗" :: s!"Accept state := {n.tr.size}" :: tr.toList ++ attrs.toList
       String.intercalate "\n  " all ++ "\n⦘⦘"
@@ -90,7 +90,7 @@ section NFA
       let mut cur := 0
       let mut ret := ss
       while front.size > 0 do
-        cur := front.back
+        cur := front.back!
         front := front.pop
         let curNexts := NFA.nextStatesOfState r cur (.inl .unit)
         for n in curNexts do
@@ -227,9 +227,9 @@ section NFA
           let new_a := a.tr.map (relocateHMap · off)
           new_a.push (Std.HashMap.empty.insert (.inl .unit) #[acc'])
         )
-      let new_tr := (#[#[initTrans]] ++ trs).concatMap id
+      let new_tr := (#[#[initTrans]] ++ trs).flatMap id
       let new_attrs := #[Std.HashSet.empty] ++
-                       (as.map (fun (⟨_, attrs⟩ : NFA σ) => attrs)).concatMap id ++
+                       (as.map (fun (⟨_, attrs⟩ : NFA σ) => attrs)).flatMap id ++
                        #[Std.HashSet.empty]
       NFA.mk new_tr new_attrs
 
@@ -308,9 +308,9 @@ section NFA
           -- Add an edge from initial state to new accept state
           new_r.modify 0 (fun hm => NFA.addEdgesToHMap hm (.inl .unit, #[acc']))
         )
-      let new_tr := new_trs.concatMap id
+      let new_tr := new_trs.flatMap id
       let new_attrs : Array (Std.HashSet String) :=
-        ((Array.mk (List.range (n - 1))).map (fun _ => r.attrs[:r.tr.size].toArray)).concatMap id ++
+        ((Array.mk (List.range (n - 1))).map (fun _ => r.attrs[:r.tr.size].toArray)).flatMap id ++
         r.attrs
       NFA.mk new_tr new_attrs
 
@@ -326,7 +326,7 @@ section NFA
 
   /-- An `NFA UInt32` that accepts exactly a string -/
   def NFA.ofSymbComp (s : Array σ) : NFA σ :=
-    let tr := (Array.mk s.toList).mapIdx (fun idx c => Std.HashMap.empty.insert (.inr c) #[idx.val + 1])
+    let tr := (Array.mk s.toList).mapIdx (fun idx c => Std.HashMap.empty.insert (.inr c) #[idx + 1])
     let attrs := Array.mk ((List.range (s.size + 1)).map (fun _ => .empty))
     NFA.mk tr attrs
 
@@ -397,7 +397,7 @@ section DFA
   def DFA.toString (d : DFA σ) : String :=
     let snatS (s : Nat) (sn : σ × Nat) := s!"({s}, {sn.fst} → {sn.snd})"
     let tr := d.tr.mapIdx (fun idx c => c.toArray.map (fun el => snatS idx el))
-    let tr := tr.concatMap id
+    let tr := tr.flatMap id
     let attrs := d.attrs.mapIdx (fun idx attrs => s!"{idx} : {attrs.toList}")
     let all := "DFA ⦗⦗" ::
                s!"Accept states := {d.accepts.toList}" ::
@@ -465,7 +465,7 @@ section DFA
           | .inr .unit => (s, tr.size)
       ))
     )
-    let accepts := dstates.mapIdx (fun idx l => if l.contains n.tr.size then some idx.val else none)
+    let accepts := dstates.mapIdx (fun idx l => if l.contains n.tr.size then some idx else none)
     let accepts := accepts.foldl (fun hs o => if let some x := o then hs.insert x else hs) Std.HashSet.empty
     let attrs := dstates.map (fun l =>
       (Array.mk l).foldl (fun acc s => if let some x := n.attrs[s]? then acc.insertMany x else acc) Std.HashSet.empty)

Auto/Parser/SMTParser.lean

@@ -369,7 +369,7 @@ partial def parseForall (vs : List Term) (symbolMap : Std.HashMap String Expr) :
   let [app sortedVars, forallBody] := vs
     | throwError "parseForall :: Unexpected input list {vs}"
   let sortedVars ← sortedVars.mapM (fun sv => parseSortedVar sv symbolMap)
-  let sortedVarsWithIndices := sortedVars.mapIdx (fun idx val => (val, idx))
+  let sortedVarsWithIndices := sortedVars.mapFinIdx (fun idx val => (val, idx))
   let mut curPropBoolChoice := some $ (sortedVarsWithIndices.filter (fun ((_, t), _) => t.isProp)).map (fun (_, idx) => (idx, false))
   let mut possibleSortedVars := #[]
   while curPropBoolChoice.isSome do
@@ -405,7 +405,7 @@ partial def parseExists (vs : List Term) (symbolMap : Std.HashMap String Expr) :
   let [app sortedVars, existsBody] := vs
     | throwError "parseExists :: Unexpected input list {vs}"
   let sortedVars ← sortedVars.mapM (fun sv => parseSortedVar sv symbolMap)
-  let sortedVarsWithIndices := sortedVars.mapIdx (fun idx val => (val, idx))
+  let sortedVarsWithIndices := sortedVars.mapFinIdx (fun idx val => (val, idx))
   let mut curPropBoolChoice := some $ (sortedVarsWithIndices.filter (fun ((_, t), _) => t.isProp)).map (fun (_, idx) => (idx, false))
   let mut possibleSortedVars := #[]
   while curPropBoolChoice.isSome do
@@ -569,7 +569,7 @@ partial def parseTerm (e : Term) (symbolMap : Std.HashMap String Expr) (parseTer
         throwError "parseTerm :: Tester applied not {testerArg} of type {idtType} which is not an inductive datatype"
       let ctorType ← inferType parsedCtor
       let ctorArgTypes := (getForallArgumentTypes ctorType).toArray
-      withLocalDeclsD (ctorArgTypes.mapIdx fun idx ty => ((.str .anonymous ("arg" ++ idx.1.repr)), fun _ => pure ty)) fun ctorArgs => do
+      withLocalDeclsD (ctorArgTypes.mapFinIdx fun idx ty => ((.str .anonymous ("arg" ++ idx.1.repr)), fun _ => pure ty)) fun ctorArgs => do
         let mut res ← mkAppM ``Eq #[parsedTesterArg, ← mkAppM' parsedCtor ctorArgs]
         for ctorArg in ctorArgs do
           res ← mkLambdaFVars #[ctorArg] res