fix: propagate Simp.Config when reducing terms and checking definit…

…ional equality in `simp`

This PR ensures that the configuration in `Simp.Config` is used when reducing terms and checking definitional equality in `simp`.

closes #5455

TODO: fix broken tests

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

@@ -111,7 +111,7 @@ where
 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 thm.rfl then
@@ -336,7 +336,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
@@ -543,7 +543,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
@@ -585,7 +585,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

@@ -131,7 +131,6 @@ private def mkIndexConfig (c : Config) : ConfigWithKey :=
 /--
 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
     proj         := if c.proj then .yesWithDelta else .no
@@ -237,6 +236,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
 

tests/lean/run/2670.lean

@@ -19,5 +19,18 @@ theorem enumFrom_eq_enumFromTR' : @enumFrom = @enumFromTR' := by
     | a::as, n => by
       rw [← show _ + as.length = n + (a::as).length from Nat.succ_add .., List.foldr, go as]
       simp [enumFrom, f]
-  rw [Array.foldr_eq_foldr_toList]
-  simp [go] -- Should close the goal
+  rw [←Array.foldr_toList]
+  simp [f] at go -- We must unfold `f` at `go`, or use `+zetaDelta`. See next theorem
+  simp [go]
+
+open List in
+theorem enumFrom_eq_enumFromTR'' : @enumFrom = @enumFromTR' := by
+  funext α n l; simp only [enumFromTR']
+  let f := fun (a : α) (n, acc) => (n-1, (n-1, a) :: acc)
+  let rec go : ∀ l n, l.foldr f (n + l.length, []) = (n, enumFrom n l)
+    | [], n => rfl
+    | a::as, n => by
+      rw [← show _ + as.length = n + (a::as).length from Nat.succ_add .., List.foldr, go as]
+      simp [enumFrom, f]
+  rw [←Array.foldr_toList]
+  simp +zetaDelta [go]

tests/lean/run/5455.lean

@@ -0,0 +1,23 @@
+variable {α : Type}
+
+theorem test1 {n : Nat} {f : Fin n → α} : False := by
+  let c (i : Fin n) : Nat := i
+  let d : Fin n → Nat × Nat := fun i => (c i, c i + 1)
+  have : ∀ i, (d i).2 ≠ c i * 2 := by
+    fail_if_success simp only -- should not unfold `d` or `i`
+    guard_target =ₛ ∀ (i : Fin n), (d i).snd ≠ c i * 2
+    simp +zetaDelta only -- `d` and `i` are now unfolded
+    guard_target =ₛ ∀ (i : Fin n), i.val + 1 ≠ i.val * 2
+    sorry
+  sorry
+
+opaque f : Nat → Nat
+axiom f_ax (x : Nat): f (f x) = x
+
+theorem test2 (a : Nat) : False := by
+  let d : Nat → Nat × Nat := fun i => (f a, i)
+  have : f (d 1).1 = a := by
+    fail_if_success simp only [f_ax] -- f_ax should be applicable
+    simp +zetaDelta only [f_ax] -- f_ax is applicable if zetaDelta := true
+    done
+  sorry

tests/lean/run/heapSort.lean

@@ -166,7 +166,8 @@ def Array.toBinaryHeap (lt : α → α → Bool) (a : Array α) : BinaryHeap α
     | none => out
     | some x =>
       have : a.popMax.size < a.size := by
-        simp; exact Nat.sub_lt (BinaryHeap.size_pos_of_max e) Nat.zero_lt_one
+        simp +zetaDelta
+        exact Nat.sub_lt (BinaryHeap.size_pos_of_max e) Nat.zero_lt_one
       loop a.popMax (out.push x)
     termination_by a.size
     decreasing_by assumption