feat: apply_rfl tactic: handle Eq, HEq, better error messages (#3714)

This implements the first half of #3302: It improves the extensible
`apply_rfl` tactic (the one that looks at `refl` attributes, part of
the `rfl` macro) to

* Check itself and ahead of time that the lhs and rhs are defEq, and
give
a nice consistent error message when they don't (instead of just passing
on
  the less helpful error message from `apply Foo.refl`), and using the 
machinery that `apply` uses to elaborate expressions to highlight diffs
  in implicit arguments.

* Also handle `Eq` and `HEq` (built in) and `Iff` (using the attribute)

Care is taken that, as before, the current transparency setting affects
comparing the lhs and rhs, but not the reduction of the relation

So before we had

```lean
opaque P : Nat → Nat → Prop
@[refl] axiom P.refl (n : Nat) : P n n

/--
error: tactic 'apply' failed, failed to unify
  P ?n ?n
with
  P 42 23
⊢ P 42 23
-/
#guard_msgs in
example : P 42 23 := by apply_rfl

opaque withImplicitNat {n : Nat} : Nat

/--
error: tactic 'apply' failed, failed to unify
  P ?n ?n
with
  P withImplicitNat withImplicitNat
⊢ P withImplicitNat withImplicitNat
-/
#guard_msgs in
example : P (@withImplicitNat 42) (@withImplicitNat 23) := by apply_rfl
```

and with this PR the messages we get are

```
error: tactic 'apply_rfl' failed, The lhs
  42
is not definitionally equal to rhs
  23
⊢ P 42 23
```
resp.
```
error: tactic 'apply_rfl' failed, The lhs
  @withImplicitNat 42
is not definitionally equal to rhs
  @withImplicitNat 23
⊢ P withImplicitNat withImplicitNat
```

A test file checks the various failure modes and error messages.

I believe this `apply_rfl` can serve as the only implementation of
`rfl`, which would then complete #3302, and actually expose these
improved
error messages to the user. But as that seems to require a
non-trivial bootstrapping dance, it’ll be separate.

src/Lean/Meta/Tactic/Refl.lean

@@ -12,6 +12,9 @@ namespace Lean.Meta
 
 /--
 Close given goal using `Eq.refl`.
+
+See `Lean.MVarId.applyRfl` for the variant that also consults `@[refl]` lemmas, and which
+backs the `rfl` tactic.
 -/
 def _root_.Lean.MVarId.refl (mvarId : MVarId) : MetaM Unit := do
   mvarId.withContext do

src/Lean/Meta/Tactic/Rfl.lean

@@ -50,33 +50,59 @@ 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 other than `=`,
-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, that is, equality or another 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)}"
-  if let .app (.const ``Eq [_]) _ := rel then
-    throwError "MVarId.applyRfl does not solve `=` goals. Use `MVarId.refl` instead."
+def _root_.Lean.MVarId.applyRfl (goal : MVarId) : MetaM Unit := goal.withContext do
+  -- 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)}"
+
+  -- 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{
+        goalsToMessageData gs}"
+    return
+
+  let rel := t.appFn!.appFn!
+  let lhs := t.appFn!.appArg!
+  let rhs := t.appArg!
+
+  let success ← approxDefEq <| isDefEqGuarded lhs rhs
+  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
+
+  if rel.isAppOfArity `Eq 1 then
+    -- The common case is equality: just use `Eq.refl`
+    let us := rel.appFn!.constLevels!
+    let α :=  rel.appArg!
+    goal.assign (mkApp2 (mkConst ``Eq.refl us) α lhs)
   else
+    -- Else search through `@refl` keyed by the relation
     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{
+          throwError MessageData.tagged `Tactic.unsolvedGoals <| m!"unsolved goals\n{
             goalsToMessageData gs}"
       catch e =>
-        ex? := ex? <|> (some (← saveState, e)) -- stash the first failure of `apply`
+        unless ex?.isSome do
+          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"
+      throwError "rfl failed, no @[refl] lemma registered for relation{indentExpr rel}"
 
 /-- Helper theorem for `Lean.MVarId.liftReflToEq`. -/
 private theorem rel_of_eq_and_refl {α : Sort _} {R : α → α → Prop}

stage0/src/stdlib_flags.h

@@ -18,3 +18,5 @@ options get_default_options() {
     return opts;
 }
 }
+
+// please update stage0

tests/lean/run/rflApplyFoApprox.lean

@@ -0,0 +1,15 @@
+
+opaque f : Nat → Nat
+-- A rewrite with a free variable on the RHS
+
+opaque P : Nat → (Nat → Nat) → Prop
+opaque Q : Nat → Prop
+opaque foo (g : Nat → Nat) (x : Nat) : P x f ↔ Q (g x) := sorry
+
+example : P x f ↔ Q (x + 10) := by
+  rewrite [foo]
+  -- we have an mvar now
+  with_reducible rfl -- should should instantiate it with the lambda on the RHS and close the goal
+  -- same as
+  -- with_reducible (apply (Iff.refl _))
+  -- NB: apply, not exact! Different defEq flags.