From bc03c21c215497f5a540502ae75bcc586b7453de Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leomoura@amazon.com>
Date: Sun, 22 Oct 2023 14:53:55 -0700
Subject: [PATCH] fix: fixes #2669 #2281

---
 src/Lean/Meta/Tactic/Simp/Rewrite.lean | 15 ++++++++++++++-
 src/Lean/Meta/Tactic/Simp/Types.lean   |  4 ++--
 tests/lean/run/2669.lean               | 15 +++++++++++++++
 3 files changed, 31 insertions(+), 3 deletions(-)
 create mode 100644 tests/lean/run/2669.lean

diff --git a/src/Lean/Meta/Tactic/Simp/Rewrite.lean b/src/Lean/Meta/Tactic/Simp/Rewrite.lean
index 54069aeffb73..61d70449738b 100644
--- a/src/Lean/Meta/Tactic/Simp/Rewrite.lean
+++ b/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
diff --git a/src/Lean/Meta/Tactic/Simp/Types.lean b/src/Lean/Meta/Tactic/Simp/Types.lean
index 5e43fd79f4f5..32470320397b 100644
--- a/src/Lean/Meta/Tactic/Simp/Types.lean
+++ b/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
diff --git a/tests/lean/run/2669.lean b/tests/lean/run/2669.lean
new file mode 100644
index 000000000000..e8ecb3458578
--- /dev/null
+++ b/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 [*]