!4#2969 simps bug? (Monad.Basic)

Stream: PR reviews

[Scott Morrison]

In !4#2969 (already merged), @Jeremy Tan changed two appearances of @[simps] to @[simp] in CategoryTheory.Monad.Basic. I think that was incorrect, and in fact there is a bug in the implementation of simps that is revealed here.

At def ComonadIso.mk, changing the @[simp] back to @[simps] gives the error:

The definition CategoryTheory.ComonadIso.mk_hom_app is not a constructor application. Please use `@[simps!]` instead.

while changing it to @[simps!] gives the error

Invalid simp lemma CategoryTheory.ComonadIso.mk_hom_app.
The given definition is not a constructor application:
  f.1

as far as I can see mk_hom_app should be a fine simp lemma, and I'm not sure what is going wrong here.

@Floris van Doorn, would you be able to have a look at this? It's all in master, so should be easy to locate.

[Adam Topaz]

@Scott Morrison in mathlib3, I think the to_nat_trans projection is what was generated; see
https://leanprover-community.github.io/mathlib_docs/category_theory/monad/basic.html#category_theory.monad_iso.mk_hom_to_nat_trans

I ran into a similar issue here: https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/simps.20generates.20invalid.20simp.20lemma/near/344295530

The solution was to use [simps! toNatTrans]

[Adam Topaz]

But I agree that the app lemma seems reasonable

[Floris van Doorn]

In the category theory library, the correct solution is to add something like initialize_simps_projections MonoidalNatTrans (-app, +toNatTrans) to every structure that extends another structure. That gives the Lean 3 behavior.
There is also an open issue of still being recover in the current configuration (!4#2936), but that is a little tricky, so probably won't be fixed soon.

[Scott Morrison]

Great, this is resolved in https://github.com/leanprover-community/mathlib4/pull/3269.

[Adam Topaz]

If we have to do this for every single structure, what’s the benefit over @[simps! toNatTrans]?

[Floris van Doorn]

Then you'd have to do it for every new object in any of those structures, of which there are probably a lot more.