chore: ensure that the rfl tactic tries Iff.rfl

[Parcly-Taxel]

Revert the removal of the macro containing Iff.rfl in #5329; it was causing errors in leanprover-community/mathlib4#16839.

[leanprover-community-mathlib4-bot]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 078e9b6d778932430adf9ecbbf02e1025e922ce1 --onto 5eea8355baa64e6fda4e3874a0f45649d4c27633. (2024-09-16 07:14:12)
• ✅ Mathlib branch lean-pr-testing-5359 has successfully built against this PR. (2024-09-16 09:02:56) View Log
• ✅ Mathlib branch lean-pr-testing-5359 has successfully built against this PR. (2024-09-16 15:40:06) View Log

[nomeata]

Just curious: When does the difference matter?

[Parcly-Taxel]

Just curious: When does the difference matter?

When it's in leanprover-community/mathlib4#16839. And I needed no adaptation of mathlib at all here, unlike #5329.

[nomeata]

Hmm, but can you explain why it makes a difference? Because I’d expect the argument is solved by unification with the goal in any case.

Compare (e.g. on https://live.lean-lang.org/, without mathlib and without #5329 yet) that both these work:

attribute [refl] Iff.refl

example : True ↔ True := by apply_rfl

attribute [refl] Iff.refl

example : True ↔ True := by apply_rfl

[Parcly-Taxel]

Hmm, but can you explain why it makes a difference? Because I’d expect the argument is solved by unification with the goal in any case.

For the simple reason that Iff.refl takes one more explicit argument. If I try to change the fragment in Data.DFinsupp.Order to

/-- The order on `DFinsupp`s over a partial order embeds into the order on functions -/
def orderEmbeddingToFun : (Π₀ i, α i) ↪o ∀ i, α i where
  toFun := DFunLike.coe
  inj' := DFunLike.coe_injective
  map_rel_iff' := by exact Iff.refl

I get the very explanatory error

type mismatch
  Iff.refl
has type
  ∀ (a : Prop), a ↔ a : Prop
but is expected to have type
  { toFun := DFunLike.coe, inj' := ⋯ } a✝ ≤ { toFun := DFunLike.coe, inj' := ⋯ } b✝ ↔ a✝ ≤ b✝ : Prop
the following variables have been introduced by the implicit lambda feature
  a✝ : Π₀ (i : ι), α i
  b✝ : Π₀ (i : ι), α i
you can disable implicit lambdas using `@` or writing a lambda expression with `{}` or `[]` binder annotations.

[nomeata]

Ah, but apply_rfl uses apply, not exact, doesn’t it?

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

Line 68 in 45af92f

let gs ← goal.apply (← mkConstWithFreshMVarLevels lem)

I’d expect apply doesn’t mind which one we use here.

(Sorry for being an annoying reviewer her, but I’d just make sure we are not missing something here. Also in light of the imminent changes to the rfl tactic in #3714.)

[Parcly-Taxel]

@nomeata apply also fails, and it also fails with Iff.rfl.

/-- The order on `DFinsupp`s over a partial order embeds into the order on functions -/
def orderEmbeddingToFun : (Π₀ i, α i) ↪o ∀ i, α i where
  toFun := DFunLike.coe
  inj' := DFunLike.coe_injective
  map_rel_iff' := by apply Iff.refl

tactic 'apply' failed, failed to unify
  ∀ (a : Prop), a ↔ a
with
  ∀ {a b : Π₀ (i : ι), α i}, { toFun := DFunLike.coe, inj' := ⋯ } a ≤ { toFun := DFunLike.coe, inj' := ⋯ } b ↔ a ≤ b

But it succeeds if implicit variables are pulled away first:

/-- The order on `DFinsupp`s over a partial order embeds into the order on functions -/
def orderEmbeddingToFun : (Π₀ i, α i) ↪o ∀ i, α i where
  toFun := DFunLike.coe
  inj' := DFunLike.coe_injective
  map_rel_iff' {a b} := by apply Iff.refl -- `Iff.rfl` works here too

[nomeata]

Interesting, so it's the implicit variables in the goal that matter here! That might explain some of the adaption changes I had to do for my changes to rfl, that's good to know.

If with apply, neither works, are you sure that this PR fixes the problems? The comment in the mathlib PR that you linked said “hopeful”.

Maybe a test case should go with this PR to test this corner case behavior, and to make sure it isn't broken again in the future.

[Parcly-Taxel]

Maybe a test case should go with this PR to test this corner case behavior, and to make sure it isn't broken again in the future.

How am I to write a test case? What should I put in there?

[nomeata]

Some small, self-contained code that breaks with current master, and works after your change. Presumably setting up a goal with implicit foralls around an Iff goal. You can put it into test/lean/run/issue5359.lean

[Parcly-Taxel]

@nomeata I'm still confused. On current master this is what is working (without a @[refl] attribute on Iff.refl in mathlib):

/-- The order on `DFinsupp`s over a partial order embeds into the order on functions -/
def orderEmbeddingToFun : (Π₀ i, α i) ↪o ∀ i, α i where
  toFun := DFunLike.coe
  inj' := DFunLike.coe_injective
  map_rel_iff' := by rfl

In the testing branch for this PR it actually breaks. I can't find any code that works in this testing branch but not on master.

[nomeata]

I can't find any code that works in this testing branch but not on master.

Now I am confused, then what is this PR fixing?

[Parcly-Taxel]

Now I am confused, then what is this PR fixing?

In short, you were wrong to make me remove the macro in #5329. The lack of that macro is what led @semorrison to have me add adaptation notes in leanprover-community/mathlib4#16839.

I am now trying to make a mathlib-free test case that works on master but breaks on bump/v4.13.0. Here is my current progress:

import Mathlib.Logic.Equiv.Defs
import Mathlib.Order.Basic

universe u v

structure DFinsupp (β : Nat → Type u) where

instance {β} : DFunLike (DFinsupp β) Nat β := sorry

variable {α : Nat → Type u} [∀ i, LE (α i)]

instance : LE (DFinsupp α) := ⟨fun f g ↦ ∀ i, f i ≤ g i⟩

example : ∀ {a b : DFinsupp α}, DFunLike.coe a ≤ DFunLike.coe b ↔ a ≤ b := by
  rfl

[nomeata]

Hmm, yes, that may be. Or maybe I was wrong to rely on “OK, mathlib builds now. The necessary modifications were very small.”

In any case, clearly the lean4 test suite is insufficient, else it is hard to tell which behaviours are accidential and which are a feature. Thanks for condensing the issue!

[nomeata]

Thanks for the test case! That helped to understand the issue better; the underlying problem here is that exact is in a way more powerful than apply that I would consider surprising. I’ve opened #5366 to discuss.

[kim-em]

@nomeata, do you think it is reasonable to proceed with this PR in the meantime? It would allow us cleaning up the four regressions on Mathlib's nightlty-testing.

[nomeata]

Hmm, wouldn’t it be better to understand if they are really regressions, or use of an “accidental feature” first?

[nomeata]

But fair enough, we can change later. If rfl ends up using exact then some other proofs will break.