Update to v4.29.0

Author: JOSHCLUNE

Auto/Embedding/LamBase.lean

@@ -4094,7 +4094,6 @@ theorem LamWF.interp_bvarAppsRev
       (pushLCtxsDep_substxs _ _ _ List.reverse_cons HList.reverse_cons)]
     rw [interp_substLCtxTerm_rec
       (pushLCtxs_append_singleton _ _ _) (pushLCtxsDep_append_singleton _ _ _)]
-    rw [LamWF.interp_substWF (wf':=wfAp)]
     apply IH (LamWF.ofApp _ wft LamWF.bvarAppsRev_Aux)
     simp only[interp]; apply HEq.trans (b:=LamSort.curry valPre lterm) <;> try rfl
     case h₁ =>
@@ -4135,7 +4134,16 @@ theorem LamWF.interp_eqForallEFN'
       enter [2]; rw [IsomType.eqForall HList.cons_IsomType]; rw [Prod.eqForall']
       unfold HList.cons_IsomType; dsimp; enter [xs, x]
     apply forall_congr; intro xs
-    rw [interp_app, interp_base, interp_lam, eq_of_heq (LamBaseTerm.interp_equiv _ _)]
+    let wf' : LamWF lval.toLamTyVal
+      ⟨pushLCtx s (pushLCtxs ls lctx), t, LamSort.base LamBaseSort.prop⟩ := by
+      simpa [pushLCtxs_cons] using wf
+    have lhsRw :
+      (interp lval (pushLCtxs ls lctx) (pushLCtxsDep xs lctxTerm) wfMkF.fromMkForallEFN').down =
+      (interp lval (pushLCtxs ls lctx) (pushLCtxsDep xs lctxTerm) (LamWF.mkForallEF wf')).down := by
+      apply congrArg GLift.down
+      simpa using LamWF.interp_substWF
+    rw [lhsRw]
+    apply Eq.trans LamWF.interp_eqForallEF
     apply forall_congr; intro x
     apply congrArg; apply eq_of_heq; apply interp_heq <;> try rfl
     case HLCtxTyEq => rw [pushLCtxs_cons]
@@ -4202,8 +4210,9 @@ theorem LamWF.interp_insertEVarAt_eIdx
   let lval' := {lval with lamEVarTy := replaceAt ty pos lamEVarTy',
                           eVarVal := replaceAtDep val pos eVarVal'}
   HEq (lwf.interp lval' lctxTy lctxTerm) val := by
-  cases lwf; simp only [interp, replaceAt, replaceAtDep]
-  rw [Nat.beq_refl]; rfl
+  cases lwf; unfold interp replaceAt replaceAtDep
+  simp only [replaceAt, id_eq, Lean.Elab.WF.paramLet, interp]
+  rw [Nat.beq_refl]
 
 theorem LamWF.interp_eVarIrrelevance
   (lval₁ : LamValuation.{u}) (lval₂ : LamValuation.{u})

Auto/Embedding/LamChecker.lean

@@ -159,7 +159,7 @@ section CVal
     ∀ (n : Nat), ILLift.{u} ((lamILTy n).interp tyVal) :=
     fun n => ILLift.default ((lamILTy n).interp tyVal)
 
-  def CVal.toLamTyVal (cv : CVal.{u} levt) : LamTyVal :=
+  noncomputable def CVal.toLamTyVal (cv : CVal.{u} levt) : LamTyVal :=
     ⟨fun n => ((cv.var.get? n).getD ⟨.base .prop, GLift.up False⟩).fst,
      fun n => ((cv.il.get? n).getD ⟨.base .prop, ILLift.default _⟩).fst,
      fun n => (levt.get? n).getD (.base .prop)⟩
@@ -173,15 +173,15 @@ section CVal
   def CPVal.toLamVarTy (cpv : CPVal.{u}) : Nat → LamSort :=
     fun n => ((cpv.var.get? n).getD ⟨.base .prop, GLift.up False⟩).fst
 
-  def CPVal.toLamILTy (cpv : CPVal.{u}) : Nat → LamSort :=
+  noncomputable def CPVal.toLamILTy (cpv : CPVal.{u}) : Nat → LamSort :=
     fun n => ((cpv.il.get? n).getD ⟨.base .prop, ILLift.default _⟩).fst
 
-  def CPVal.toLamTyValWithLamEVarTy (cpv : CPVal.{u}) (levt : Nat → LamSort) : LamTyVal :=
+  noncomputable def CPVal.toLamTyValWithLamEVarTy (cpv : CPVal.{u}) (levt : Nat → LamSort) : LamTyVal :=
     ⟨fun n => ((cpv.var.get? n).getD ⟨.base .prop, GLift.up False⟩).fst,
      fun n => ((cpv.il.get? n).getD ⟨.base .prop, ILLift.default _⟩).fst,
      levt⟩
 
-  def CPVal.toLamTyValEraseEtom (cpv : CPVal.{u}) : LamTyVal :=
+  noncomputable def CPVal.toLamTyValEraseEtom (cpv : CPVal.{u}) : LamTyVal :=
     ⟨fun n => ((cpv.var.get? n).getD ⟨.base .prop, GLift.up False⟩).fst,
      fun n => ((cpv.il.get? n).getD ⟨.base .prop, ILLift.default _⟩).fst,
      fun _ => .base .prop⟩
@@ -422,7 +422,7 @@ abbrev importTablePSigmaβ (cpv : CPVal.{u}) (ie : ImportEntry) :=
 abbrev importTablePSigmaMk (cpv : CPVal.{u}) :=
   @PSigma.mk ImportEntry (importTablePSigmaβ cpv)
 
-def ImportTable.importFacts (it : ImportTable cpv) : BinTree REntry :=
+noncomputable def ImportTable.importFacts (it : ImportTable cpv) : BinTree REntry :=
   it.mapOpt (fun ⟨ie, _⟩ =>
     match ie with
     | .valid p =>
@@ -2345,7 +2345,7 @@ theorem ChkSteps.run_correct
   dsimp [ChkSteps.run]; apply BinTree.foldl_inv (fun (r : RTable) => ∃ eV', RTable.inv r ⟨cpv, eV'⟩) inv
   intro r' (c, n) inv'; exact ChkStep.run_correct r' cpv inv' c n
 
-def ChkSteps.runFromBeginning (cpv : CPVal.{u}) (it : ImportTable cpv) (cs : ChkSteps) :=
+noncomputable def ChkSteps.runFromBeginning (cpv : CPVal.{u}) (it : ImportTable cpv) (cs : ChkSteps) :=
   ChkSteps.run cpv.toLamVarTy cpv.toLamILTy ⟨it.importFacts, 0, .leaf⟩ cs
 
 /--

Auto/Embedding/LamSystem.lean

@@ -522,7 +522,7 @@ theorem LamValid.intro1H (H : LamValid lval lctx (.mkForallE s t)) :
     have ⟨wfF, hF⟩ := H
     have .ofApp _ (.ofBase (.ofForallE _)) wft := wfF
     ⟨.mkForallEF (.ofApp _ (.bvarLift _ wft) .pushLCtx_ofBVar), fun lctxTerm => by
-      simp only [LamWF.mkForallEF, LamWF.interp, LamBaseTerm.LamWF.interp]
+      simp only [LamWF.mkForallEF]
       intro x; simp only [LamWF.pushLCtx_ofBVar, LamWF.interp, eq_mp_eq_cast, cast_eq, id_eq]
       apply Eq.mp _ (hF lctxTerm x); apply congrArg; rw [← LamWF.interp_bvarLift]⟩
   )

Auto/Embedding/LamTermInterp.lean

@@ -263,7 +263,23 @@ structure State where
 
 abbrev InterpM := StateRefT State MetaState.MetaStateM
 
-#genMonadState InterpM
+def getSortFVars : InterpM (Array FVarId) := do
+  return (← get).sortFVars
+
+def setSortFVars (sortFVars : Array FVarId) : InterpM Unit := do
+  modify fun s => { s with sortFVars := sortFVars }
+
+def getSortMap : InterpM (Std.HashMap LamSort FVarId) := do
+  return (← get).sortMap
+
+def setSortMap (sortMap : Std.HashMap LamSort FVarId) : InterpM Unit := do
+  modify fun s => { s with sortMap := sortMap }
+
+def getLctxTyRev : InterpM (Array LamSort) := do
+  return (← get).lctxTyRev
+
+def setLctxTyRev (lctxTyRev : Array LamSort) : InterpM Unit := do
+  modify fun s => { s with lctxTyRev := lctxTyRev }
 
 def getLCtxTy! (idx : Nat) : InterpM LamSort := do
   let lctxTyRev ← getLctxTyRev

Auto/IR/SMT.lean

@@ -438,8 +438,7 @@ section
 
   @[always_inline]
   instance : Monad (TransM ω φ) :=
-    let i := inferInstanceAs (Monad (TransM ω φ));
-    { pure := i.pure, bind := i.bind }
+    inferInstance
 
   instance : Inhabited (TransM ω φ α) where
     default := fun _ => throw default
@@ -453,7 +452,41 @@ section
   @[inline] def TransM.run' (x : TransM ω φ α) (s : State ω φ := {}) : MetaM α :=
     Prod.fst <$> StateRefT'.run x s
 
-  #genMonadState (TransM ω φ)
+  def getH2lMap : TransM ω φ (Std.HashMap ω String) := do
+    return (← get).h2lMap
+
+  def setH2lMap (h2lMap : Std.HashMap ω String) : TransM ω φ Unit := do
+    modify fun s => { s with h2lMap := h2lMap }
+
+  def getL2hMap : TransM ω φ (Std.HashMap String ω) := do
+    return (← get).l2hMap
+
+  def setL2hMap (l2hMap : Std.HashMap String ω) : TransM ω φ Unit := do
+    modify fun s => { s with l2hMap := l2hMap }
+
+  def getUsedNames : TransM ω φ (Std.HashMap String Nat) := do
+    return (← get).usedNames
+
+  def setUsedNames (usedNames : Std.HashMap String Nat) : TransM ω φ Unit := do
+    modify fun s => { s with usedNames := usedNames }
+
+  def getWfPredicatesMap : TransM ω φ (Std.HashMap φ (Option String)) := do
+    return (← get).wfPredicatesMap
+
+  def setWfPredicatesMap (wfPredicatesMap : Std.HashMap φ (Option String)) : TransM ω φ Unit := do
+    modify fun s => { s with wfPredicatesMap := wfPredicatesMap }
+
+  def getWfPredicatesInvMap : TransM ω φ (Std.HashMap String φ) := do
+    return (← get).wfPredicatesInvMap
+
+  def setWfPredicatesInvMap (wfPredicatesInvMap : Std.HashMap String φ) : TransM ω φ Unit := do
+    modify fun s => { s with wfPredicatesInvMap := wfPredicatesInvMap }
+
+  def getCommands : TransM ω φ (Array Command) := do
+    return (← get).commands
+
+  def setCommands (commands : Array Command) : TransM ω φ Unit := do
+    modify fun s => { s with commands := commands }
 
   def getMapSize : TransM ω φ Nat := do
     let size := (← getH2lMap).size

Auto/Lib/MetaState.lean

@@ -14,7 +14,7 @@ structure SavedState where
 abbrev MetaStateM := StateRefT State CoreM
 
 @[always_inline]
-instance : Monad MetaStateM := let i := inferInstanceAs (Monad MetaStateM); { pure := i.pure, bind := i.bind }
+instance : Monad MetaStateM := inferInstance
 
 instance : MonadLCtx MetaStateM where
   getLCtx := return (← get).toContext.lctx
@@ -42,7 +42,17 @@ instance : MonadBacktrack SavedState MetaStateM where
   saveState      := MetaState.saveState
   restoreState s := s.restore
 
-#genMonadState MetaStateM
+def getToState : MetaStateM Meta.State := do
+  return (← get).toState
+
+def setToState (st : Meta.State) : MetaStateM Unit := do
+  modify fun s => { s with toState := st }
+
+def getToContext : MetaStateM Meta.Context := do
+  return (← get).toContext
+
+def setToContext (ctx : Meta.Context) : MetaStateM Unit := do
+  modify fun s => { s with toContext := ctx }
 
 def runMetaM (n : MetaM α) : MetaStateM α := do
   let s ← get

Auto/Lib/ToExprExtra.lean

@@ -23,6 +23,7 @@ scoped instance : ToExpr Int where
   We require that `toExpr (self:=instExprToExprId (.const ``Nat [])) l₂ ≝ l₁`
   It is obvious that this shouldn't be marked as an `instance`
 -/
+@[reducible]
 def instExprToExprId (ty : Expr) : ToExpr Expr :=
   { toExpr := id, toTypeExpr := ty}
 

Auto/MathlibEmulator/ToLevel.lean

@@ -35,10 +35,12 @@ instance [ToLevel.{u}] : ToLevel.{u+1} where
   toLevel := .succ toLevel.{u}
 
 /-- `ToLevel` for `max u v`. This is not an instance since it causes divergence. -/
+@[reducible]
 def ToLevel.max [ToLevel.{u}] [ToLevel.{v}] : ToLevel.{max u v} where
   toLevel := .max toLevel.{u} toLevel.{v}
 
 /-- `ToLevel` for `imax u v`. This is not an instance since it causes divergence. -/
+@[reducible]
 def ToLevel.imax [ToLevel.{u}] [ToLevel.{v}] : ToLevel.{imax u v} where
   toLevel := .imax toLevel.{u} toLevel.{v}
 

Auto/Translation/Inductive.lean

@@ -85,7 +85,17 @@ structure CollectInduct.State where
 
 abbrev IndCollectM := StateRefT CollectInduct.State MetaM
 
-#genMonadState IndCollectM
+def getRecorded : IndCollectM (Std.HashMap Name (Array Expr)) := do
+  return (← get).recorded
+
+def setRecorded (recorded : Std.HashMap Name (Array Expr)) : IndCollectM Unit := do
+  modify fun s => { s with recorded := recorded }
+
+def getSis : IndCollectM (Array (Array SimpleIndVal)) := do
+  return (← get).sis
+
+def setSis (sis : Array (Array SimpleIndVal)) : IndCollectM Unit := do
+  modify fun s => { s with sis := sis }
 
 private def collectSimpleInduct
   (tyctor : Name) (lvls : List Level) (args : Array Expr) : MetaM SimpleIndVal := do

Auto/Translation/Lam2DAtomAsFVar.lean

@@ -64,7 +64,44 @@ def ExternM.run (m : ExternM α) (s : State) : MetaStateM (α × State) :=
 def ExternM.run' (m : ExternM α) (s : State) : MetaStateM α :=
   StateRefT'.run' m s
 
-#genMonadState ExternM
+def getTyVal : ExternM (Array (Expr × Level)) := do
+  return (← get).tyVal
+
+def getVarVal : ExternM (Array (Expr × LamSort)) := do
+  return (← get).varVal
+
+def getLamEVarTy : ExternM (Array LamSort) := do
+  return (← get).lamEVarTy
+
+def getAtomsToAbstract : ExternM (Array (FVarId × Expr)) := do
+  return (← get).atomsToAbstract
+
+def setAtomsToAbstract (atomsToAbstract : Array (FVarId × Expr)) : ExternM Unit := do
+  modify fun s => { s with atomsToAbstract := atomsToAbstract }
+
+def getEtomsToAbstract : ExternM (Array (FVarId × Nat)) := do
+  return (← get).etomsToAbstract
+
+def setEtomsToAbstract (etomsToAbstract : Array (FVarId × Nat)) : ExternM Unit := do
+  modify fun s => { s with etomsToAbstract := etomsToAbstract }
+
+def getTypeAtomFVars : ExternM (Std.HashMap Nat Expr) := do
+  return (← get).typeAtomFVars
+
+def setTypeAtomFVars (typeAtomFVars : Std.HashMap Nat Expr) : ExternM Unit := do
+  modify fun s => { s with typeAtomFVars := typeAtomFVars }
+
+def getTermAtomFVars : ExternM (Std.HashMap Nat Expr) := do
+  return (← get).termAtomFVars
+
+def setTermAtomFVars (termAtomFVars : Std.HashMap Nat Expr) : ExternM Unit := do
+  modify fun s => { s with termAtomFVars := termAtomFVars }
+
+def getEtomFVars : ExternM (Std.HashMap Nat Expr) := do
+  return (← get).etomFVars
+
+def setEtomFVars (etomFVars : Std.HashMap Nat Expr) : ExternM Unit := do
+  modify fun s => { s with etomFVars := etomFVars }
 
 def withTypeAtomsAsFVar (atoms : Array Nat) : ExternM Unit :=
   for atom in atoms do