Attribute to map rewrite rules through a functor?

Stream: Is there code for X?

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

The category theory library has a useful attribute, @[reassoc], to generate a lemma f ≫ (g ≫ a) = h ≫ a from f ≫ g = h; simp can apply the former but not the latter after reassociating to the right. Another thing that sometimes happens is that we want to apply F.map f ≫ F.map g = F.map h as a simp rule, but this also will not trigger from just the original lemma; is there an attribute to automatically generate this (perhaps quantifying over all F)?

[Adam Topaz]

i think grind is supposed to eesolve all such issues

[Adam Topaz]

but the answer is no.

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

Is there a writeup anywhere of how grind will deal with situations like this one? In the meantime, I wrote the attribute by copy-pasting reassoc.

[Yaël Dillies]

Just to flag that @Andrew Yang have the same thought as you in the context of Toric

[Andrew Yang]

I suggest we have this in mathlib and tag every category theory lemma with this.

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

It would be quite a lot of lemmas added to the simp set.. I am mostly using these in a particular situation where we work with yoneda.map a lot. You also run into the funny situation of needing all of f ≫ g = h, f ≫ (g ≫ a) = h ≫ a, F.map f ≫ F.map g = F.map h, and F.map f ≫ (F.map g ≫ a) = F.map h ≫ a which is achieved via the monstrous @[functor_map (attr := reassoc (attr := simp))].

[Kevin Buzzard]

you might call it monstrous but it's pretty cool if that works.

[Yaël Dillies]

I think that actually the lemmas that are eligible for this new kind of auxiliary lemma generation are the same that are available for reassoc. So I think we don't need a new attribute at all, but merely an extension of reassoc.

[Robin Carlier]

If you want to make it an extension of reassoc, be aware that I have an open PR (#24303) modifying reassoc, so there might be some conflicts in the code.

[Kenny Lau]

(push)
we might also want attributes to convert between f ∘ g = h and f (g x) = h x?

[Calle Sönne]

There seems to be a bunch of these sort of attributes popping up now. For example @Robin Carlier wrote reassocIso (which was incoporated into @[reassoc]), and I wrote @[to_app]. Both of these (essentially) do the same thing: apply a function to the type of the lemma and then apply some chosen simp lemmas. I have been wondering if there should be some more general framework/attribute for these kinds of situation. Something like @[apply_fun arg] where arg can be Functor.map, Category.comp etc.

Although there will definitely be individual complications, but maybe there could be a very naive general framework that allows for specializations. For example, for @[reassoc] we need introduce a new morphism h before applying .comp. In @[to_app] we need to specialize a certain bicategory argument to Cat before being able to apply the function NatTrans.app (which also requires introducing an object X). The specialization here is also a bit tricky because a bicategory takes 3 universe variables, wheras Cat only needs two.

If these were all put in the same framework then there could also maybe be some simplified notation for chaining these together in a specified way (as in @𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒 's comment above). For example, it would be nice if I proved a lemma about isomorphisms in a bicategory, to be able to first specialize these using .hom and .inv and then on these new lemmas one can apply NatTrans.app as in @[to_app] (and then reassoc all the lemmas obtained).

[Calle Sönne]

(although I'm not sure if this can apply to @Kenny Lau 's comment above, so sorry for hijacking this)

[Christian Merten]

I was recently thinking about a specialize attribute that takes an arbitrary congr() pattern as its input, applies that to the lemma and runs a configurable post-processing step, e.g. apply dsimp on both sides. (We started hacking on this recently in our metaprogramming study group in Utrecht.)

[Robin Carlier]

Would this be able to generate some "simps"-like lemmas for constructor applications? E.g when working with sums of categories, simps can not generate lemmas that says something about a declaration specialized to an application of the constructors Sum.inl or Sum.inr, and we have to add manually lemmas like docs#CategoryTheory.Functor.sum_obj_inl.

I guess this is applying a congr to one of the argument of the declaration rather than at its output, so might be less easy.

[Kenny Lau]

https://github.com/leanprover-community/mathlib4/issues/26047

[Kenny Lau]

Btw there seems to be an elementwise attribute that I didn't know before; it automatically applies an element to an equality of commring homs