feat: apply rfl theorems at dsimp

closes #1113

RELEASES.md

@@ -1,6 +1,9 @@
 Unreleased
 ---------
 
+* Apply `rfl` theorems at the `dsimp` auxiliary method used by `simp`. `dsimp` can be used anywhere in an expression
+  because it preserves definitional equality.
+
 * Refine auto bound implicit feature. It does not consider anymore unbound variables that have the same
   name of a declaration being defined. Example:
   ```lean

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

@@ -157,7 +157,18 @@ private partial def reduce (e : Expr) : SimpM Expr := withIncRecDepth do
   | none => return e
 
 private partial def dsimp (e : Expr) : M Expr := do
-  transform e (post := fun e => return TransformStep.done (← reduce e))
+  let pre (e : Expr) : M TransformStep := do
+    if let Step.visit r ← rewritePre e (fun _ => pure none) (rflOnly := true) then
+      if r.expr != e then
+        return .visit r.expr
+    return .visit e
+  let post (e : Expr) : M TransformStep := do
+    if let Step.visit r ← rewritePost e (fun _ => pure none) (rflOnly := true) then
+      if r.expr != e then
+        return .visit r.expr
+    let eNew ← reduce e
+    if eNew != e then return .visit eNew else return .done e
+  transform e (pre := pre) (post := post)
 
 inductive SimpLetCase where
   | dep -- `let x := v; b` is not equivalent to `(fun x => b) v`

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

@@ -130,7 +130,7 @@ def tryTheorem? (e : Expr) (thm : SimpTheorem) (discharge? : Expr → SimpM (Opt
 /-
 Remark: the parameter tag is used for creating trace messages. It is irrelevant otherwise.
 -/
-def rewrite? (e : Expr) (s : DiscrTree SimpTheorem) (erased : Std.PHashSet Name) (discharge? : Expr → SimpM (Option Expr)) (tag : String) : SimpM (Option Result) := do
+def rewrite? (e : Expr) (s : DiscrTree SimpTheorem) (erased : Std.PHashSet Name) (discharge? : Expr → SimpM (Option Expr)) (tag : String) (rflOnly : Bool) : SimpM (Option Result) := do
   let candidates ← s.getMatchWithExtra e
   if candidates.isEmpty then
     trace[Debug.Meta.Tactic.simp] "no theorems found for {tag}-rewriting {e}"
@@ -138,7 +138,7 @@ def rewrite? (e : Expr) (s : DiscrTree SimpTheorem) (erased : Std.PHashSet Name)
   else
     let candidates := candidates.insertionSort fun e₁ e₂ => e₁.1.priority > e₂.1.priority
     for (thm, numExtraArgs) in candidates do
-      unless inErasedSet thm do
+      unless inErasedSet thm || (rflOnly && !thm.rfl) do
         if let some result ← tryTheoremWithExtraArgs? e thm numExtraArgs discharge? then
           trace[Debug.Meta.Tactic.simp] "rewrite result {e} => {result.expr}"
           return some result
@@ -224,15 +224,15 @@ def simpMatch? (discharge? : Expr → SimpM (Option Expr)) (e : Expr) : SimpM (O
   else
     return none
 
-def rewritePre (e : Expr) (discharge? : Expr → SimpM (Option Expr)) : SimpM Step := do
+def rewritePre (e : Expr) (discharge? : Expr → SimpM (Option Expr)) (rflOnly := false) : SimpM Step := do
   for thms in (← read).simpTheorems do
-    if let some r ← rewrite? e thms.pre thms.erased discharge? (tag := "pre") then
+    if let some r ← rewrite? e thms.pre thms.erased discharge? (tag := "pre") (rflOnly := rflOnly) then
       return Step.visit r
   return Step.visit { expr := e }
 
-def rewritePost (e : Expr) (discharge? : Expr → SimpM (Option Expr)) : SimpM Step := do
+def rewritePost (e : Expr) (discharge? : Expr → SimpM (Option Expr)) (rflOnly := false) : SimpM Step := do
   for thms in (← read).simpTheorems do
-    if let some r ← rewrite? e thms.post thms.erased discharge? (tag := "post") then
+    if let some r ← rewrite? e thms.post thms.erased discharge? (tag := "post") (rflOnly := rflOnly) then
       return Step.visit r
   return Step.visit { expr := e }
 

tests/lean/1113.lean

@@ -0,0 +1,16 @@
+def foo: {n: Nat} → Fin n → Nat
+|   0, _ => 0
+| n+1, _ => 0
+
+theorem t3 {f: Fin (n+1)}:
+  foo f = 0 := by
+  simp only [←Nat.succ_eq_add_one n] at f
+  trace_state
+  simp only [←Nat.succ_eq_add_one n, foo]
+
+example {n: Nat} {f: Fin (n+1)}:
+  foo f = 0 := by
+  revert f
+  rw[←Nat.succ_eq_add_one n]
+  intro f
+  simp only [foo]

tests/lean/1113.lean.expected.out

@@ -0,0 +1,3 @@
+n : Nat
+f : Fin (Nat.succ n)
+⊢ foo f = 0

tests/lean/run/ofNatNormNum.lean

@@ -38,7 +38,7 @@ instance [S α] : OfNat α n where
 instance [S α] : OfNatSound α where
   ofNat_add n m := by
     induction m with
-    | zero => simp [S.ofNat]; rw [Nat.add_zero]; erw [S.add_zero]; done
+    | zero => simp [S.ofNat]; erw [S.add_zero]; done
     | succ m ih => simp [OfNat.ofNat, S.ofNat] at *; erw [← ih]; rw [S.add_assoc]
 
 theorem S.ofNat_mul [S α] (n m : Nat) : (OfNat.ofNat n : α) * OfNat.ofNat m = OfNat.ofNat (n * m) := by