feat: apply_rfl tactic: handle Eq, HEq, better error messages

[nomeata]

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

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.

[leanprover-community-mathlib4-bot]

Mathlib CI status (docs):

• ❗ Mathlib CI can not be attempted yet, as the nightly-testing-2024-03-19 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-mathlib, Mathlib CI should run now. (2024-03-19 09:43:25)
• ❌ Mathlib branch lean-pr-testing-3714 built against this PR, but linting failed. (2024-03-19 13:33:57) View Log
• ❌ Mathlib branch lean-pr-testing-3714 built against this PR, but linting failed. (2024-03-19 13:52:24) View Log
• 💥 Mathlib branch lean-pr-testing-3714 build failed against this PR. (2024-09-10 07:58:17) View Log
• 💥 Mathlib branch lean-pr-testing-3714 build failed against this PR. (2024-09-10 09:17:09) View Log
• ❌ Mathlib branch lean-pr-testing-3714 built against this PR, but the archive failed. (2024-09-10 11:10:48) View Log
• ✅ Mathlib branch lean-pr-testing-3714 has successfully built against this PR. (2024-09-10 14:27:39) View Log
• ✅ Mathlib branch lean-pr-testing-3714 has successfully built against this PR. (2024-09-11 09:49:40) View Log
• ✅ Mathlib branch lean-pr-testing-3714 has successfully built against this PR. (2024-09-13 10:57:06) View Log
• ✅ Mathlib branch lean-pr-testing-3714 has successfully built against this PR. (2024-09-14 10:38:21) View Log
• 💥 Mathlib branch lean-pr-testing-3714 build failed against this PR. (2024-09-15 22:12:07) View Log
• ❌ Mathlib branch lean-pr-testing-3714 built against this PR, but the archive failed. (2024-09-16 09:17:29) View Log
• ✅ Mathlib branch lean-pr-testing-3714 has successfully built against this PR. (2024-09-16 10:42:54) View Log
• ✅ Mathlib branch lean-pr-testing-3714 has successfully built against this PR. (2024-09-16 11:51:14) View Log
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase e417ad8a704fcc1b5b4e6fb316fbe0ae739fb586 --onto 77cd700fa877033316046f463f4c1b455b4498d2. (2024-09-18 20:04:22)
• ❗ Mathlib CI can not be attempted yet, as the nightly-testing-2024-09-19 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-mathlib, Mathlib CI should run now. (2024-09-19 14:29:29)
• 💥 Mathlib branch lean-pr-testing-3714 build failed against this PR. (2024-09-19 15:23:45) View Log
• ✅ Mathlib branch lean-pr-testing-3714 has successfully built against this PR. (2024-09-19 17:48:38) View Log

[digama0]

this seems like it should be a function somewhere

[nomeata]

Ah, interesting: The eq_refl tactic reduces the goal with the current transparency (whnf) before it checks if it is an Eq, while the extensible apply_rfl tactic reduces the goal only with reducible transparency (whnfR) before consulting the the @[refl] lemmas. This PR currently tries to do the whnfR same in both cases, but of course that breaks existing proofs.

So I should adjust this code to do these things as well (reduce with whnf, check if it is Eq, IfforHEq, handle that, else re-reduce with whnfR`, and handle that) to not have to chance down breakages.

[nomeata]

This is a bit unfortunate: since a given goal can look quite different under whnf and whnfR, in general there are also two different lhs/rhs pairs that need to be compared. And thus in the failure case, a comprehensive error message would have to somehow explain thas, requiring an annoying amount of code.

Given prominence of rfl, it's probably still with it…

(The alternative of using either whnf or whnfR exclusively is likely too disruptive…)