feat: track rfl simp theorems

See issue #1113

We need update stage0 before closing the issue.

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

@@ -60,10 +60,15 @@ private def tryTheoremCore (lhs : Expr) (xs : Array Expr) (bis : Array BinderInf
     if (← isDefEq lhs e) then
       unless (← synthesizeArgs thm.getName xs bis discharge?) do
         return none
-      let proof ← instantiateMVars (mkAppN val xs)
-      if ← hasAssignableMVar proof then
-        trace[Meta.Tactic.simp.rewrite] "{thm}, has unassigned metavariables after unification"
-        return none
+      let proof? ←
+        if thm.rfl then
+          pure none
+        else
+          let proof ← instantiateMVars (mkAppN val xs)
+          if (← hasAssignableMVar proof) then
+            trace[Meta.Tactic.simp.rewrite] "{thm}, has unassigned metavariables after unification"
+            return none
+          pure <| some proof
       let rhs := (← instantiateMVars type).appArg!
       if e == rhs then
         return none
@@ -72,7 +77,7 @@ private def tryTheoremCore (lhs : Expr) (xs : Array Expr) (bis : Array BinderInf
           trace[Meta.Tactic.simp.rewrite] "{thm}, perm rejected {e} ==> {rhs}"
           return none
       trace[Meta.Tactic.simp.rewrite] "{thm}, {e} ==> {rhs}"
-      return some { expr := rhs, proof? := proof }
+      return some { expr := rhs, proof? }
     else
       unless lhs.isMVar do
         -- We do not report unification failures when `lhs` is a metavariable
@@ -125,18 +130,19 @@ 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 Result := do
+def rewrite? (e : Expr) (s : DiscrTree SimpTheorem) (erased : Std.PHashSet Name) (discharge? : Expr → SimpM (Option Expr)) (tag : String) : 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}"
-    return { expr := e }
+    return none
   else
     let candidates := candidates.insertionSort fun e₁ e₂ => e₁.1.priority > e₂.1.priority
     for (thm, numExtraArgs) in candidates do
       unless inErasedSet thm do
         if let some result ← tryTheoremWithExtraArgs? e thm numExtraArgs discharge? then
-          return result
-    return { expr := e }
+          trace[Debug.Meta.Tactic.simp] "rewrite result {e} => {result.expr}"
+          return some result
+    return none
 where
   inErasedSet (thm : SimpTheorem) : Bool :=
     match thm.name? with
@@ -206,7 +212,7 @@ def simpArith? (e : Expr) : SimpM (Option Step) := do
 def simpMatchCore? (app : MatcherApp) (e : Expr) (discharge? : Expr → SimpM (Option Expr)) : SimpM (Option Step) := do
   for matchEq in (← Match.getEquationsFor app.matcherName).eqnNames do
     -- Try lemma
-    match (← withReducible <| Simp.tryTheorem? e { proof := mkConst matchEq, name? := some matchEq } discharge?) with
+    match (← withReducible <| Simp.tryTheorem? e { proof := mkConst matchEq, name? := some matchEq, rfl := (← isRflTheorem matchEq) } discharge?) with
     | none   => pure ()
     | some r => return some (Simp.Step.done r)
   return none
@@ -220,15 +226,13 @@ def simpMatch? (discharge? : Expr → SimpM (Option Expr)) (e : Expr) : SimpM (O
 
 def rewritePre (e : Expr) (discharge? : Expr → SimpM (Option Expr)) : SimpM Step := do
   for thms in (← read).simpTheorems do
-    let r ← rewrite e thms.pre thms.erased discharge? (tag := "pre")
-    if r.proof?.isSome then
+    if let some r ← rewrite? e thms.pre thms.erased discharge? (tag := "pre") then
       return Step.visit r
   return Step.visit { expr := e }
 
 def rewritePost (e : Expr) (discharge? : Expr → SimpM (Option Expr)) : SimpM Step := do
   for thms in (← read).simpTheorems do
-    let r ← rewrite e thms.post thms.erased discharge? (tag := "post")
-    if r.proof?.isSome then
+    if let some r ← rewrite? e thms.post thms.erased discharge? (tag := "post") then
       return Step.visit r
   return Step.visit { expr := e }
 

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

@@ -22,12 +22,24 @@ namespace Lean.Meta
 -/
 structure SimpTheorem where
   keys        : Array DiscrTree.Key := #[]
-  levelParams : Array Name := #[] -- non empty for local universe polymorphic proofs.
+  /--
+    It stores universe parameter names for universe polymorphic proofs.
+    Recall that it is non-empty only when we elaborate an expression provided by the user.
+    When `proof` is just a constant, we can use the universe parameter names stored in the declaration.
+   -/
+  levelParams : Array Name := #[]
   proof       : Expr
   priority    : Nat  := eval_prio default
   post        : Bool := true
-  perm        : Bool := false -- true is lhs and rhs are identical modulo permutation of variables
-  name?       : Option Name := none -- for debugging and tracing purposes
+  /-- `perm` is true if lhs and rhs are identical modulo permutation of variables. -/
+  perm        : Bool := false
+  /--
+    `name?` is mainly relevant for producing trace messages.
+    It is also viewed an `id` used to "erase" `simp` theorems from `SimpTheorems`.
+  -/
+  name?       : Option Name := none
+  /-- `rfl` is true if `proof` is by `Eq.refl` or `rfl`. -/
+  rfl         : Bool
   deriving Inhabited
 
 def SimpTheorem.getName (s : SimpTheorem) : Name :=
@@ -35,6 +47,28 @@ def SimpTheorem.getName (s : SimpTheorem) : Name :=
   | some n => n
   | none   => "<unknown>"
 
+def isRflProofCore (type : Expr) (proof : Expr) : Bool :=
+  match type with
+  | .forallE _ _ type _ =>
+    if let .lam _ _ proof _ := proof then
+      isRflProofCore type proof
+    else
+      false
+  | _ =>
+    type.isAppOfArity ``Eq 3
+    &&
+    (proof.isAppOfArity ``Eq.refl 2 || proof.isAppOfArity ``rfl 2)
+
+def isRflTheorem (declName : Name) : CoreM Bool := do
+  let .thmInfo info ← getConstInfo declName | return false
+  return isRflProofCore info.type info.value
+
+def isRflProof (proof : Expr) : CoreM Bool := do
+  if let .const declName .. := proof then
+    isRflTheorem declName
+  else
+    return false
+
 instance : ToFormat SimpTheorem where
   format s :=
     let perm := if s.perm then ":perm" else ""
@@ -195,7 +229,7 @@ private def mkSimpTheoremCore (e : Expr) (levelParams : Array Name) (proof : Exp
       match type.eq? with
       | some (_, lhs, rhs) => pure (← DiscrTree.mkPath lhs, ← isPerm lhs rhs)
       | none => throwError "unexpected kind of 'simp' theorem{indentExpr type}"
-    return { keys := keys, perm := perm, post := post, levelParams := levelParams, proof := proof, name? := name?, priority := prio }
+    return { keys, perm, post, levelParams, proof, name?, priority := prio, rfl := (← isRflProof proof) }
 
 private def mkSimpTheoremsFromConst (declName : Name) (post : Bool) (inv : Bool) (prio : Nat) : MetaM (Array SimpTheorem) := do
   let cinfo ← getConstInfo declName

src/Lean/Meta/Tactic/Split.lean

@@ -44,7 +44,7 @@ where
       | some e' => return Simp.Step.done { expr := e' }
       | none    =>
       -- Try lemma
-      match (← withReducible <| Simp.tryTheorem? e { proof := mkConst matchEqDeclName, name? := matchEqDeclName } SplitIf.discharge?) with
+      match (← withReducible <| Simp.tryTheorem? e { proof := mkConst matchEqDeclName, name? := matchEqDeclName, rfl := (← isRflTheorem matchEqDeclName) } SplitIf.discharge?) with
       | none => return Simp.Step.visit { expr := e }
       | some r => return Simp.Step.done r
     else

src/Lean/Meta/Tactic/Unfold.lean

@@ -23,7 +23,7 @@ def unfold (e : Expr) (declName : Name) : MetaM Simp.Result := do
     return { expr  := (← deltaExpand e (· == declName)) }
 where
   pre (unfoldThm : Name) (e : Expr) : SimpM Simp.Step := do
-    match (← withReducible <| Simp.tryTheorem? e { proof := mkConst unfoldThm, name? := some unfoldThm } (fun _ => return none)) with
+    match (← withReducible <| Simp.tryTheorem? e { proof := mkConst unfoldThm, name? := some unfoldThm, rfl := (← isRflTheorem unfoldThm) } (fun _ => return none)) with
     | none   => pure ()
     | some r => return Simp.Step.done r
     return Simp.Step.visit { expr := e }

tests/lean/rfl_simp_thm.lean

@@ -0,0 +1,8 @@
+def inc (x : Nat) := x + 1
+
+@[simp] theorem inc_eq : inc x = x + 1 := rfl
+
+theorem ex (a b : Fin (inc n)) (h : a = b) : b = a := by
+  simp only [inc_eq] at a
+  trace_state
+  exact h.symm

tests/lean/rfl_simp_thm.lean.expected.out

@@ -0,0 +1,5 @@
+n : Nat
+a : Fin (n + 1)
+b : Fin (inc n)
+h : a = b
+⊢ b = a