chore: add refl attribute to Eq.refl

[semorrison]

Without this attribute, rw? doesn't work.

[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 e8a2786d6d4defa29f8991eb03e1dd975311e5ae --onto 4c0106d757d4d6d3b7f3903611ce22100d539d2a. (2024-03-26 10:56:55)

[nomeata]

Now rfl will try to solve the goal with equality twice, I fear. Not horrible, but kinda unsatisfying… #3714 could help, not sure though if I’ll follow through with that.

[semorrison]

Ugh.

(I guess Mathlib has been doing this all along, for what it's worth, but still this is no good.)

I'm heading off to bed, but I guess we want to change rw? so that it just makes a cheaper rfl attempt in the first place. @joehendrix?

[nomeata]

Is it this line where we need this?

lean4/src/Lean/Elab/Tactic/Rewrites.lean

Line 66 in e8a2786

evalTactic (← `(tactic| try rfl))

But rfl should do equality as well… so probably somewhere else?

Ah, maybe it’s this line:

lean4/src/Lean/Meta/Tactic/Rewrites.lean

Line 143 in e8a2786

withReducible (← mkFreshExprMVar res.eNew).mvarId!.applyRfl

Could this just use the rfl tactic as well, using evalTactic, as a stop-gap measure?

Or else run Lean.MVarId.refl first and catch if it fails to run applyRfl second, at least until #3714 is fixed.

[joehendrix]

@nomeata That second place looks like the right place.

It strikes me as a little strange to have two extension mechanisms for extending rfl. Should we try to consolidate?

With the current system, I think the right approach is to use the elaborator evalTactic (← ``(tactic| try rfl)) approach so that both kinds of user extension mechanisms have a chance to trigger.

Any disagreement?

[nomeata]

My attempt at consolidating is in #3714, and I plan to return to that.

Until then, evalTactic is certainly a reasonable choice.

[joehendrix]

I looked into this, and evalTactic (← ``(tactic| rfl)) would change the current behavior of rw? to use rfl in a context with default transparency rather than reducible. Given there's a test case for that, it seems like that's not desired.

I think using the attribute here is reasonable while we have two mechanisms like this. applyRfl looks up which refl lemma to use in a discriminator tree, so rfl will only check twice the term is a Eq.

[nomeata]

Looks like #3783 subsumes this?