fix: fixes #2669 #2281

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

@@ -142,11 +142,24 @@ def tryTheorem? (e : Expr) (thm : SimpTheorem) (discharge? : Expr → SimpM (Opt
         tryTheoremCore lhs xs bis val type e thm (eNumArgs - lhsNumArgs) discharge?
       else
         return none
+
+/--
+Reture 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
+disabled 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 }
+
 /--
 Remark: the parameter tag is used for creating trace messages. It is irrelevant otherwise.
 -/
 def rewrite? (e : Expr) (s : SimpTheoremTree) (erased : PHashSet Origin) (discharge? : Expr → SimpM (Option Expr)) (tag : String) (rflOnly : Bool) : SimpM (Option Result) := do
-  let candidates ← s.getMatchWithExtra e simpDtConfig
+  let candidates ← s.getMatchWithExtra e (getDtConfig (← getConfig))
   if candidates.isEmpty then
     trace[Debug.Meta.Tactic.simp] "no theorems found for {tag}-rewriting {e}"
     return none

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

@@ -80,8 +80,8 @@ def post (e : Expr) : M Step := do
 def discharge? (e : Expr) : M (Option Expr) := do
   (← read).discharge? e
 
-def getConfig : M Config :=
-  return (← readThe Context).config
+def getConfig : SimpM Config :=
+  return (← read).config
 
 @[inline] def withParent (parent : Expr) (f : M α) : M α :=
   withTheReader Context (fun ctx => { ctx with parent? := parent }) f

tests/lean/run/2669.lean

@@ -0,0 +1,15 @@
+def f : Nat → Nat := fun x => x - x
+
+@[simp] theorem f_zero (n : Nat) : f n = 0 :=
+  Nat.sub_self n
+
+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
+  sorry
+
+example (h : a = b) : (fun x => a + x) 0 = b := by
+  fail_if_success simp (config := { beta := false })
+  simp [*]