Algebra.Hom.GroupAction

Stream: mathlib4

[Kevin Buzzard]

I was trying to diagnose why the simp was failing in mathlib4#1424 and it seems to be the following thing (this works on mathlib master and can be massively minimised I'm sure)

import Mathlib.Algebra.GroupRingAction.Basic
import Mathlib.Algebra.Module.Basic

variable (M' : Type _)

variable (X : Type _) [SMul M' X]
variable (Y : Type _) [SMul M' Y]

structure MulActionHom where
  /-- The underlying function. -/
  toFun : X → Y
  /-- The proposition that the function preserves the action. -/
  map_smul' : ∀ (m : M') (x : X), toFun (m • x) = m • toFun x

@[inherit_doc]
notation:25 X " →[" M:25 "] " Y:0 => MulActionHom M X Y

variable (M : Type _) [Monoid M]

variable (A : Type _) [AddMonoid A] [DistribMulAction M A]
variable (B : Type _) [AddMonoid B] [DistribMulAction M B]

structure DistribMulActionHom extends A →[M] B, A →+ B

@[inherit_doc]
notation:25 A " →+[" M:25 "] " B:0 => DistribMulActionHom M A B

instance : Zero (A →+[M] B) :=
  ⟨{ (0 : A →+ B) with map_smul' := fun m x => by {
    -- src✝ : A →+ B := 0
    -- ⊢ ↑↑src✝ (m • x) = m • ↑↑src✝ x
    simp
    -- ⊢ ↑↑0 (m • x) = m • ↑↑0 x
    -- now let's change it to the goal we had in mathlib3 at this point
    change (0 : A →+ B) (m • x) = m • (0 : A →+ B) x
    simp -- now works
  }}⟩

Because of some change between Lean 3 and Lean 4 the goal is much more ugly in the Lean 4 version. simp removes the inaccessible variable but it doesn't have enough power to close the goal; presumably one could add more simp lemmas and fix the problem but then this would be an issue with divergence from mathlib3 I guess (for example if they're added later on in the port). I can imagine a lot more goals later on in the port being harder to prove because of this.

[Eric Wieser]

I suspect adding the missing fun_like instances in Lean3 would solve this

[Kevin Buzzard]

Aah I see!

[Eric Wieser]

I don't think we should spend any time on this file until we've done that

[Kevin Buzzard]

So in Lean 4 the missing lemmas are

@[simp]
lemma foo1 : AddMonoidHom.toZeroHom (0 : A →+ B) = 0 := rfl
@[simp] lemma foo2 (x : A) : ZeroHom.toFun (0 : ZeroHom A B) x = 0 := rfl

[Kevin Buzzard]

I'm not very good at naming conventions and I'm not very good at knowing where things go but if you just want to give me some hints I can make the mathlib3 PR

[Yaël Dillies]

zero_hom.coe_add_monoid_hom_zero, zero_hom.coe_zero, both simp and norm_cast

[Eric Wieser]

The first lemma shouldn't have coe in the name (in lean 3) since it is not about coe, and the second should be stated with ⇑ and already exist as docs4#ZeroHom.zero_apply (docs#zero_hom.zero_apply)

[Eric Wieser]

What's missing is the one that says ⇑(0 : ZeroHom A B) = 0

[Yaël Dillies]

Oh sorry I checked the existing lemmas and concluded this was the coe one, not the apply one

[Lukas Miaskiwskyi]

I've spent a little bit of time looking into this, and I think this particular example might not even require a mathlib3 port: What makes simp work again here is simply a theorem like

@[simp, to_additive]
theorem OneHom.toFun_eq_coe [One M] [One N] (f : OneHom M N) : f.toFun = f := rfl

And this exists in mathlib3! But it was taken out in the port of Algebra.Hom.Group. Overeagerly so, I'm guessing, because mathlib4#1219 intends to reintroduce it in a semi-big refactoring effort, and it looks like people generally think the things that are happening in that PR are the right things to do.

[Eric Wieser]

This is the wrong fix, the right fix is the FunLike instances

[Floris van Doorn]

Probably unrelated, but @[simp, to_additive] is now spelled @[to_additive (attr := simp)]

[Lukas Miaskiwskyi]

In the same file, there are also issues with coercion lemmas that come out as syntactic tautologies; the lean3 versions being (see also here)

@[simp] lemma to_fun_eq_coe (f : A →+[M] B) : f.to_fun = ⇑f := rfl
@[norm_cast] lemma coe_fn_coe' (f : A →+[M] B) : ((f : A →[M] B) : A → B) = f := rfl

(there are some "syntactic tautologies" in that file, but they are similar to these.)

I'm trying to get a feeling for this: to_fun_eq_coe should indeed turn into a syntactic equality and be removed no matter what, right? That is how I understand the porting wiki's remarks on coercions.

For the second one, both sides are unfolded to f.toMulActionHom.toFun, when maybe we'd rather want the lemma to unfold to

FunLike.coe (SMulHomClass.toMulActionHom f) = FunLike.coe f

If I look how similar instances are handled elsewhere in mathlib4, the approach in Algebra.Hom.Group would lead me to defining

@[coe]
def SMulHomClass.toMulActionHom [SMul M X] [SMul M Y] [SMulHomClass F M X Y]
  (f : F) : X →[M] Y :=
 { toFun := FunLike.coe f
   map_smul' := map_smul f}

instance [SMul M X] [SMul M Y] [SMulHomClass F M X Y] : CoeTC F (X →[M] Y) :=
  ⟨SMulHomClass.toMulActionHom⟩

I don't know why CoeTC comes in here while being generally discouraged in its tooltip, but we'll take it. And with this new instance (maybe this is what Eric meant with the FunLike instances), the translation

@[norm_cast]
theorem coe_fn_coe' (f : A →+[M] B) : ⇑(f : A →[M] B) = f :=
  rfl

causes no issue anymore with the linter and, when we remove some of the CoeFun instances in the file, unfolds exactly to the equation we hoped for. So, modulo backporting, is that what we want?

Apologies for mucho texto, coe is melting my brain. I'm just hoping this is easy enough to parse to the experts. Also tagging @Chris Hughes since he made remarks about this on the PR.

[Kevin Buzzard]

Much of what you say sounds fine to me. I don't really understand CoeTC yet.

[Eric Wieser]

maybe this is what Eric meant with the FunLike instances

I mean that in lean 3 we need a add_monoid_hom_class (A →+[M] B) (A → B) instance, and that porting the file is going to be a massive headache without that

[Eric Wieser]

(deleted)

[Eric Wieser]

Sorry, I'm being stupid; these instances already exist!

[Lukas Miaskiwskyi]

Thanks for clearing up the FunLike comment! I implemented the changes that I outlined in my previous post. They don't fix the simp issue that started the thread, but at least the syntactic tautologies stop being tautologies. Even lemmas like DistribMulActionHom.toFun_eq_coe (f : A →+[M] B): f.toFun = f, contrary to what I said earlier, now unfold to something meaningful, f.toMulActionHom.toFun = FunLike.coe f. The approach also seems consistent with mathlib4#1219, which, if accepted as the correct thing to do and merged, will fix the simp issue.