“implicit lambda” works with `exact`, but not `apply`

[nomeata]

I find this surprising:

example : {a : Nat} → a+1 = a.succ := rfl -- works
example : {a : Nat} → a+1 = a.succ := by exact rfl -- works
example : {a : Nat} → a+1 = a.succ := by apply rfl -- does not work

As a user I expect to apply work when exact works.

By using a wrong term we can see a bit more what’s happening:

example : {a : Nat} → a+1 = a.succ := by exact Iff.rfl

type mismatch
  Iff.rfl
has type
  ?m.960 ↔ ?m.960 : Prop
but is expected to have type
  a✝ + 1 = a✝.succ : Prop
the following variables have been introduced by the implicit lambda feature
  a✝ : Nat
you can disable implicit lambdas using `@` or writing a lambda expression with `{}` or `[]` binder annotations.

So exact somehow triggers “implicit lambda feature” but apply doesn’t. Should it?

Versions

4.12.0-nightly-2024-09-16

Additional Information

This causes unexpected(?) regressions(?) when using @[refl] rather than extending the rfl macro, #5359.

Impact

Add :+1: to issues you consider important. If others are impacted by this issue, please ask them to add :+1: to it.

[nomeata]

I haven’t interacted with the “implicit lambda feature” a lot yet, so I don’t have a good sense whether we have a problem here, and what the proper fix is.

[Parcly-Taxel]

Zulip seems to indicate that there is no problem here and that apply and exact need not have any strict relationship in strength.

[nomeata]

Hmm, but then the question is: Should applyRfl (and thus rfl) behave like exact instead of apply? It's muddy:

• We do have proofs in mathlib that requires the strength of apply here (approximate defeq), so switching to exact breaks something else.
• It would be great if rfl can always be replaced by the chosen refl lemma, with some basic lemma like apply or exact.
• It cannot be the solution to just keep the macro for Iff.refl around. Why Iff and not also all the other lemmas with [simp], like Perm.refl?

If these are accepted premises, it seems the only solutions are

• use either apply or exact in applyRfl and live with the fallout one way or the other in mathlib or
• make apply stronger (use implicit lambda feature)
• make exact stronger (approximate defeq)

[nomeata]

Related to #5359 and Iff.rfl specifically:

Currently (in lean stable, with the Iff.rfl macro) we have this behavior:

example : {a : Nat} → a+1 = a.succ         := by rfl        -- doesn’t work
example : {a : Nat} → a+1 = a.succ         := by intro; rfl -- works
example : {a : Nat} → a+1 = 5 ↔ a.succ = 5 := by rfl        -- works
example : {a : Nat} → a+1 = 5 ↔ a.succ = 5 := by intro; rfl -- works

This difference between Eq and Iff is silly!

Without #5359 we are getting

example : {a : Nat} → a+1 = a.succ         := by rfl        -- doesn’t work
example : {a : Nat} → a+1 = a.succ         := by intro; rfl -- works
example : {a : Nat} → a+1 = 5 ↔ a.succ = 5 := by rfl        -- doesn’t work
example : {a : Nat} → a+1 = 5 ↔ a.succ = 5 := by intro; rfl -- works

which I find more consistent and sensible.

This points to “using the rfl tactic should not implicitly introduces lambdas”, and thus https://github.com/leanprover/lean4/pull/5359 was a step in the wrong direction, and the there mentioned adaption fixes should just stay (i.e. write intro; rfl if the goal isn't a reflexive relation yet).

@semorrison, what do you think?

[digama0]

Your comment just made me realize that we have a funny inconsistency in precedence:

example : ((a : Nat) → True ↔ True) = ((a : Nat) → (True ↔ True)) := rfl
example : (Nat → True ↔ True) = ((Nat → True) ↔ True) := rfl

[kmill]

If these are accepted premises, it seems the only solutions are ...

I mentioned this privately, but I figured I'll mention a couple other ideas here as well:

• Make rfl be "binder tolerant" like mathlib's subsingleton tactic. That is, make it work as if it begins with intros. This minor amount of automation is a nicety, and it sidesteps questions about implicit lambda being active or not.
• Adjust Lean.Elab.Tactic.elabTermEnsuringType to do its defeq check with approximations enabled. This is justified by the fact that the defeq check is "post-elaboration", and the tactic otherwise fails if the defeq check fails. Users likely would accept approximate solutions from exact and refine (and maybe even want them!). This is a stronger version of your third solution, because it affects all tactics using this function.

[nomeata]

Hmm, both tempting ideas.

As for the first suggestion: I’m always a bit hesitant to make tactics do more than they have to do. Why should rfl (a tactic to solve reflexive goals) do intros, and shouldn’t by the same reason essentially every tactic do intros?

Personally I would find having to do stuff like this acceptable:

diff --git a/Mathlib/Algebra/Category/Ring/Basic.lean b/Mathlib/Algebra/Category/Ring/Basic.lean
index f195911a46493..8493abcccb639 100644
--- a/Mathlib/Algebra/Category/Ring/Basic.lean
+++ b/Mathlib/Algebra/Category/Ring/Basic.lean
@@ -391,7 +391,7 @@ instance hasForgetToSemiRingCat : HasForget₂ CommSemiRingCat SemiRingCat :=
 instance hasForgetToCommMonCat : HasForget₂ CommSemiRingCat CommMonCat :=
   HasForget₂.mk' (fun R : CommSemiRingCat => CommMonCat.of R) (fun R => rfl)
     -- Porting note: `(_ := _)` trick
-    (fun {R₁ R₂} f => RingHom.toMonoidHom (α := R₁) (β := R₂) f) (by rfl)
+    (fun {R₁ R₂} f => RingHom.toMonoidHom (α := R₁) (β := R₂) f) (by intros; rfl)

 /--
 Ring equivalence are isomorphisms in category of commutative semirings
@@ -549,7 +549,7 @@ instance hasForgetToRingCat : HasForget₂ CommRingCat RingCat :=
 /-- The forgetful functor from commutative rings to (multiplicative) commutative monoids. -/
 instance hasForgetToCommSemiRingCat : HasForget₂ CommRingCat CommSemiRingCat :=
   HasForget₂.mk' (fun R : CommRingCat => CommSemiRingCat.of R) (fun R => rfl)
-    (fun {R₁ R₂} f => f) (by rfl)
+    (fun {R₁ R₂} f => f) (by intros; rfl)

 instance : (forget₂ CommRingCat CommSemiRingCat).Full where map_surjective f := ⟨f, rfl⟩

The second suggestion does make sense to me, but I’m not an expert here.

[kmill]

An argument in support of auto-intros is that rfl is meant to be a closing tactic, and intros; rfl is a common pattern. Plus, intros never makes rfl fail, and it's cheap.

I think there are a number of closing tactics that could be improved with auto-intros, like perhaps ring and linarith, but I'd imagine the impact would be low due to it being rare to need intros before them. Non-closing tactics like simp/apply/exact/etc. would get really messed up by auto-intros.

(Re the approx defeq suggestion, it seems worth trying it out and seeing what the impact is. I don't have a very good sense of the full scope of the approximations.)