fix: propagate Simp.Config when reducing terms and checking definitional equality in simp

src/Init/Data/Array/Basic.lean

@@ -801,7 +801,7 @@ decreasing_by simp_wf; exact Nat.sub_succ_lt_self _ _ h
   induction a, i, h using Array.eraseIdx.induct with
   | @case1 a i h h' a' ih =>
     unfold eraseIdx
-    simp [h', a', ih]
+    simp +zetaDelta [h', a', ih]
   | case2 a i h h' =>
     unfold eraseIdx
     simp [h']

src/Init/Data/List/Impl.lean

@@ -332,7 +332,7 @@ def enumFromTR (n : Nat) (l : List α) : List (Nat × α) :=
       rw [← show _ + as.length = n + (a::as).length from Nat.succ_add .., foldr, go as]
       simp [enumFrom, f]
   rw [← Array.foldr_toList]
-  simp [go]
+  simp +zetaDelta [go]
 
 /-! ## Other list operations -/
 

src/Lean/Data/RArray.lean

@@ -55,7 +55,7 @@ where
   go lb ub h1 h2 : (ofFn.go f lb ub h1 h2).size = ub - lb := by
     induction lb, ub, h1, h2 using RArray.ofFn.go.induct (f := f) (n := n)
     case case1 => simp [ofFn.go, size]; omega
-    case case2 ih1 ih2 hiu => rw [ofFn.go]; simp [size, *]; omega
+    case case2 ih1 ih2 hiu => rw [ofFn.go]; simp +zetaDelta [size, *]; omega
 
 section Meta
 open Lean

src/Lean/Elab/PatternVar.lean

@@ -159,7 +159,7 @@ private def processVar (idStx : Syntax) : M Syntax := do
 private def samePatternsVariables (startingAt : Nat) (s₁ s₂ : State) : Bool := Id.run do
   if h₁ : s₁.vars.size = s₂.vars.size then
     for h₂ : i in [startingAt:s₁.vars.size] do
-      if s₁.vars[i] != s₂.vars[i]'(by obtain ⟨_, y⟩ := h₂; simp_all) then return false
+      if s₁.vars[i] != s₂.vars[i]'(by obtain ⟨_, y⟩ := h₂; simp_all +zetaDelta) then return false
     true
   else
     false

src/Lean/Meta/Basic.lean

@@ -187,7 +187,7 @@ structure Config where
   Zeta-delta reduction: given a local context containing entry `x : t := e`, free variable `x` reduces to `e`.
   -/
   zetaDelta : Bool := true
-  deriving Inhabited
+  deriving Inhabited, Repr
 
 /-- Convert `isDefEq` and `WHNF` relevant parts into a key for caching results -/
 private def Config.toKey (c : Config) : UInt64 :=

src/Lean/Meta/ExprDefEq.lean

@@ -380,12 +380,13 @@ private def checkTypesAndAssign (mvar : Expr) (v : Expr) : MetaM Bool :=
     else
       -- must check whether types are definitionally equal or not, before assigning and returning true
       let mvarType ← inferType mvar
-      let vType ← inferType v
-      if (← withTransparency TransparencyMode.default <| Meta.isExprDefEqAux mvarType vType) then
-        mvar.mvarId!.assign v
-        pure true
-      else
-        pure false
+      withInferTypeConfig do
+        let vType ← inferType v
+        if (← Meta.isExprDefEqAux mvarType vType) then
+          mvar.mvarId!.assign v
+          pure true
+        else
+          pure false
 
 /--
 Auxiliary method for solving constraints of the form `?m xs := v`.

src/Lean/Meta/InferType.lean

@@ -177,15 +177,20 @@ private def inferFVarType (fvarId : FVarId) : MetaM Expr := do
         modifyInferTypeCache fun c => c.insert key type
       return type
 
-private def defaultConfig : ConfigWithKey :=
-  { : Config }.toConfigWithKey
-
-private def allConfig : ConfigWithKey :=
-  { transparency := .all : Config }.toConfigWithKey
+/--
+Ensure `MetaM` configuration is strong enough for inferring/checking types.
+For example, `beta := true` is essential when type checking.
 
-@[inline] def withInferTypeConfig (x : MetaM α) : MetaM α := do
-  let cfg := if (← getTransparency) == .all then allConfig else defaultConfig
-  withConfigWithKey cfg x
+Remark: we previously use the default configuration here, but this is problematic
+because it overrides unrelated configurations.
+-/
+@[inline] def withInferTypeConfig (x : MetaM α) : MetaM α :=
+  withAtLeastTransparency .default do
+    let cfg ← getConfig
+    if cfg.beta && cfg.iota && cfg.zeta && cfg.zetaDelta && cfg.proj == .yesWithDelta then
+      x
+    else
+      withConfig (fun cfg => { cfg with beta := true, iota := true, zeta := true, zetaDelta := true, proj := .yesWithDelta }) x
 
 @[export lean_infer_type]
 def inferTypeImp (e : Expr) : MetaM Expr :=

src/Lean/Meta/Tactic/Simp/Main.lean

@@ -57,7 +57,7 @@ private def reduceProjFn? (e : Expr) : SimpM (Option Expr) := do
         match e? with
         | none   => pure none
         | some e =>
-          match (← reduceProj? e.getAppFn) with
+          match (← withSimpMetaConfig <| reduceProj? e.getAppFn) with
           | some f => return some (mkAppN f e.getAppArgs)
           | none   => return none
       if projInfo.fromClass then
@@ -152,7 +152,7 @@ private def unfold? (e : Expr) : SimpM (Option Expr) := do
       withDefault <| unfoldDefinition? e
     else if (← isMatchDef fName) then
       let some value ← withDefault <| unfoldDefinition? e | return none
-      let .reduced value ← reduceMatcher? value | return none
+      let .reduced value ← withSimpMetaConfig <| reduceMatcher? value | return none
       return some value
     else
       return none
@@ -166,6 +166,7 @@ private def reduceStep (e : Expr) : SimpM Expr := do
   let f := e.getAppFn
   if f.isMVar then
     return (← instantiateMVars e)
+  withSimpMetaConfig do
   if cfg.beta then
     if f.isHeadBetaTargetFn false then
       return f.betaRev e.getAppRevArgs
@@ -256,7 +257,7 @@ def withNewLemmas {α} (xs : Array Expr) (f : SimpM α) : SimpM α := do
     withFreshCache do f
 
 def simpProj (e : Expr) : SimpM Result := do
-  match (← reduceProj? e) with
+  match (← withSimpMetaConfig <| reduceProj? e) with
   | some e => return { expr := e }
   | none =>
     let s := e.projExpr!
@@ -484,7 +485,7 @@ def processCongrHypothesis (h : Expr) : SimpM Bool := do
     let rhs := hType.appArg!
     rhs.withApp fun m zs => do
       let val ← mkLambdaFVars zs r.expr
-      unless (← isDefEq m val) do
+      unless (← withSimpMetaConfig <| isDefEq m val) do
         throwCongrHypothesisFailed
       let mut proof ← r.getProof
       if hType.isAppOf ``Iff then
@@ -528,7 +529,7 @@ def trySimpCongrTheorem? (c : SimpCongrTheorem) (e : Expr) : SimpM (Option Resul
     let args := e.getAppArgs
     e := mkAppN e.getAppFn args[:numArgs]
     extraArgs := args[numArgs:].toArray
-  if (← isDefEq lhs e) then
+  if (← withSimpMetaConfig <| isDefEq lhs e) then
     let mut modified := false
     for i in c.hypothesesPos do
       let x := xs[i]!

src/Lean/Meta/Tactic/Simp/Rewrite.lean

@@ -117,7 +117,7 @@ private def useImplicitDefEqProof (thm : SimpTheorem) : SimpM Bool := do
 private def tryTheoremCore (lhs : Expr) (xs : Array Expr) (bis : Array BinderInfo) (val : Expr) (type : Expr) (e : Expr) (thm : SimpTheorem) (numExtraArgs : Nat) : SimpM (Option Result) := do
   recordTriedSimpTheorem thm.origin
   let rec go (e : Expr) : SimpM (Option Result) := do
-    if (← isDefEq lhs e) then
+    if (← withSimpMetaConfig <| isDefEq lhs e) then
       unless (← synthesizeArgs thm.origin bis xs) do
         return none
       let proof? ← if (← useImplicitDefEqProof thm) then
@@ -342,7 +342,7 @@ def simpMatchCore (matcherName : Name) (e : Expr) : SimpM Step := do
 def simpMatch : Simproc := fun e => do
   unless (← getConfig).iota do
     return .continue
-  if let some e ← reduceRecMatcher? e then
+  if let some e ← withSimpMetaConfig <| reduceRecMatcher? e then
     return .visit { expr := e }
   let .const declName _ := e.getAppFn
     | return .continue
@@ -549,7 +549,7 @@ private def dischargeUsingAssumption? (e : Expr) : SimpM (Option Expr) := do
     -- well-behaved discharger. See comment at `Methods.wellBehavedDischarge`
     else if !contextual && localDecl.index >= lctxInitIndices then
       return none
-    else if (← isDefEq e localDecl.type) then
+    else if (← withSimpMetaConfig <| isDefEq e localDecl.type) then
       return some localDecl.toExpr
     else
       return none
@@ -591,7 +591,7 @@ def dischargeRfl (e : Expr) : SimpM (Option Expr) := do
   forallTelescope e fun xs e => do
     let some (t, a, b) := e.eq? | return .none
     unless a.getAppFn.isMVar || b.getAppFn.isMVar do return .none
-    if (← withReducible <| isDefEq a b) then
+    if (← withSimpMetaConfig <| isDefEq a b) then
       trace[Meta.Tactic.simp.discharge] "Discharging with rfl: {e}"
       let u ← getLevel t
       let proof := mkApp2 (.const ``rfl [u]) t a

src/Lean/Meta/Tactic/Simp/Types.lean

@@ -122,18 +122,33 @@ private def updateArith (c : Config) : CoreM Config := do
 /--
 Converts `Simp.Config` into `Meta.ConfigWithKey` used for indexing.
 -/
-private def mkIndexConfig (c : Config) : ConfigWithKey :=
-  { c with
+private def mkIndexConfig (c : Config) : MetaM ConfigWithKey := do
+  let curr ← Meta.getConfig
+  return { curr with
+    beta         := c.beta
+    iota         := c.iota
+    zeta         := c.zeta
+    zetaDelta    := c.zetaDelta
+    etaStruct    := c.etaStruct
+    /-
+    When indexing terms we disable projection to ensure a term such as `f ((a, b).1)`
+    is an instance of the pattern `f (?x.1)`
+    -/
     proj         := .no
     transparency := .reducible
   : Meta.Config }.toConfigWithKey
 
 /--
 Converts `Simp.Config` into `Meta.ConfigWithKey` used for `isDefEq`.
 -/
--- TODO: use `metaConfig` at `isDefEq`. It is not being used yet because it will break Mathlib.
-private def mkMetaConfig (c : Config) : ConfigWithKey :=
-  { c with
+private def mkMetaConfig (c : Config) : MetaM ConfigWithKey := do
+  let curr ← Meta.getConfig
+  return { curr with
+    beta         := c.beta
+    iota         := c.iota
+    zeta         := c.zeta
+    zetaDelta    := c.zetaDelta
+    etaStruct    := c.etaStruct
     proj         := if c.proj then .yesWithDelta else .no
     transparency := .reducible
   : Meta.Config }.toConfigWithKey
@@ -142,12 +157,16 @@ def mkContext (config : Config := {}) (simpTheorems : SimpTheoremsArray := {}) (
   let config ← updateArith config
   return {
     config, simpTheorems, congrTheorems
-    metaConfig := mkMetaConfig config
-    indexConfig := mkIndexConfig config
+    metaConfig := (← mkMetaConfig config)
+    indexConfig := (← mkIndexConfig config)
   }
 
-def Context.setConfig (context : Context) (config : Config) : Context :=
-  { context with config }
+def Context.setConfig (context : Context) (config : Config) : MetaM Context := do
+  return { context with
+    config
+    metaConfig := (← mkMetaConfig config)
+    indexConfig := (← mkIndexConfig config)
+  }
 
 def Context.setSimpTheorems (c : Context) (simpTheorems : SimpTheoremsArray) : Context :=
   { c with simpTheorems }
@@ -237,6 +256,12 @@ For example, if the user has set `simp (config := { zeta := false })`,
 @[inline] def withSimpIndexConfig (x : SimpM α) : SimpM α := do
   withConfigWithKey (← readThe Simp.Context).indexConfig x
 
+/--
+Executes `x` using a `MetaM` configuration for inferred from `Simp.Config`.
+-/
+@[inline] def withSimpMetaConfig (x : SimpM α) : SimpM α := do
+  withConfigWithKey (← readThe Simp.Context).metaConfig x
+
 @[extern "lean_simp"]
 opaque simp (e : Expr) : SimpM Result
 

src/Lean/Meta/WHNF.lean

@@ -572,7 +572,17 @@ where
             return (← go <| mkAppN (b.instantiate1 v) args)
         let f := f.getAppFn
         let f' ← go f
-        if cfg.beta && f'.isLambda then
+        /-
+        If `f'` is a lambda, then we perform beta-reduction here IF
+        1- `cfg.beta` is enabled, OR
+        2- `f` was not a lambda expression. That is, `f` was reduced, and the beta-reduction step is part
+           of this step. This is similar to allowing beta-reduction while unfolding expressions even if `cfg.beta := false`.
+
+        We added case 2 because a failure at `norm_cast`. See test `6123_mod_cast.lean`.
+        Another possible fix to this test is to set `beta := true` at the `Simp.Config` value at
+        `NormCast.lean`.
+        -/
+        if f'.isLambda && (cfg.beta || !f.isLambda) then
           let revArgs := e.getAppRevArgs
           go <| f'.betaRev revArgs
         else if let some eNew ← whnfDelayedAssigned? f' e then

src/Std/Sat/AIG/Basic.lean

@@ -471,7 +471,7 @@ def mkGate (aig : AIG α) (input : GateInput aig) : Entrypoint α :=
       have := input.lhs.ref.hgate
       have := input.rhs.ref.hgate
       omega
-  ⟨{ aig with decls, invariant, cache }, ⟨g, by simp [decls]⟩⟩
+  ⟨{ aig with decls, invariant, cache }, ⟨g, by simp [g, decls]⟩⟩
 
 /--
 Add a new input node to the AIG in `aig`. Note that this version is only meant for proving,
@@ -487,7 +487,7 @@ def mkAtom (aig : AIG α) (n : α) : Entrypoint α :=
     split at h2
     · apply aig.invariant <;> assumption
     · contradiction
-  ⟨{ decls, invariant, cache }, ⟨g, by simp [decls]⟩⟩
+  ⟨{ decls, invariant, cache }, ⟨g, by simp [g, decls]⟩⟩
 
 /--
 Add a new constant node to `aig`. Note that this version is only meant for proving,
@@ -503,7 +503,7 @@ def mkConst (aig : AIG α) (val : Bool) : Entrypoint α :=
     split at h2
     · apply aig.invariant <;> assumption
     · contradiction
-  ⟨{ decls, invariant, cache }, ⟨g, by simp [decls]⟩⟩
+  ⟨{ decls, invariant, cache }, ⟨g, by simp [g, decls]⟩⟩
 
 end AIG
 

src/Std/Sat/AIG/CNF.lean

@@ -505,7 +505,7 @@ def State.addConst (state : State aig) (idx : Nat) (h : idx < aig.decls.size)
   let newCnf := Decl.constToCNF (.inr ⟨idx, h⟩) b
   have hinv := toCNF.State.Inv_constToCNF htip
   let ⟨cache, hcache⟩ := cache.addConst idx h htip
-  ⟨⟨newCnf ++ cnf, cache, State.Inv_append hinv inv⟩, by simp [hcache]⟩
+  ⟨⟨newCnf ++ cnf, cache, State.Inv_append hinv inv⟩, by simp [newCnf, hcache]⟩
 
 /--
 Add the CNF for a `Decl.atom` to the state.
@@ -517,7 +517,7 @@ def State.addAtom (state : State aig) (idx : Nat) (h : idx < aig.decls.size)
   let newCnf := Decl.atomToCNF (.inr ⟨idx, h⟩) (.inl a)
   have hinv := toCNF.State.Inv_atomToCNF htip
   let ⟨cache, hcache⟩ := cache.addAtom idx h htip
-  ⟨⟨newCnf ++ cnf, cache, State.Inv_append hinv inv⟩, by simp [hcache]⟩
+  ⟨⟨newCnf ++ cnf, cache, State.Inv_append hinv inv⟩, by simp [newCnf, hcache]⟩
 
 /--
 Add the CNF for a `Decl.gate` to the state.
@@ -537,7 +537,7 @@ def State.addGate (state : State aig) {hlb} {hrb} (idx : Nat) (h : idx < aig.dec
       rinv
   have hinv := toCNF.State.Inv_gateToCNF htip
   let ⟨cache, hcache⟩ := cache.addGate idx h htip hl hr
-  ⟨⟨newCnf ++ cnf, cache, State.Inv_append hinv inv⟩, by simp [hcache]⟩
+  ⟨⟨newCnf ++ cnf, cache, State.Inv_append hinv inv⟩, by simp [newCnf, hcache]⟩
 
 /--
 Evaluate the CNF contained within the state.

src/Std/Sat/AIG/Relabel.lean

@@ -65,7 +65,7 @@ def relabel (r : α → β) (aig : AIG α) : AIG β :=
     cache,
     invariant := by
       intro idx lhs rhs linv rinv hbound hgate
-      simp [decls] at hgate
+      simp +zetaDelta [decls] at hgate
       have := Decl.relabel_gate hgate
       apply aig.invariant
       assumption

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

@@ -224,7 +224,7 @@ theorem ratAdd_result {n : Nat} (f : DefaultFormula n) (c : DefaultClause n) (p
             have insertRupUnits_rw : (insertRupUnits f (negate c)).1 =
               ⟨(insertRupUnits f (negate c)).1.clauses, (insertRupUnits f (negate c)).1.rupUnits,
                (insertRupUnits f (negate c)).1.ratUnits, (insertRupUnits f (negate c)).1.assignments⟩ := rfl
-            simp only [performRatCheck_fold_formula_eq performRupCheck_res h_performRupCheck_res (Literal.negate p) ratHints,
+            simp +zetaDelta only [performRatCheck_fold_formula_eq performRupCheck_res h_performRupCheck_res (Literal.negate p) ratHints,
               clauses_performRupCheck, rupUnits_performRupCheck, ratUnits_performRupCheck,
               restoreAssignments_performRupCheck fc fc_assignments_size, ← insertRupUnits_rw,
               clear_insertRup f f_readyForRatAdd.2 (negate c), fc, performRupCheck_res]

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

@@ -111,7 +111,7 @@ theorem insertUnitInvariant_insertUnit {n : Nat} (assignments0 : Array Assignmen
           ⟨units.size, units_size_lt_updatedUnits_size⟩
         have i_gt_zero : i.1 > 0 := by rw [i_eq_l]; exact l.1.2.1
         refine ⟨mostRecentUnitIdx, l.2, i_gt_zero, ?_⟩
-        simp only [insertUnit, h3, ite_false, Array.getElem_push_eq, i_eq_l, reduceCtorEq]
+        simp +zetaDelta only [insertUnit, h3, ite_false, Array.getElem_push_eq, i_eq_l, reduceCtorEq]
         constructor
         · rfl
         · constructor
@@ -131,7 +131,6 @@ theorem insertUnitInvariant_insertUnit {n : Nat} (assignments0 : Array Assignmen
                   exact k_property
                 · intro h
                   simp only [← h, not_true, mostRecentUnitIdx] at hk
-                  exact hk rfl
               rw [Array.getElem_push_lt _ _ _ k_in_bounds]
               rw [i_eq_l] at h2
               exact h2 ⟨k.1, k_in_bounds⟩
@@ -193,7 +192,7 @@ theorem insertUnitInvariant_insertUnit {n : Nat} (assignments0 : Array Assignmen
           constructor
           · rw [Array.getElem_push_lt units l j.1 j.2, h1]
           · constructor
-            · simp [i_eq_l, ← hl]
+            · simp +zetaDelta [i_eq_l, ← hl]
               rfl
             · constructor
               · simp only [i_eq_l]
@@ -228,7 +227,7 @@ theorem insertUnitInvariant_insertUnit {n : Nat} (assignments0 : Array Assignmen
           refine ⟨mostRecentUnitIdx, ⟨j.1, j_lt_updatedUnits_size⟩, i_gt_zero, ?_⟩
           simp [insertUnit, h5, ite_false, Array.getElem_push_eq, ne_eq]
           constructor
-          · simp [i_eq_l, ← hl]
+          · simp +zetaDelta [i_eq_l, ← hl]
             rfl
           · constructor
             · rw [Array.getElem_push_lt units l j.1 j.2, h1]
@@ -1330,7 +1329,7 @@ theorem rupAdd_result {n : Nat} (f : DefaultFormula n) (c : DefaultClause n) (ru
         have fc_assignments_size : (insertRupUnits f (negate c)).1.assignments.size = n := by
           rw [size_assignments_insertRupUnits f (negate c)]
           exact f_readyForRupAdd.2.1
-        simp only [clauses_performRupCheck, rupUnits_performRupCheck, ratUnits_performRupCheck,
+        simp +zetaDelta only [clauses_performRupCheck, rupUnits_performRupCheck, ratUnits_performRupCheck,
           restoreAssignments_performRupCheck fc fc_assignments_size, Prod.mk.injEq, and_true] at rupAddSuccess
         have rupAddSuccess : DefaultFormula.insert (clearRupUnits (insertRupUnits f (negate c)).fst) c = f' := by
           rw [rupAddSuccess]

src/Std/Time/Date/ValidDate.lean

@@ -48,7 +48,7 @@ def ofOrdinal (ordinal : Day.Ordinal.OfYear leap) : ValidDate leap :=
         let bounded := Bounded.LE.mk ordinal.val (And.intro h h₁) |>.sub acc
         let bounded : Bounded.LE 1 monthDays.val := bounded.cast (by omega) (by omega)
         let days₁ : Day.Ordinal := ⟨bounded.val, And.intro bounded.property.left (Int.le_trans bounded.property.right monthDays.property.right)⟩
-        ⟨⟨idx, days₁⟩, Int.le_trans bounded.property.right (by simp)⟩
+        ⟨⟨idx, days₁⟩, Int.le_trans bounded.property.right (by simp +zetaDelta)⟩
       else by
         let h₂ := Int.not_le.mp h₁