refl attribute

Stream: mathlib4

[Johan Commelin]

Does anybody know why

/-- Algebra equivalences are reflexive. -/
@[refl]
def refl : A₁ ≃ₐ[R] A₁ :=
  { (.refl _ : A₁ ≃+* A₁) with commutes' := fun _ => rfl }

works in Algebra/Algebra/Equiv.lean#L218

but

/-- Identity map as an `AffineEquiv`. -/
@[refl] -- Porting note: removed attribute
def refl : P₁ ≃ᵃ[k] P₁ where
  toEquiv := Equiv.refl P₁
  linear := LinearEquiv.refl k V₁
  map_vadd' _ _ := rfl

errors with

@[refl] attribute only applies to lemmas proving x ∼ x, got (k : Type u_1) →
  (P₁ : Type u_2) →
    {V₁ : Type u_6} →
      [inst : Ring k] → [inst_1 : AddCommGroup V₁] → [inst_2 : Module k V₁] → [inst_3 : AffineSpace V₁ P₁] → P₁ ≃ᵃ[k] P₁

in LinearAlgebra/AffineSpace/AffineEquiv.lean#L229

[Yaël Dillies]

Isn't it something about the order of the arguments to AffineEquiv vs AlgEquiv?

[Yaël Dillies]

Try reordering P and V

[Jz Pan]

Yaël Dillies said:

Isn't it something about the order of the arguments to AffineEquiv vs AlgEquiv?

I don't quite get the point. In fact I also met this problem at https://github.com/acmepjz/lean-iwasawa/blob/5e49802bc024d9227b40958045bee3a6604a68ac/Iwasawalib/RingTheory/PseudoNull/Basic.lean#L186. I tried to reorder variables, but it didn't work.

[Kyle Miller]

That's funny that this works. @[refl] isn't supposed to work there, and I think it accidentally does work for some dependent type reasons.

All the attribute looks for is that there are at least two arguments and that the last two are defeq. docs#AlgEquiv has at least two arguments, and the last two are the [Algebra R A] and [Algebra R B] instances. If you try to unify two instances, I think that will require that A and B be defeq, which is exactly what's needed for the relation.

It would be better I think if the explicit arguments were the ones that were being considered, but it's not the worst thing for the underlying algebra structures to be what's related in AlgEquiv.

[Aaron Liu]

Should rfl skip implicit arguments?

[Kyle Miller]

That's what I'm suggesting in the last paragraph, yes.

It's a little complicated though, since the current logic tries to do a just single defeq. The attribute needs to keep track of which arguments are explicit (or else the tactic needs to recompute this every time).

[Johan Commelin]

#24156 fixes AffineEquiv using the insight that we should reorder the typeclass variables. But admittedly, this is a bit of a hack...