debug option, not trace option

Author: nomeata

src/Init/Data/List/Lemmas.lean

@@ -834,7 +834,7 @@ theorem getElem_length_sub_one_eq_getLast {l : List α} (h : l.length - 1 < l.le
   rw [← getLast_eq_getElem]
 
 @[simp, grind] theorem getLast_cons_cons {a : α} {l : List α} :
-    getLast (a :: b :: l) (by simp) = getLast (b :: l) (by simp) := by
+    getLast (a :: b :: l) (by simp) = getLast (b :: l) (by simp) :=
   rfl
 
 theorem getLast_cons {a : α} {l : List α} : ∀ (h : l ≠ nil),

src/Lean/Meta/Tactic/Simp.lean

@@ -28,7 +28,6 @@ builtin_initialize registerTraceClass `Meta.Tactic.simp.unify (inherited := true
 builtin_initialize registerTraceClass `Meta.Tactic.simp.ground (inherited := true)
 builtin_initialize registerTraceClass `Meta.Tactic.simp.numSteps
 builtin_initialize registerTraceClass `Meta.Tactic.simp.heads
-builtin_initialize registerTraceClass `Meta.Tactic.simp.rflAttrMismatch
 builtin_initialize registerTraceClass `Debug.Meta.Tactic.simp
 builtin_initialize registerTraceClass `Debug.Meta.Tactic.simp.congr (inherited := true)
 

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

@@ -218,15 +218,20 @@ where
     else
       let candidates := candidates.insertionSort fun e₁ e₂ => e₁.1.priority > e₂.1.priority
       for (thm, numExtraArgs) in candidates do
-        unless inErasedSet thm || (rflOnly && !thm.isRfl (← getEnv)) do
-          if let some result ← tryTheoremWithExtraArgs? e thm numExtraArgs then
-            trace[Debug.Meta.Tactic.simp] "rewrite result {e} => {result.expr}"
-            return some result
-        if !inErasedSet thm && rflOnly && !thm.isRfl (← getEnv) then
-            let r ← withOptions (experimental.tactic.simp.useRflAttr.set · false) do
-              isRflProof thm.proof
-            if r then
-              trace[Meta.Tactic.simp.rflAttrMismatch] "theorem {thm.proof} is no longer rfl"
+        if inErasedSet thm then continue
+        if rflOnly then
+          let isRfl := thm.isRfl (← getEnv)
+          if !isRfl then
+            if debug.tactic.simp.checkRflAttr.get (← getOptions) &&
+               experimental.tactic.simp.useRflAttr.get (← getOptions) then
+              let isRflOld ← withOptions (experimental.tactic.simp.useRflAttr.set · false) do
+                isRflProof thm.proof
+              if isRflOld then
+                logWarning "theorem {thm.proof} is no longer rfl"
+            continue
+        if let some result ← tryTheoremWithExtraArgs? e thm numExtraArgs then
+          trace[Debug.Meta.Tactic.simp] "rewrite result {e} => {result.expr}"
+          return some result
       return none
 
   /--

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

@@ -20,6 +20,13 @@ register_builtin_option experimental.tactic.simp.useRflAttr : Bool := {
   descr    := "use `rfl` attribute rather than theorem body to decide rfl-ness"
 }
 
+register_builtin_option debug.tactic.simp.checkRflAttr : Bool := {
+  defValue := false
+  descr    := "if true, whenever `dsimp` fails to apply a rewrite rule because it is not marked as \
+    `rfl`, check whether it would have been considered as a rfl theorem before the introduction of \
+    the `rfl` attribute, and warn if it was. Note that this is a costly check."
+}
+
 /--
 An `Origin` is an identifier for simp theorems which indicates roughly
 what action the user took which lead to this theorem existing in the simp set.