feat: change apply_rfl tactic so that it does not operate on =

[kim-em]

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.

[leanprover-community-mathlib4-bot]

Mathlib CI status (docs):

• ❗ Std/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase b17c47d8526208db27105eafdf96a0668621c740 --onto 4c0106d757d4d6d3b7f3903611ce22100d539d2a. (2024-03-27 03:25:36)
• ❗ Std/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 16fdca1cbd603a05bd173584045adc9c13b38591 --onto b4caee80a3dfc5c9619d88b16c40cc3db90da4e2. (2024-03-27 11:57:04)

[kim-em]

I guess this should be considered as quicker / hackier alternative to #3714.

[nomeata]

Do we have a use case for failOnEq := false?

It seems we have

• End users calling rfl. They don’t need it.
• Tactics or Meta use that wants to work on Eq only. They can use eq_refl or with_reducible eq_refl resp. MVarId.refl or withReducible MVarId.refl as suitable.

Who wants to use MVarId.applyRfl, wants to handle more than Eq, but also wants to handle Eq, and can’t go via the rfl tactic?

(Also note that .applyRfl still behaves different than the rfl tactic. All very confusing.)

Preventing users from registering Eq.refl is fine.

[nomeata]

I guess I can grep mathlib myself…

There is

def rflTac : TacticM Unit :=
  withMainContext do liftMetaFinishingTactic (·.applyRfl)

which is corresponds to

src/Lean/Elab/Tactic/Rfl.lean:  | `(tactic| apply_rfl) => withMainContext do liftMetaFinishingTactic (·.applyRfl)

in core.

It is used in

attribute [aesop safe tactic (rule_sets := [CategoryTheory])] Mathlib.Tactic.rflTac

Then there is

/-- See if the term is `a = b` and the goal is `a ∼ b` or `b ∼ a`, with `∼` reflexive. -/
@[gcongr_forward] def exactRefl : ForwardExt where
  eval h goal := do
    let m ← mkFreshExprMVar none
    goal.assignIfDefeq (← mkAppOptM ``Eq.subst #[h, m])
    goal.applyRfl

in Mathlib/Tactic/GCongr/Core.lean. I’m not entirely sure, but it seems that here you don’t want to handle also Eq.

There is also

withReducible (← mkFreshExprMVar r.result.eNew).mvarId!.applyRfl

in Mathlib/Tactic/Rewrites.lean. Upstreamed and fixed with #3783.

And finally in rw_search we have

/-- Check whether a goal can be solved by `rfl`, and fill in the `SearchNode.rfl?` field. -/
def compute_rfl? (n : SearchNode) : MetaM SearchNode := withMCtx n.mctx do
  if (← try? n.goal.applyRfl).isSome then

and I wonder if that really wants to use applyRfl, and not .refl instead.

Hyrum’s law is strong again :-)

[kim-em]

I think this last one does want to use applyRfl, or at least there are test cases that expect it, so they can discharge Iff goals...

So when this PR lands, it will again break rw_search, and I'll patch it up to try .refl and then .applyRfl....