feat: change apply_rfl tactic so that it does not operate on = (#3784)

Previously:

If the `rfl` macro was going to fail, it would:
1. expand to `eq_refl`, which is implemented by
`Lean.Elab.Tactic.evalRefl`, and call `Lean.MVarId.refl` which would:
* either try kernel defeq (if in `.default` or `.all` transparency mode)
  * otherwise try `IsDefEq`
  * then fail.
2. Next expand to the `apply_rfl` tactic, which is implemented by
`Lean.Elab.Tactic.Rfl.evalApplyRfl`, and call `Lean.MVarId.applyRefl`
which would look for lemmas labelled `@[refl]`, and unfortunately in
Mathlib find `Eq.refl`, so try applying that (resulting in another
`IsDefEq`)
3. Because of an accidental duplication, if `Lean.Elab.Tactic.Rfl` was
imported, it would *again* expand to `apply_rfl`.

Now:
1. Same behaviour in `eq_refl`.
2. The `@[refl]` attribute will reject `Eq.refl`, and `MVarId.applyRefl`
will fail when applied to equality goals.
3. The duplication has been removed.

src/Init/Tactics.lean

@@ -377,8 +377,9 @@ macro_rules | `(tactic| rfl) => `(tactic| eq_refl)
 macro_rules | `(tactic| rfl) => `(tactic| exact HEq.rfl)
 
 /--
-This tactic applies to a goal whose target has the form `x ~ x`, where `~` is a reflexive
-relation, that is, a relation which has a reflexive lemma tagged with the attribute [refl].
+This tactic applies to a goal whose target has the form `x ~ x`,
+where `~` is a reflexive relation other than `=`,
+that is, a relation which has a reflexive lemma tagged with the attribute @[refl].
 -/
 syntax (name := applyRfl) "apply_rfl" : tactic
 

src/Lean/Elab/Tactic/Rfl.lean

@@ -10,19 +10,12 @@ import Lean.Elab.Tactic.Basic
 /-!
 # `rfl` tactic extension for reflexive relations
 
-This extends the `rfl` tactic so that it works on any reflexive relation,
+This extends the `rfl` tactic so that it works on reflexive relations other than `=`,
 provided the reflexivity lemma has been marked as `@[refl]`.
 -/
 
 namespace Lean.Elab.Tactic.Rfl
 
-/--
-This tactic applies to a goal whose target has the form `x ~ x`, where `~` is a reflexive
-relation, that is, a relation which has a reflexive lemma tagged with the attribute [refl].
--/
-elab_rules : tactic
-  | `(tactic| rfl) => withMainContext do liftMetaFinishingTactic (·.applyRfl)
-
 @[builtin_tactic Lean.Parser.Tactic.applyRfl] def evalApplyRfl : Tactic := fun stx =>
   match stx with
   | `(tactic| apply_rfl) => withMainContext do liftMetaFinishingTactic (·.applyRfl)

src/Lean/Meta/Tactic/Rfl.lean

@@ -6,6 +6,7 @@ Authors: Newell Jensen, Thomas Murrills
 prelude
 import Lean.Meta.Tactic.Apply
 import Lean.Elab.Tactic.Basic
+import Lean.Meta.Tactic.Refl
 
 /-!
 # `rfl` tactic extension for reflexive relations
@@ -38,6 +39,8 @@ initialize registerBuiltinAttribute {
     let fail := throwError
       "@[refl] attribute only applies to lemmas proving x ∼ x, got {declTy}"
     let .app (.app rel lhs) rhs := targetTy | fail
+    if let .app (.const ``Eq [_]) _ := rel then
+      throwError "@[refl] attribute may not be used on `Eq.refl`."
     unless ← withNewMCtxDepth <| isDefEq lhs rhs do fail
     let key ← DiscrTree.mkPath rel reflExt.config
     reflExt.add (decl, key) kind
@@ -47,29 +50,33 @@ open Elab Tactic
 
 /-- `MetaM` version of the `rfl` tactic.
 
-This tactic applies to a goal whose target has the form `x ~ x`, where `~` is a reflexive
-relation, that is, a relation which has a reflexive lemma tagged with the attribute [refl].
+This tactic applies to a goal whose target has the form `x ~ x`,
+where `~` is a reflexive relation other than `=`,
+that is, a relation which has a reflexive lemma tagged with the attribute @[refl].
 -/
 def _root_.Lean.MVarId.applyRfl (goal : MVarId) : MetaM Unit := do
   let .app (.app rel _) _ ← whnfR <|← instantiateMVars <|← goal.getType
     | throwError "reflexivity lemmas only apply to binary relations, not{
         indentExpr (← goal.getType)}"
-  let s ← saveState
-  let mut ex? := none
-  for lem in ← (reflExt.getState (← getEnv)).getMatch rel reflExt.config do
-    try
-      let gs ← goal.apply (← mkConstWithFreshMVarLevels lem)
-      if gs.isEmpty then return () else
-        logError <| MessageData.tagged `Tactic.unsolvedGoals <| m!"unsolved goals\n{
-          goalsToMessageData gs}"
-    catch e =>
-      ex? := ex? <|> (some (← saveState, e)) -- stash the first failure of `apply`
-    s.restore
-  if let some (sErr, e) := ex? then
-    sErr.restore
-    throw e
+  if let .app (.const ``Eq [_]) _ := rel then
+    throwError "MVarId.applyRfl does not solve `=` goals. Use `MVarId.refl` instead."
   else
-    throwError "rfl failed, no lemma with @[refl] applies"
+    let s ← saveState
+    let mut ex? := none
+    for lem in ← (reflExt.getState (← getEnv)).getMatch rel reflExt.config do
+      try
+        let gs ← goal.apply (← mkConstWithFreshMVarLevels lem)
+        if gs.isEmpty then return () else
+          logError <| MessageData.tagged `Tactic.unsolvedGoals <| m!"unsolved goals\n{
+            goalsToMessageData gs}"
+      catch e =>
+        ex? := ex? <|> (some (← saveState, e)) -- stash the first failure of `apply`
+      s.restore
+    if let some (sErr, e) := ex? then
+      sErr.restore
+      throw e
+    else
+      throwError "rfl failed, no lemma with @[refl] applies"
 
 /-- Helper theorem for `Lean.MVarId.liftReflToEq`. -/
 private theorem rel_of_eq_and_refl {α : Sort _} {R : α → α → Prop}
@@ -78,7 +85,7 @@ private theorem rel_of_eq_and_refl {α : Sort _} {R : α → α → Prop}
 
 /--
 Convert a goal of the form `x ~ y` into the form `x = y`, where `~` is a reflexive
-relation, that is, a relation which has a reflexive lemma tagged with the attribute `[refl]`.
+relation, that is, a relation which has a reflexive lemma tagged with the attribute `@[refl]`.
 If this can't be done, returns the original `MVarId`.
 -/
 def _root_.Lean.MVarId.liftReflToEq (mvarId : MVarId) : MetaM MVarId := do

tests/lean/run/rewrites.lean

@@ -1,5 +1,3 @@
-attribute [refl] Eq.refl
-
 private axiom test_sorry : ∀ {α}, α
 
 -- To see the (sorted) list of lemmas that `rw?` will try rewriting by, use: