test: for issue #2843

closes #2843

RELEASES.md

@@ -18,6 +18,54 @@ v4.7.0 (development in progress)
 
 * `pp.proofs.withType` is now set to false by default to reduce noise in the info view.
 
+* New `simp` (and `dsimp`) configuration option: `zetaDelta`. It is `false` by default.
+  The `zeta` option is still `true` by default, but their meaning has changed.
+  - When `zeta := true`, `simp` and `dsimp` reduce terms of the form
+    `let x := val; e[x]` into `e[val]`.
+  - When `zetaDelta := true`, `simp` and `dsimp` will expand let-variables in
+    the context. For example, suppose the context contains `x := val`. Then,
+    any occurrence of `x` is replaced with `val`.
+
+  See issue #2682 for additional details. Here are some examples:
+  ```
+  example (h : z = 9) : let x := 5; let y := 4; x + y = z := by
+    intro x
+    simp
+    /-
+    New goal:
+    h : z = 9; x := 5 |- x + 4 = z
+    -/
+    rw [h]
+
+  example (h : z = 9) : let x := 5; let y := 4; x + y = z := by
+    intro x
+    -- Using both `zeta` and `zetaDelta`.
+    simp (config := { zetaDelta := true })
+    /-
+    New goal:
+    h : z = 9; x := 5 |- 9 = z
+    -/
+    rw [h]
+
+  example (h : z = 9) : let x := 5; let y := 4; x + y = z := by
+    intro x
+    simp [x] -- asks `simp` to unfold `x`
+    /-
+    New goal:
+    h : z = 9; x := 5 |- 9 = z
+    -/
+    rw [h]
+
+  example (h : z = 9) : let x := 5; let y := 4; x + y = z := by
+    intro x
+    simp (config := { zetaDelta := true, zeta := false })
+    /-
+    New goal:
+    h : z = 9; x := 5 |- let y := 4; 5 + y = z
+    -/
+    rw [h]
+  ```
+
 v4.6.0
 ---------
 

src/Init/MetaTypes.lean

@@ -43,6 +43,7 @@ inductive EtaStructMode where
 namespace DSimp
 
 structure Config where
+  /-- `let x := v; e[x]` reduces to `e[v]`. -/
   zeta              : Bool := true
   beta              : Bool := true
   eta               : Bool := true
@@ -57,6 +58,8 @@ structure Config where
   /-- If `unfoldPartialApp := true`, then calls to `simp`, `dsimp`, or `simp_all`
   will unfold even partial applications of `f` when we request `f` to be unfolded. -/
   unfoldPartialApp  : Bool := false
+  /-- Given a local context containing entry `x : t := e`, free variable `x` reduces to `e`. -/
+  zetaDelta         : Bool := false
   deriving Inhabited, BEq
 
 end DSimp
@@ -71,6 +74,7 @@ structure Config where
   contextual        : Bool := false
   memoize           : Bool := true
   singlePass        : Bool := false
+  /-- `let x := v; e[x]` reduces to `e[v]`. -/
   zeta              : Bool := true
   beta              : Bool := true
   eta               : Bool := true
@@ -95,6 +99,8 @@ structure Config where
   /-- If `unfoldPartialApp := true`, then calls to `simp`, `dsimp`, or `simp_all`
   will unfold even partial applications of `f` when we request `f` to be unfolded. -/
   unfoldPartialApp  : Bool := false
+  /-- Given a local context containing entry `x : t := e`, free variable `x` reduces to `e`. -/
+  zetaDelta         : Bool := false
   deriving Inhabited, BEq
 
 -- Configuration object for `simp_all`
@@ -111,6 +117,7 @@ def neutralConfig : Simp.Config := {
   arith             := false
   autoUnfold        := false
   ground            := false
+  zetaDelta         := false
 }
 
 end Simp

src/Init/WFTactics.lean

@@ -11,7 +11,7 @@ import Init.WF
 /-- Unfold definitions commonly used in well founded relation definitions.
 This is primarily intended for internal use in `decreasing_tactic`. -/
 macro "simp_wf" : tactic =>
-  `(tactic| try simp (config := { unfoldPartialApp := true }) [invImage, InvImage, Prod.lex, sizeOfWFRel, measure, Nat.lt_wfRel, WellFoundedRelation.rel])
+  `(tactic| try simp (config := { unfoldPartialApp := true, zetaDelta := true }) [invImage, InvImage, Prod.lex, sizeOfWFRel, measure, Nat.lt_wfRel, WellFoundedRelation.rel])
 
 /-- Extensible helper tactic for `decreasing_tactic`. This handles the "base case"
 reasoning after applying lexicographic order lemmas.

src/Lean/Elab/MutualDef.lean

@@ -531,8 +531,8 @@ private partial def mkClosureForAux (toProcess : Array FVarId) : StateRefT Closu
       let toProcess ← pushLocalDecl toProcess fvarId userName type bi k
       mkClosureForAux toProcess
     | .ldecl _ _ userName type val _ k =>
-      let zetaFVarIds ← getZetaFVarIds
-      if !zetaFVarIds.contains fvarId then
+      let zetaDeltaFVarIds ← getZetaDeltaFVarIds
+      if !zetaDeltaFVarIds.contains fvarId then
         /- Non-dependent let-decl. See comment at src/Lean/Meta/Closure.lean -/
         let toProcess ← pushLocalDecl toProcess fvarId userName type .default k
         mkClosureForAux toProcess
@@ -696,8 +696,8 @@ def main (sectionVars : Array Expr) (mainHeaders : Array DefViewElabHeader) (mai
   let letRecsToLift := letRecsToLift.toArray
   let mainFVarIds := mainFVars.map Expr.fvarId!
   let recFVarIds  := (letRecsToLift.map fun toLift => toLift.fvarId) ++ mainFVarIds
-  resetZetaFVarIds
-  withTrackingZeta do
+  resetZetaDeltaFVarIds
+  withTrackingZetaDelta do
     -- By checking `toLift.type` and `toLift.val` we populate `zetaFVarIds`. See comments at `src/Lean/Meta/Closure.lean`.
     let letRecsToLift ← letRecsToLift.mapM fun toLift => withLCtx toLift.lctx toLift.localInstances do
       Meta.check toLift.type

src/Lean/Elab/Structure.lean

@@ -739,7 +739,7 @@ private def addDefaults (lctx : LocalContext) (defaultAuxDecls : Array (Name ×
         throwError "invalid default value for field, it contains metavariables{indentExpr value}"
       /- The identity function is used as "marker". -/
       let value ← mkId value
-      discard <| mkAuxDefinition declName type value (zeta := true)
+      discard <| mkAuxDefinition declName type value (zetaDelta := true)
       setReducibleAttribute declName
 
 /--

src/Lean/Elab/Tactic/ElabTerm.lean

@@ -356,7 +356,7 @@ def elabAsFVar (stx : Syntax) (userName? : Option Name := none) : TacticM FVarId
 
 /--
    Make sure `expectedType` does not contain free and metavariables.
-   It applies zeta-reduction to eliminate let-free-vars.
+   It applies zeta and zetaDelta-reduction to eliminate let-free-vars.
 -/
 private def preprocessPropToDecide (expectedType : Expr) : TermElabM Expr := do
   let mut expectedType ← instantiateMVars expectedType

src/Lean/Meta/AbstractNestedProofs.lean

@@ -35,10 +35,10 @@ private def mkAuxLemma (e : Expr) : M Expr := do
   let s ← get
   let lemmaName ← mkAuxName (ctx.baseName ++ `proof) s.nextIdx
   modify fun s => { s with nextIdx := s.nextIdx + 1 }
-  /- We turn on zeta-expansion to make sure we don't need to perform an expensive `check` step to
-     identify which let-decls can be abstracted. If we design a more efficient test, we can avoid the eager zeta expansion step.
+  /- We turn on zetaDelta-expansion to make sure we don't need to perform an expensive `check` step to
+     identify which let-decls can be abstracted. If we design a more efficient test, we can avoid the eager zetaDelta expansion step.
      It a benchmark created by @selsam, The extra `check` step was a bottleneck. -/
-  mkAuxTheoremFor lemmaName e (zeta := true)
+  mkAuxTheoremFor lemmaName e (zetaDelta := true)
 
 partial def visit (e : Expr) : M Expr := do
   if e.isAtomic then

src/Lean/Meta/Basic.lean

@@ -96,17 +96,17 @@ structure Config where
    -/
   transparency       : TransparencyMode := TransparencyMode.default
   /--
-  When `trackZeta = true`, we track all free variables that have been zeta-expanded.
+  When `trackZetaDelta = true`, we track all free variables that have been zetaDelta-expanded.
   That is, suppose the local context contains
-  the declaration `x : t := v`, and we reduce `x` to `v`, then we insert `x` into `State.zetaFVarIds`.
-  We use `trackZeta` to discover which let-declarations `let x := v; e` can be represented as `(fun x => e) v`.
+  the declaration `x : t := v`, and we reduce `x` to `v`, then we insert `x` into `State.zetaDeltaFVarIds`.
+  We use `trackZetaDelta` to discover which let-declarations `let x := v; e` can be represented as `(fun x => e) v`.
   When we find these declarations we set their `nonDep` flag with `true`.
   To find these let-declarations in a given term `s`, we
-  1- Reset `State.zetaFVarIds`
-  2- Set `trackZeta := true`
+  1- Reset `State.zetaDeltaFVarIds`
+  2- Set `trackZetaDelta := true`
   3- Type-check `s`.
   -/
-  trackZeta          : Bool := false
+  trackZetaDelta     : Bool := false
   /-- Eta for structures configuration mode. -/
   etaStruct          : EtaStructMode := .all
 
@@ -261,12 +261,12 @@ structure PostponedEntry where
   `MetaM` monad state.
 -/
 structure State where
-  mctx           : MetavarContext := {}
-  cache          : Cache := {}
-  /-- When `trackZeta == true`, then any let-decl free variable that is zeta expansion performed by `MetaM` is stored in `zetaFVarIds`. -/
-  zetaFVarIds    : FVarIdSet := {}
+  mctx             : MetavarContext := {}
+  cache            : Cache := {}
+  /-- When `trackZetaDelta == true`, then any let-decl free variable that is zetaDelta expansion performed by `MetaM` is stored in `zetaDeltaFVarIds`. -/
+  zetaDeltaFVarIds : FVarIdSet := {}
   /-- Array of postponed universe level constraints -/
-  postponed      : PersistentArray PostponedEntry := {}
+  postponed        : PersistentArray PostponedEntry := {}
   deriving Inhabited
 
 /--
@@ -330,7 +330,7 @@ protected def saveState : MetaM SavedState :=
 /-- Restore backtrackable parts of the state. -/
 def SavedState.restore (b : SavedState) : MetaM Unit := do
   Core.restore b.core
-  modify fun s => { s with mctx := b.meta.mctx, zetaFVarIds := b.meta.zetaFVarIds, postponed := b.meta.postponed }
+  modify fun s => { s with mctx := b.meta.mctx, zetaDeltaFVarIds := b.meta.zetaDeltaFVarIds, postponed := b.meta.postponed }
 
 instance : MonadBacktrack SavedState MetaM where
   saveState      := Meta.saveState
@@ -374,7 +374,7 @@ section Methods
 variable [MonadControlT MetaM n] [Monad n]
 
 @[inline] def modifyCache (f : Cache → Cache) : MetaM Unit :=
-  modify fun { mctx, cache, zetaFVarIds, postponed } => { mctx, cache := f cache, zetaFVarIds, postponed }
+  modify fun { mctx, cache, zetaDeltaFVarIds, postponed } => { mctx, cache := f cache, zetaDeltaFVarIds, postponed }
 
 @[inline] def modifyInferTypeCache (f : InferTypeCache → InferTypeCache) : MetaM Unit :=
   modifyCache fun ⟨ic, c1, c2, c3, c4, c5, c6⟩ => ⟨f ic, c1, c2, c3, c4, c5, c6⟩
@@ -394,11 +394,11 @@ def getLocalInstances : MetaM LocalInstances :=
 def getConfig : MetaM Config :=
   return (← read).config
 
-def resetZetaFVarIds : MetaM Unit :=
-  modify fun s => { s with zetaFVarIds := {} }
+def resetZetaDeltaFVarIds : MetaM Unit :=
+  modify fun s => { s with zetaDeltaFVarIds := {} }
 
-def getZetaFVarIds : MetaM FVarIdSet :=
-  return (← get).zetaFVarIds
+def getZetaDeltaFVarIds : MetaM FVarIdSet :=
+  return (← get).zetaDeltaFVarIds
 
 /-- Return the array of postponed universe level constraints. -/
 def getPostponed : MetaM (PersistentArray PostponedEntry) :=
@@ -790,10 +790,10 @@ def elimMVarDeps (xs : Array Expr) (e : Expr) (preserveOrder : Bool := false) :
   mapMetaM <| withReader (fun ctx => { ctx with config := f ctx.config })
 
 /--
-Executes `x` tracking zeta reductions `Config.trackZeta := true`
+Executes `x` tracking zetaDelta reductions `Config.trackZetaDelta := true`
 -/
-@[inline] def withTrackingZeta (x : n α) : n α :=
-  withConfig (fun cfg => { cfg with trackZeta := true }) x
+@[inline] def withTrackingZetaDelta (x : n α) : n α :=
+  withConfig (fun cfg => { cfg with trackZetaDelta := true }) x
 
 @[inline] def withoutProofIrrelevance (x : n α) : n α :=
   withConfig (fun cfg => { cfg with proofIrrelevance := false }) x

src/Lean/Meta/Closure.lean

@@ -56,14 +56,14 @@ def aux := fun (y : Nat) => h (g y)
 Note that in this particular case, it is safe to lambda abstract the let-varible `y`.
 This module uses the following approach to decide whether it is safe or not to lambda
 abstract a let-variable.
-1) We enable zeta-expansion tracking in `MetaM`. That is, whenever we perform type checking
-   if a let-variable needs to zeta expanded, we store it in the set `zetaFVarIds`.
-   We say a let-variable is zeta expanded when we replace it with its value.
+1) We enable zetaDelta-expansion tracking in `MetaM`. That is, whenever we perform type checking
+   if a let-variable needs to zetaDelta expanded, we store it in the set `zetaDeltaFVarIds`.
+   We say a let-variable is zetaDelta expanded when we replace it with its value.
 2) We use the `MetaM` type checker `check` to type check the expression we want to close,
    and the type of the binders.
-3) If a let-variable is not in `zetaFVarIds`, we lambda abstract it.
+3) If a let-variable is not in `zetaDeltaFVarIds`, we lambda abstract it.
 
-Remark: We still use let-expressions for let-variables in `zetaFVarIds`, but we move the
+Remark: We still use let-expressions for let-variables in `zetaDeltaFVarIds`, but we move the
 `let` inside the lambdas. The idea is to make sure the auxiliary definition does not have
 an interleaving of `lambda` and `let` expressions. Thus, if the let-variable occurs in
 the type of one of the lambdas, we simply zeta-expand it there.
@@ -89,7 +89,7 @@ let n : Nat := 20;
 (let y : {v // v=n} := {val := 20, property := ex._proof_1}; y.val+n+f x, z+10)
 ```
 
-BTW, this module also provides the `zeta : Bool` flag. When set to true, it
+BTW, this module also provides the `zetaDelta : Bool` flag. When set to true, it
 expands all let-variables occurring in the target expression.
 -/
 
@@ -102,7 +102,7 @@ structure ToProcessElement where
   deriving Inhabited
 
 structure Context where
-  zeta : Bool
+  zetaDelta : Bool
 
 structure State where
   visitedLevel          : LevelMap Level := {}
@@ -165,9 +165,9 @@ def collectLevel (u : Level) : ClosureM Level := do
 def preprocess (e : Expr) : ClosureM Expr := do
   let e ← instantiateMVars e
   let ctx ← read
-  -- If we are not zeta-expanding let-decls, then we use `check` to find
+  -- If we are not zetaDelta-expanding let-decls, then we use `check` to find
   -- which let-decls are dependent. We say a let-decl is dependent if its lambda abstraction is type incorrect.
-  if !ctx.zeta then
+  if !ctx.zetaDelta then
     check e
   pure e
 
@@ -207,7 +207,7 @@ partial def collectExprAux (e : Expr) : ClosureM Expr := do
     }
     return mkFVar newFVarId
   | Expr.fvar fvarId =>
-    match (← read).zeta, (← fvarId.getValue?) with
+    match (← read).zetaDelta, (← fvarId.getValue?) with
     | true, some value => collect (← preprocess value)
     | _,    _          =>
       let newFVarId ← mkFreshFVarId
@@ -259,14 +259,14 @@ partial def process : ClosureM Unit := do
       pushFVarArg (mkFVar fvarId)
       process
     | .ldecl _ _ userName type val _ _ =>
-      let zetaFVarIds ← getZetaFVarIds
-      if !zetaFVarIds.contains fvarId then
+      let zetaDeltaFVarIds ← getZetaDeltaFVarIds
+      if !zetaDeltaFVarIds.contains fvarId then
         /- Non-dependent let-decl
 
-            Recall that if `fvarId` is in `zetaFVarIds`, then we zeta-expanded it
+            Recall that if `fvarId` is in `zetaDeltaFVarIds`, then we zetaDelta-expanded it
             during type checking (see `check` at `collectExpr`).
 
-            Our type checker may zeta-expand declarations that are not needed, but this
+            Our type checker may zetaDelta-expand declarations that are not needed, but this
             check is conservative, and seems to work well in practice. -/
         pushLocalDecl newFVarId userName type
         pushFVarArg (mkFVar fvarId)
@@ -315,15 +315,15 @@ structure MkValueTypeClosureResult where
   exprArgs    : Array Expr
 
 def mkValueTypeClosureAux (type : Expr) (value : Expr) : ClosureM (Expr × Expr) := do
-  resetZetaFVarIds
-  withTrackingZeta do
+  resetZetaDeltaFVarIds
+  withTrackingZetaDelta do
     let type  ← collectExpr type
     let value ← collectExpr value
     process
     pure (type, value)
 
-def mkValueTypeClosure (type : Expr) (value : Expr) (zeta : Bool) : MetaM MkValueTypeClosureResult := do
-  let ((type, value), s) ← ((mkValueTypeClosureAux type value).run { zeta := zeta }).run {}
+def mkValueTypeClosure (type : Expr) (value : Expr) (zetaDelta : Bool) : MetaM MkValueTypeClosureResult := do
+  let ((type, value), s) ← ((mkValueTypeClosureAux type value).run { zetaDelta }).run {}
   let newLocalDecls := s.newLocalDecls.reverse ++ s.newLocalDeclsForMVars
   let newLetDecls   := s.newLetDecls.reverse
   let type  := mkForall newLocalDecls (mkForall newLetDecls type)
@@ -344,8 +344,8 @@ end Closure
   A "closure" is computed, and a term of the form `name.{u_1 ... u_n} t_1 ... t_m` is
   returned where `u_i`s are universe parameters and metavariables `type` and `value` depend on,
   and `t_j`s are free and meta variables `type` and `value` depend on. -/
-def mkAuxDefinition (name : Name) (type : Expr) (value : Expr) (zeta : Bool := false) (compile : Bool := true) : MetaM Expr := do
-  let result ← Closure.mkValueTypeClosure type value zeta
+def mkAuxDefinition (name : Name) (type : Expr) (value : Expr) (zetaDelta : Bool := false) (compile : Bool := true) : MetaM Expr := do
+  let result ← Closure.mkValueTypeClosure type value zetaDelta
   let env ← getEnv
   let decl := Declaration.defnDecl {
     name        := name
@@ -361,16 +361,16 @@ def mkAuxDefinition (name : Name) (type : Expr) (value : Expr) (zeta : Bool := f
   return mkAppN (mkConst name result.levelArgs.toList) result.exprArgs
 
 /-- Similar to `mkAuxDefinition`, but infers the type of `value`. -/
-def mkAuxDefinitionFor (name : Name) (value : Expr) (zeta : Bool := false) : MetaM Expr := do
+def mkAuxDefinitionFor (name : Name) (value : Expr) (zetaDelta : Bool := false) : MetaM Expr := do
   let type ← inferType value
   let type := type.headBeta
-  mkAuxDefinition name type value (zeta := zeta)
+  mkAuxDefinition name type value (zetaDelta := zetaDelta)
 
 /--
   Create an auxiliary theorem with the given name, type and value. It is similar to `mkAuxDefinition`.
 -/
-def mkAuxTheorem (name : Name) (type : Expr) (value : Expr) (zeta : Bool := false) : MetaM Expr := do
-  let result ← Closure.mkValueTypeClosure type value zeta
+def mkAuxTheorem (name : Name) (type : Expr) (value : Expr) (zetaDelta : Bool := false) : MetaM Expr := do
+  let result ← Closure.mkValueTypeClosure type value zetaDelta
   let env ← getEnv
   let decl :=
     if env.hasUnsafe result.type || env.hasUnsafe result.value then
@@ -396,9 +396,9 @@ def mkAuxTheorem (name : Name) (type : Expr) (value : Expr) (zeta : Bool := fals
 /--
   Similar to `mkAuxTheorem`, but infers the type of `value`.
 -/
-def mkAuxTheoremFor (name : Name) (value : Expr) (zeta : Bool := false) : MetaM Expr := do
+def mkAuxTheoremFor (name : Name) (value : Expr) (zetaDelta : Bool := false) : MetaM Expr := do
   let type ← inferType value
   let type := type.headBeta
-  mkAuxTheorem name type value zeta
+  mkAuxTheorem name type value zetaDelta
 
 end Lean.Meta

src/Lean/Meta/Match/Match.lean

@@ -682,7 +682,7 @@ builtin_initialize matcherExt : EnvExtension (PHashMap (Expr × Bool) Name) ←
 def mkMatcherAuxDefinition (name : Name) (type : Expr) (value : Expr) : MetaM (Expr × Option (MatcherInfo → MetaM Unit)) := do
   trace[Meta.Match.debug] "{name} : {type} := {value}"
   let compile := bootstrap.genMatcherCode.get (← getOptions)
-  let result ← Closure.mkValueTypeClosure type value (zeta := false)
+  let result ← Closure.mkValueTypeClosure type value (zetaDelta := false)
   let env ← getEnv
   let mkMatcherConst name :=
     mkAppN (mkConst name result.levelArgs.toList) result.exprArgs

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

@@ -76,7 +76,7 @@ private def reduceProjFn? (e : Expr) : SimpM (Option Expr) := do
         reduceProjCont? (← unfoldDefinition? e)
 
 private def reduceFVar (cfg : Config) (thms : SimpTheoremsArray) (e : Expr) : MetaM Expr := do
-  if cfg.zeta || thms.isLetDeclToUnfold e.fvarId! then
+  if cfg.zetaDelta || thms.isLetDeclToUnfold e.fvarId! then
     match (← getFVarLocalDecl e).value? with
     | some v => return v
     | none   => return e
@@ -166,6 +166,8 @@ private def reduceStep (e : Expr) : SimpM Expr := do
   if cfg.zeta then
     if let some (args, _, _, v, b) := e.letFunAppArgs? then
       return mkAppN (b.instantiate1 v) args
+    if e.isLet then
+      return e.letBody!.instantiate1 e.letValue!
   match (← unfold? e) with
   | some e' =>
     trace[Meta.Tactic.simp.rewrite] "unfold {mkConst e.getAppFn.constName!}, {e} ==> {e'}"

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

@@ -165,7 +165,7 @@ structure SimpTheorems where
   lemmaNames   : PHashSet Origin := {}
   /--
   Constants (and let-declaration `FVarId`) to unfold.
-  When `zeta := false`, the simplifier will expand a let-declaration if it is in this set.
+  When `zetaDelta := false`, the simplifier will expand a let-declaration if it is in this set.
   -/
   toUnfold     : PHashSet Name := {}
   erased       : PHashSet Origin := {}
@@ -173,7 +173,7 @@ structure SimpTheorems where
   deriving Inhabited
 
 /-- Configuration for the discrimination tree. -/
-def simpDtConfig : WhnfCoreConfig := { iota := false, proj := .no }
+def simpDtConfig : WhnfCoreConfig := { iota := false, proj := .no, zetaDelta := false }
 
 def addSimpTheoremEntry (d : SimpTheorems) (e : SimpTheorem) : SimpTheorems :=
   if e.post then

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

@@ -14,7 +14,7 @@ namespace Simp
 
 /-- The result of simplifying some expression `e`. -/
 structure Result where
-  /-- The simplified version of `e` -/ 
+  /-- The simplified version of `e` -/
   expr           : Expr
   /-- A proof that `$e = $expr`, where the simplified expression is on the RHS.
   If `none`, the proof is assumed to be `refl`. -/
@@ -481,15 +481,13 @@ def tryAutoCongrTheorem? (e : Expr) : SimpM (Option Result) := do
 
 /--
 Return a WHNF configuration for retrieving `[simp]` from the discrimination tree.
-If user has disabled `zeta` and/or `beta` reduction in the simplifier, we must also
-disable them when retrieving lemmas from discrimination tree. See issues: #2669 and #2281
+If user has disabled `zeta` and/or `beta` reduction in the simplifier, or enabled `zetaDelta`,
+we must also disable/enable them when retrieving lemmas from discrimination tree. See issues: #2669 and #2281
 -/
 def getDtConfig (cfg : Config) : WhnfCoreConfig :=
-  match cfg.beta, cfg.zeta with
-  | true, true => simpDtConfig
-  | true, false => { simpDtConfig with zeta := false }
-  | false, true => { simpDtConfig with beta := false }
-  | false, false => { simpDtConfig with beta := false, zeta := false }
+  match cfg.beta, cfg.zeta, cfg.zetaDelta with
+  | true, true, false => simpDtConfig
+  | _,    _,    _     => { simpDtConfig with zeta := cfg.zeta, beta := cfg.beta, zetaDelta := cfg.zetaDelta }
 
 def Result.addExtraArgs (r : Result) (extraArgs : Array Expr) : MetaM Result := do
   match r.proof? with

src/Lean/Meta/Transform.lean

@@ -134,6 +134,7 @@ partial def transform {m} [Monad m] [MonadLiftT MetaM m] [MonadControlT MetaM m]
         | _                  => visitPost e
   visit input |>.run
 
+-- TODO: add options to distinguish zeta and zetaDelta reduction
 def zetaReduce (e : Expr) : MetaM Expr := do
   let pre (e : Expr) : MetaM TransformStep := do
     match e with

src/Lean/Meta/WHNF.lean

@@ -335,11 +335,7 @@ structure WhnfCoreConfig where
   /-- Control projection reduction at `whnfCore`. -/
   proj : ProjReductionKind := .yesWithDelta
   /--
-  Zeta reduction.
-  It includes two kinds of reduction:
-  - `let x := v; e[x]` reduces to `e[v]`.
-  - Given a local context containing entry `x : t := e`, free variable `x` reduces to `e`.
-
+  Zeta reduction: `let x := v; e[x]` reduces to `e[v]`.
   We say a let-declaration `let x := v; e` is non dependent if it is equivalent to `(fun x => e) v`.
   Recall that
   ```
@@ -352,6 +348,10 @@ structure WhnfCoreConfig where
   is not.
   -/
   zeta : Bool := true
+  /--
+  Zeta-delta reduction: given a local context containing entry `x : t := e`, free variable `x` reduces to `e`.
+  -/
+  zetaDelta : Bool := true
 
 /-- Auxiliary combinator for handling easy WHNF cases. It takes a function for handling the "hard" cases as an argument -/
 @[specialize] partial def whnfEasyCases (e : Expr) (k : Expr → MetaM Expr) (config : WhnfCoreConfig := {}) : MetaM Expr := do
@@ -371,9 +371,9 @@ structure WhnfCoreConfig where
     match decl with
     | .cdecl .. => return e
     | .ldecl (value := v) .. =>
-      unless config.zeta do return e
-      if (← getConfig).trackZeta then
-        modify fun s => { s with zetaFVarIds := s.zetaFVarIds.insert fvarId }
+      unless config.zetaDelta do return e
+      if (← getConfig).trackZetaDelta then
+        modify fun s => { s with zetaDeltaFVarIds := s.zetaDeltaFVarIds.insert fvarId }
       whnfEasyCases v k config
   | .mvar mvarId   =>
     match (← getExprMVarAssignment? mvarId) with

tests/lean/heapSort.lean

@@ -108,7 +108,7 @@ def popMaxAux {lt} (self : BinaryHeap α lt) : {a' : BinaryHeap α lt // a'.size
     if hn0 : 0 < n then
       let a := self.1.swap ⟨0, h0⟩ ⟨n, hn⟩ |>.pop
       ⟨⟨heapifyDown lt a ⟨0, sorry⟩⟩,
-        by simp [size]⟩
+        by simp [size, a]⟩
     else
       ⟨⟨self.1.pop⟩, by simp [size]⟩
 
@@ -133,7 +133,7 @@ def insertExtractMax {lt} (self : BinaryHeap α lt) (x : α) : α × BinaryHeap
   | some m =>
     if lt x m then
       let a := self.1.set ⟨0, size_pos_of_max e⟩ x
-      (m, ⟨heapifyDown lt a ⟨0, by simp; exact size_pos_of_max e⟩⟩)
+      (m, ⟨heapifyDown lt a ⟨0, by simp [a]; exact size_pos_of_max e⟩⟩)
     else (x, self)
 
 /-- `O(log n)`. Equivalent to `(self.max, self.popMax.insert x)`. -/
@@ -142,7 +142,7 @@ def replaceMax {lt} (self : BinaryHeap α lt) (x : α) : Option α × BinaryHeap
   | none => (none, ⟨self.1.push x⟩)
   | some m =>
     let a := self.1.set ⟨0, size_pos_of_max e⟩ x
-    (some m, ⟨heapifyDown lt a ⟨0, by simp; exact size_pos_of_max e⟩⟩)
+    (some m, ⟨heapifyDown lt a ⟨0, by simp [a]; exact size_pos_of_max e⟩⟩)
 
 /-- `O(log n)`. Replace the value at index `i` by `x`. Assumes that `x ≤ self.get i`. -/
 def decreaseKey {lt} (self : BinaryHeap α lt) (i : Fin self.size) (x : α) : BinaryHeap α lt where

tests/lean/run/2669.lean

@@ -7,7 +7,7 @@ example (n : Nat) : False := by
   let g := f n
   have : g + n = n := by
     fail_if_success simp (config := { zeta := false }) [Nat.zero_add] -- Should not succeed
-    simp
+    simp [g]
   sorry
 
 example (h : a = b) : (fun x => a + x) 0 = b := by

tests/lean/run/2843.lean

@@ -0,0 +1,18 @@
+axiom abs : Int → Int
+
+axiom abs_eq_self {a : Int }: abs a = a ↔ 0 ≤ a
+
+example (x : Int) : False := by
+  let y := x/2
+  have h : 0 ≤ y := sorry
+  have : abs y = y := by
+    -- generalize y = z at *
+    simp (config := {zeta := false}) only [abs_eq_self.mpr h]
+  sorry
+
+example (x : Int) : False := by
+  let y := x/2
+  have h : 0 ≤ y := sorry
+  have : abs y = y := by
+    simp only [abs_eq_self.mpr h]
+  sorry

tests/lean/run/796.lean

@@ -52,7 +52,7 @@ def pred_with_proof (n : ℕ) (h : n ≠ zero) : Σ' m, n = succ m :=
   by
   revert h
   let P (k : ℕ) := k ≠ zero → Σ' m, k = succ m
-  exact (nat_induction (by simp ; exact False.elim) (λ k _ _ => ⟨k, rfl⟩) n : P n)
+  exact (nat_induction (by simp [P]; exact False.elim) (λ k _ _ => ⟨k, rfl⟩) n : P n)
 
 def pred (n : ℕ) (h : n ≠ zero) : ℕ := (pred_with_proof n h).fst
 end

tests/lean/run/inductionLetIssue.lean

@@ -12,7 +12,7 @@ def f (x? : Option Nat) (hp : P x?) : { r? : Option Nat // P r? } :=
     let x := x?.get h₁
     have : x > 0 := by
       cases h₂ : x with
-      | zero => have := aux x? hp h₁; simp at h₂; simp [h₂] at this
+      | zero => have := aux x? hp h₁; simp [x] at h₂; simp [h₂] at this; done
       | succ x' => simp_arith
     ⟨some x, .somePos this⟩
   else

tests/lean/run/meta7.lean

@@ -28,9 +28,9 @@ def tst1 : MetaM Unit := do
 print "----- tst1 -----";
 let c ← getConstInfo `ex;
 lambdaTelescope c.value?.get! fun xs body =>
-  withTrackingZeta do
+  withTrackingZetaDelta do
     check body;
-    let ys ← getZetaFVarIds;
+    let ys ← getZetaDeltaFVarIds;
     let ys := ys.toList.map mkFVar;
     print ys;
     checkM $ pure $ ys.length == 2;

tests/lean/run/zetaDSimpIssue.lean

@@ -0,0 +1,8 @@
+def f (x : Nat) :=
+  let n := x + 1
+  n + n
+
+example : f x = 2*x + 2 := by
+  dsimp [f]
+  guard_target =ₛ x + 1 + (x + 1) = 2*x + 2
+  simp_arith

tests/lean/run/zetaDelta.lean

@@ -0,0 +1,23 @@
+example (h : z = 9) : let x := 5; let y := 4; x + y = z := by
+  intro x
+  simp
+  guard_target =ₛ x + 4 = z
+  rw [h]
+
+example (h : z = 9) : let x := 5; let y := 4; x + y = z := by
+  intro x
+  simp (config := { zetaDelta := true })
+  guard_target =ₛ 9 = z
+  rw [h]
+
+example (h : z = 9) : let x := 5; let y := 4; x + y = z := by
+  intro x
+  simp [x]
+  guard_target =ₛ 9 = z
+  rw [h]
+
+example (h : z = 9) : let x := 5; let y := 4; x + y = z := by
+  intro x
+  simp (config := { zetaDelta := true, zeta := false })
+  guard_target =ₛlet y := 4; 5 + y = z
+  rw [h]

tests/lean/simpZetaFalse.lean.expected.out

@@ -15,7 +15,7 @@ fun x h =>
         (let_congr (Eq.refl (x * x)) fun y =>
           ite_congr (Eq.trans (congrArg (fun x_1 => x_1 = x) h) (eq_self x)) (fun a => Eq.refl 1) fun a =>
             Eq.refl (y + 1))))
-    (of_eq_true (eq_self 1))
+    (of_eq_true (Eq.trans (congrArg (fun x => x = 1) (ite_cond_eq_true 1 (x * x + 1) (Eq.refl True))) (eq_self 1)))
 x z : Nat
 h : f (f x) = x
 h' : z = x

tests/lean/simp_trace.lean.expected.out

@@ -16,11 +16,10 @@ Try this: simp only [head]
 Try this: simp only [foo]
 [Meta.Tactic.simp.rewrite] unfold foo, foo ==> 10
 [Meta.Tactic.simp.rewrite] @eq_self:1000, 10 + x = 10 + x ==> True
-Try this: simp only [g, Id.pure_eq]
+Try this: simp only [g, pure]
 [Meta.Tactic.simp.rewrite] unfold g, g x ==> Id.run
       (let x := x;
       pure x)
-[Meta.Tactic.simp.rewrite] @Id.pure_eq:1000, pure x ==> x
 Try this: simp (config := { unfoldPartialApp := true }) only [f1, modify, modifyGet, MonadStateOf.modifyGet,
   StateT.modifyGet, pure, f2, bind, StateT.bind, get, getThe, MonadStateOf.get, StateT.get, set, StateT.set]
 [Meta.Tactic.simp.rewrite] unfold f1, f1 ==> modify fun x => g x