From 20dd63aabf2de3bd740813df2ba1f41d500b1a44 Mon Sep 17 00:00:00 2001
From: Scott Morrison <scott.morrison@gmail.com>
Date: Tue, 12 Dec 2023 10:51:31 +1100
Subject: [PATCH] chore: fix superfluous lemmas in simp.trace (#2923)

Fixes an issue reported on Zulip; see the test case.

* Modifies the `MonadBacktrack` instance for `SimpM` to also backtrack
the `UsedSimps` field.
* When calling the discharger, `saveState`, and then `restoreState` if
something goes wrong.

I'm not certain that it makes sense to restore the `MetaM` state if
discharging fails. I can easily change this to more conservatively just
backtrack the `UsedSimps` after failed discharging.
---
 src/Lean/Meta/Tactic/Simp/Rewrite.lean        |  5 +++++
 tests/lean/simp_trace_backtrack.lean          | 19 +++++++++++++++++++
 .../simp_trace_backtrack.lean.expected.out    |  3 +++
 3 files changed, 27 insertions(+)
 create mode 100644 tests/lean/simp_trace_backtrack.lean
 create mode 100644 tests/lean/simp_trace_backtrack.lean.expected.out

diff --git a/src/Lean/Meta/Tactic/Simp/Rewrite.lean b/src/Lean/Meta/Tactic/Simp/Rewrite.lean
index f508092cf5..06c51e2e1c 100644
--- a/src/Lean/Meta/Tactic/Simp/Rewrite.lean
+++ b/src/Lean/Meta/Tactic/Simp/Rewrite.lean
@@ -37,13 +37,18 @@ def synthesizeArgs (thmId : Origin) (xs : Array Expr) (bis : Array BinderInfo) (
         if (← synthesizeInstance x type) then
           continue
       if (← isProp type) then
+        -- We save the state, so that `UsedTheorems` does not accumulate
+        -- `simp` lemmas used during unsuccessful discharging.
+        let usedTheorems := (← get).usedTheorems
         match (← discharge? type) with
         | some proof =>
           unless (← isDefEq x proof) do
             trace[Meta.Tactic.simp.discharge] "{← ppOrigin thmId}, failed to assign proof{indentExpr type}"
+            modify fun s => { s with usedTheorems }
             return false
         | none =>
           trace[Meta.Tactic.simp.discharge] "{← ppOrigin thmId}, failed to discharge hypotheses{indentExpr type}"
+          modify fun s => { s with usedTheorems }
           return false
   return true
 where
diff --git a/tests/lean/simp_trace_backtrack.lean b/tests/lean/simp_trace_backtrack.lean
new file mode 100644
index 0000000000..2448481fb1
--- /dev/null
+++ b/tests/lean/simp_trace_backtrack.lean
@@ -0,0 +1,19 @@
+-- As reported at https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/simp.3F.20giving.20nonsense.20lemmas/near/403082483
+
+universe u
+
+-- {α : Type} works as expected, as does specializing this lemma for `Nat`.
+@[simp]
+theorem tsub_eq_zero_of_le {α : Type u} [LE α] [Sub α] [OfNat α 0] {a b : α} :
+    a ≤ b → a - b = 0 := by sorry
+
+@[simp]
+theorem ge_iff_le (x y : Nat) : x ≥ y ↔ y ≤ x := Iff.rfl
+
+set_option tactic.simp.trace true
+
+-- This used to report: `Try this: simp only [ge_iff_le, Nat.succ_sub_succ_eq_sub]`
+-- because we were not backtracking the "used simps" when the discharger failed.
+example {n : Nat} : n = 2 - (n + 1) := by
+  simp [Nat.succ_sub_succ_eq_sub]
+  sorry
diff --git a/tests/lean/simp_trace_backtrack.lean.expected.out b/tests/lean/simp_trace_backtrack.lean.expected.out
new file mode 100644
index 0000000000..7df7cbe9c5
--- /dev/null
+++ b/tests/lean/simp_trace_backtrack.lean.expected.out
@@ -0,0 +1,3 @@
+simp_trace_backtrack.lean:7:8-7:26: warning: declaration uses 'sorry'
+Try this: simp only [Nat.succ_sub_succ_eq_sub]
+simp_trace_backtrack.lean:17:0-17:7: warning: declaration uses 'sorry'