simps + Trans

Stream: mathlib4

[Adam Topaz]

@Matthew Ballard found the following interesting looking lemma:
https://leanprover-community.github.io/mathlib4_docs/Mathlib/CategoryTheory/Functor/Currying.html#CategoryTheory.currying_unitIso_inv_app_app_app

It seems that the Trans.trans appearing there are not being simplified away as part of the simps lemma generation. I think the fix is to add some simps tag to the Trans instances we had to manually put in the category theory port. One example that seems to be the culprit in this case is the Trans instance for docs4#CategoryTheory.Iso . Another one I can think of is around docs4#CategoryTheory.Equivalence and there may be others as well, possibly even outside the category theory library.

By adding a simps tag to the instance here
https://github.com/leanprover-community/mathlib4/blob/7e974fd3806866272e9f6d9e44fa04c210a21f87/Mathlib/CategoryTheory/Iso.lean#L160

the lemma I linked above becomes a nice

CategoryTheory.currying_unitIso_inv_app_app_app:
      ∀ {C : Type u₂} [inst : CategoryTheory.Category C] {D : Type u₃} [inst_1 : CategoryTheory.Category D]
        {E : Type u₄} [inst_2 : CategoryTheory.Category E] (X : C ⥤ D ⥤ E) (X_1 : C) (X_2 : D),
        CategoryTheory.NatTrans.app
            (CategoryTheory.NatTrans.app (CategoryTheory.NatTrans.app CategoryTheory.currying.unitIso.inv X) X_1) X_2 =
          𝟙 (Prefunctor.obj (Prefunctor.obj X.toPrefunctor X_1).toPrefunctor X_2)

which also matches the mathlib3 version here:
https://leanprover-community.github.io/mathlib_docs/category_theory/functor/currying.html#category_theory.currying_unit_iso_hom_app_app_app

Does anyone see any reason not to go ahead and go through with this fix?

[Matthew Ballard]

The refl, symm, and trans attributes all seem to share a common issue. https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Tactic.20porting.20assignments/near/327682968

Would fixing those directly get simp firing?

[Floris van Doorn]

@Adam Topaz Yes, I think it's definitely fine to add @[simps] to that Trans instance.

[Adam Topaz]

Is the issue simply that refl, symm and trans tags are not generating simp lemmas which were generated in lean3?

[Matthew Ballard]

They are not generating instances for their appropriate classes 100% of the time

[Matthew Ballard]

    let .app (.app rel lhs) rhs := targetTy | fail

tries to match against the two types being related but it just takes the first two parameters (afaik)

[Matthew Ballard]

For at least one category theory problem, it was getting C and an the category instance on C

[Matthew Ballard]

Swapping the orders so that C and D came first fixed that in that particular case

[Adam Topaz]

oh I see yeah this is an issue, but I think it's separate from the issue in the thread above.

[Adam Topaz]

But maybe the @[trans] tag does generate the simp lemmas when it successfully generates the instance, and in this case, the issue you pointer out is the only issue

[Matthew Ballard]

My guess.

[Matthew Ballard]

But until someone has time to fix those, I think just making the instances by hand and tagging them makes the most sense

[Floris van Doorn]

I don't think @[trans] will ever generate any simp-lemmas (or even knows about the simp attribute).

[Adam Topaz]

ok so I guess I misunderstood how the attribute trans and refl actually work.

[Matthew Ballard]

Bad guess :)

[Adam Topaz]

!4#2421 just for now, until the trans attribute gets fixed.

[Matthew Ballard]

Wait, how did it work in Lean 3?

[Adam Topaz]

:ping_pong: for !4#2421 (it's holding up !4#2455 )