refactor: back rfl tactic primarily via apply_rfl (#3718)

building upon #3714, this (almost) implements the second half of #3302.

The main effect is that we now get a better error message when `rfl`
fails. For
```lean
example : n+1+m = n + (1+m) := by rfl
```
instead of the wall of text
```
The rfl tactic failed. Possible reasons:
- The goal is not a reflexive relation (neither `=` nor a relation with a @[refl] lemma).
- The arguments of the relation are not equal.
Try using the reflexivity lemma for your relation explicitly, e.g. `exact Eq.refl _` or
`exact HEq.rfl` etc.
n m : Nat
⊢ n + 1 + m = n + (1 + m)
```
we now get
```
error: tactic 'rfl' failed, the left-hand side
  n + 1 + m
is not definitionally equal to the right-hand side
  n + (1 + m)
n m : Nat
⊢ n + 1 + m = n + (1 + m)
```

Unfortunately, because of very subtle differences in semantics (which
transparency setting is used when reducing the goal and whether the
“implicit lambda” feature applies) I could not make this simply the only
`rfl` implementation. So `rfl` remains a macro and is still expanded to
`eq_refl` (difference transparency setting) and `exact Iff.rfl` and
`exact HEq.rfl` (implicit lambda) to not break existing code. This can
be revised later, so this still closes: #3302.

A user might still be puzzled *why* to terms are not defeq. Explaining
that better (“reduced to… and reduces to… etc.”) would also be great,
but that’s not specific to `rfl`, so better left for some other time.

src/Init/Core.lean

@@ -823,6 +823,7 @@ theorem iff_iff_implies_and_implies {a b : Prop} : (a ↔ b) ↔ (a → b) ∧ (
 protected theorem Iff.rfl {a : Prop} : a ↔ a :=
   Iff.refl a
 
+-- And, also for backward compatibility, we try `Iff.rfl.` using `exact` (see #5366)
 macro_rules | `(tactic| rfl) => `(tactic| exact Iff.rfl)
 
 theorem Iff.of_eq (h : a = b) : a ↔ b := h ▸ Iff.rfl

src/Init/Tactics.lean

@@ -364,31 +364,24 @@ syntax (name := fail) "fail" (ppSpace str)? : tactic
 syntax (name := eqRefl) "eq_refl" : tactic
 
 /--
-`rfl` tries to close the current goal using reflexivity.
-This is supposed to be an extensible tactic and users can add their own support
-for new reflexive relations.
-
-Remark: `rfl` is an extensible tactic. We later add `macro_rules` to try different
-reflexivity theorems (e.g., `Iff.rfl`).
+This tactic applies to a goal whose target has the form `x ~ x`,
+where `~` is equality, heterogeneous equality or any relation that
+has a reflexivity lemma tagged with the attribute @[refl].
 -/
-macro "rfl" : tactic => `(tactic| case' _ => fail "The rfl tactic failed. Possible reasons:
-- The goal is not a reflexive relation (neither `=` nor a relation with a @[refl] lemma).
-- The arguments of the relation are not equal.
-Try using the reflexivity lemma for your relation explicitly, e.g. `exact Eq.refl _` or
-`exact HEq.rfl` etc.")
-
-macro_rules | `(tactic| rfl) => `(tactic| eq_refl)
-macro_rules | `(tactic| rfl) => `(tactic| exact HEq.rfl)
+syntax "rfl" : tactic
 
 /--
-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].
+The same as `rfl`, but without trying `eq_refl` at the end.
 -/
 syntax (name := applyRfl) "apply_rfl" : tactic
 
+-- We try `apply_rfl` first, beause it produces a nice error message
 macro_rules | `(tactic| rfl) => `(tactic| apply_rfl)
 
+-- But, mostly for backward compatibility, we try `eq_refl` too (reduces more aggressively)
+macro_rules | `(tactic| rfl) => `(tactic| eq_refl)
+-- Als for backward compatibility, because `exact` can trigger the implicit lambda feature (see #5366)
+macro_rules | `(tactic| rfl) => `(tactic| exact HEq.rfl)
 /--
 `rfl'` is similar to `rfl`, but disables smart unfolding and unfolds all kinds of definitions,
 theorems included (relevant for declarations defined by well-founded recursion).

src/Lean/Elab/Tactic/Rfl.lean

@@ -16,6 +16,10 @@ 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].
+-/
 @[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

@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2022 Newell Jensen. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Newell Jensen, Thomas Murrills
+Authors: Newell Jensen, Thomas Murrills, Joachim Breitner
 -/
 prelude
 import Lean.Meta.Tactic.Apply
@@ -58,13 +58,13 @@ def _root_.Lean.MVarId.applyRfl (goal : MVarId) : MetaM Unit := goal.withContext
   -- NB: uses whnfR, we do not want to unfold the relation itself
   let t ← whnfR <|← instantiateMVars <|← goal.getType
   if t.getAppNumArgs < 2 then
-    throwError "rfl can only be used on binary relations, not{indentExpr (← goal.getType)}"
+    throwTacticEx `rfl goal "expected goal to be a binary relation"
 
   -- Special case HEq here as it has a different argument order.
   if t.isAppOfArity ``HEq 4 then
     let gs ← goal.applyConst ``HEq.refl
     unless gs.isEmpty do
-      throwError MessageData.tagged `Tactic.unsolvedGoals <| m!"unsolved goals\n{
+      throwTacticEx `rfl goal <| MessageData.tagged `Tactic.unsolvedGoals <| m!"unsolved goals\n{
         goalsToMessageData gs}"
     return
 
@@ -76,8 +76,8 @@ def _root_.Lean.MVarId.applyRfl (goal : MVarId) : MetaM Unit := goal.withContext
   unless success do
     let explanation := MessageData.ofLazyM (es := #[lhs, rhs]) do
       let (lhs, rhs) ← addPPExplicitToExposeDiff lhs rhs
-      return m!"The lhs{indentExpr lhs}\nis not definitionally equal to rhs{indentExpr rhs}"
-    throwTacticEx `apply_rfl goal explanation
+      return m!"the left-hand side{indentExpr lhs}\nis not definitionally equal to the right-hand side{indentExpr rhs}"
+    throwTacticEx `rfl goal explanation
 
   if rel.isAppOfArity `Eq 1 then
     -- The common case is equality: just use `Eq.refl`
@@ -86,6 +86,9 @@ def _root_.Lean.MVarId.applyRfl (goal : MVarId) : MetaM Unit := goal.withContext
     goal.assign (mkApp2 (mkConst ``Eq.refl us) α lhs)
   else
     -- Else search through `@refl` keyed by the relation
+    -- We change the type to `lhs ~ lhs` so that we do not the (possibly costly) `lhs =?= rhs` check
+    -- again.
+    goal.setType (.app t.appFn! lhs)
     let s ← saveState
     let mut ex? := none
     for lem in ← (reflExt.getState (← getEnv)).getMatch rel reflExt.config do
@@ -102,7 +105,7 @@ def _root_.Lean.MVarId.applyRfl (goal : MVarId) : MetaM Unit := goal.withContext
       sErr.restore
       throw e
     else
-      throwError "rfl failed, no @[refl] lemma registered for relation{indentExpr rel}"
+      throwTacticEx `rfl goal m!"no @[refl] lemma registered for relation{indentExpr rel}"
 
 /-- Helper theorem for `Lean.MVarId.liftReflToEq`. -/
 private theorem rel_of_eq_and_refl {α : Sort _} {R : α → α → Prop}

tests/lean/run/4644.lean

@@ -11,11 +11,10 @@ def check_sorted [x: LE α] [DecidableRel x.le] (a: Array α): Bool :=
   sorted_from_var a 0
 
 /--
-error: The rfl tactic failed. Possible reasons:
-- The goal is not a reflexive relation (neither `=` nor a relation with a @[refl] lemma).
-- The arguments of the relation are not equal.
-Try using the reflexivity lemma for your relation explicitly, e.g. `exact Eq.refl _` or
-`exact HEq.rfl` etc.
+error: tactic 'rfl' failed, the left-hand side
+  check_sorted #[0, 3, 3, 5, 8, 10, 10, 10]
+is not definitionally equal to the right-hand side
+  true
 ⊢ check_sorted #[0, 3, 3, 5, 8, 10, 10, 10] = true
 -/
 #guard_msgs in

tests/lean/run/rflReducibility.lean

@@ -0,0 +1,25 @@
+/-!
+The (attribute-extensible) `rfl` tactic only unfolds the goal with reducible transparency to look
+for a relation which may have a `refl` lemma associated with it. But historically, `rfl` also
+invoked `eq_refl`, which more aggressively unfolds. This checks that this still works.
+-/
+
+def Foo (a b : Nat) : Prop := a = b
+
+/--
+error: tactic 'rfl' failed, no @[refl] lemma registered for relation
+  Foo
+⊢ Foo 1 1
+-/
+#guard_msgs in
+example : Foo 1 1 := by
+  apply_rfl
+
+
+#guard_msgs in
+example : Foo 1 1 := by
+  eq_refl
+
+#guard_msgs in
+example : Foo 1 1 := by
+  rfl