refactor: back rfl tactic primarily via apply_rfl

[nomeata]

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

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.

[nomeata]

(Likely needs a stage0 update after 8463000)

[nomeata]

I am a bit confused now. After a stage0 update, so that

@[builtin_tactic Lean.Parser.Tactic.applyRfl] def evalApplyRfl

kicks in I would have expected that with

syntax (name := applyRfl) "rfl" : tactic

the new code is used reliably.

Nevertheless

theorem add_le_iff_le_sub (a b c : Int) : a + b ≤ c ↔ a ≤ c - b := by
  conv =>
    lhs
    rw [← Int.add_zero c, ← Int.sub_self (-b), Int.sub_eq_add_neg, ← Int.add_assoc, Int.neg_neg,
      Int.add_le_add_iff_right]
  -- rfl here works, so why does the rfl within `conv` no work?

fails with

unsolved goals
abc: Int
⊢ a ≤ c + -b ↔ a ≤ c - b

It seems to me that somehow the

   evalTactic (← `(tactic| try rfl))

in

@[builtin_tactic Lean.Parser.Tactic.Conv.conv] def evalConv : Tactic := fun stx => do

is broken.

Maybe I can work around that, do another stage0 update, and then it works…

[digama0]

Your change changed the grammar, so you need to do an update-stage0 after it. The problem is that you removed a syntax node kind for the old refl, but conv and others from stage0 were elaborated with syntax quotations using rfl and so they have the old refl syntax node kind baked in. After removing the old syntax node kind these tactics will therefore produce ill formed syntax (not to mention that you also changed the syntax for applyRfl so even new syntax will be ill-formed, although the identity of the atom in the syntax usually doesn't matter).

[leanprover-community-mathlib4-bot]

Mathlib CI status (docs):

• ❌ Mathlib branch lean-pr-testing-3718 built against this PR, but linting failed. (2024-03-19 15:01:21) View Log
• ❌ Mathlib branch lean-pr-testing-3718 built against this PR, but linting failed. (2024-03-19 15:20:02) View Log
• ❌ Mathlib branch lean-pr-testing-3718 built against this PR, but linting failed. (2024-03-19 21:26:13) View Log
• 💥 Mathlib branch lean-pr-testing-3718 build failed against this PR. (2024-09-13 10:08:21) View Log
• 💥 Mathlib branch lean-pr-testing-3718 build failed against this PR. (2024-09-13 10:53:40) View Log
• 💥 Mathlib branch lean-pr-testing-3718 build failed against this PR. (2024-09-13 11:32:06) View Log
• 🟡 Mathlib branch lean-pr-testing-3718 build against this PR was cancelled. (2024-09-13 12:53:28) View Log
• 💥 Mathlib branch lean-pr-testing-3718 build failed against this PR. (2024-09-13 13:24:13) View Log
• 🟡 Mathlib branch lean-pr-testing-3718 build against this PR was cancelled. (2024-09-13 14:07:46) View Log
• ✅ Mathlib branch lean-pr-testing-3718 has successfully built against this PR. (2024-09-13 14:31:25) View Log
• 💥 Mathlib branch lean-pr-testing-3718 build failed against this PR. (2024-09-19 15:17:49) View Log
• 💥 Mathlib branch lean-pr-testing-3718 build failed against this PR. (2024-09-19 17:41:41) View Log
• ✅ Mathlib branch lean-pr-testing-3718 has successfully built against this PR. (2024-09-19 19:13:59) View Log
• ✅ Mathlib branch lean-pr-testing-3718 has successfully built against this PR. (2024-09-20 09:39:30) View Log
• ✅ Mathlib branch lean-pr-testing-3718 has successfully built against this PR. (2024-09-23 11:34:17) View Log
• ✅ Mathlib branch lean-pr-testing-3718 has successfully built against this PR. (2024-09-24 00:06:34) View Log
• ✅ Mathlib branch lean-pr-testing-3718 has successfully built against this PR. (2024-09-25 10:58:31) View Log

[nomeata]

I still see mathlib failures

 Error: ./././Mathlib/Analysis/NormedSpace/Star/ContinuousFunctionalCalculus/Instances.lean:223:35: error: type mismatch
  HEq.rfl
has type
  HEq ?m.240013 ?m.240013 : Prop
but is expected to have type
  IsSelfAdjoint 2 : Prop

which I did not expect. It seems that the macro_rules are duplicated in std4, proposing a fix at leanprover-community/batteries#702.

[nomeata]

(Edited…)

Compared the wrong revisions. Actually no significant change, as expected:
http://speed.lean-fro.org/mathlib4/compare/06e47b6a-c46f-4080-9596-b9b454a23113/to/67ef7d7c-5aa6-4d77-9c99-c9ef1755c289