Bug in reassoc?

Stream: mathlib4

[Adam Topaz]

In mathlib3, reassoc was used to generate the following lemma: docs#category_theory.monad.algebra.unit_assoc
In mathlib4, the reassoc attribute generates a lemma with the following type:

∀ {C : Type u₁} [inst : Category C] {T : Monad C} (self : Monad.Algebra T) {Z : C} (h : self.A ⟶ Z),
  (Monad.η T).app self.A ≫ self.a ≫ h = 𝟙 self.A ≫ h

Note that the RHS is a composition of an identity morphism with h, while the mathlib3 version doesn't have that identity on the RHS.

Is this expected?

[Adam Topaz]

It seems that the lean3 code simplifies using assoc, id_comp and comp_id when generating the lemma:
https://github.com/leanprover-community/mathlib/blob/8eb9c42d4d34c77f6ee84ea766ae4070233a973c/src/tactic/reassoc_axiom.lean#L82

And the lean4 code tries to do the same:
https://github.com/leanprover-community/mathlib4/blob/c9a607f6035bfd472080a5568493eefd447c3e2c/Mathlib/Tactic/Reassoc.lean#L39

I don't know why simplification is failing for this lemma.

[Matthew Ballard]

If you do the steps manually, it works fine?

[Matthew Ballard]

The lowercase a is a typo right? Nevermind different thing

[Adam Topaz]

no, that's the name for the structure morphism of an algebra for a monad.

[Adam Topaz]

example : ∀ {C : Type u₁} [inst : Category C] {T : Monad C} (X : Algebra T) {Z : C} (h : X.A ⟶ Z),
  (η T).app X.A ≫ X.a ≫ h = h := by
  intros C _ T X Z h
  have e := eq_whisker X.unit h
  -- e: ((η T).app X.A ≫ X.a) ≫ h = 𝟙 X.A ≫ h
  simp only [id_comp, comp_id, assoc] at e
  -- e: ((η T).app X.A ≫ X.a) ≫ h = 𝟙 X.A ≫ h
  -- sigh
  sorry

[Adam Topaz]

I have no clue why simp is failing here.

[Matthew Ballard]

rw?

[Adam Topaz]

yeah rw fails as well

[Matthew Ballard]

If you trace things, what does it say?

[Adam Topaz]

what do you suggest I trace here?

[Matthew Ballard]

Instance synthesis

[Adam Topaz]

I'm not sure that would reveal anything, but I'll try

[Matthew Ballard]

Don't see how but that has been the # 1 cause of failure for me in simp's or rw's

[Adam Topaz]

sigh, the issue is that lean4 is not eager to see that the identity functor applied to A is defeq to A.

[Adam Topaz]

If I change the definition of an algebra from

structure Algebra (T : Monad C) : Type max u₁ v₁ where
  /-- The underlying object associated to an algebra. -/
  A : C
  /-- The structure morphism associated to an algebra. -/
  a : (T : C ⥤ C).obj A ⟶ A
  /-- The unit axiom associated to an algebra. -/
  unit : T.η.app A ≫ a = 𝟙 A := by aesop_cat
  /-- The associativity axiom associated to an algebra. -/
  assoc : T.μ.app A ≫ a = (T : C ⥤ C).map a ≫ a := by aesop_cat

to

structure Algebra (T : Monad C) : Type max u₁ v₁ where
  /-- The underlying object associated to an algebra. -/
  A : C
  /-- The structure morphism associated to an algebra. -/
  a : (T : C ⥤ C).obj A ⟶ A
  /-- The unit axiom associated to an algebra. -/
  unit : T.η.app A ≫ a = 𝟙 _ := by aesop_cat
  /-- The associativity axiom associated to an algebra. -/
  assoc : T.μ.app A ≫ a = (T : C ⥤ C).map a ≫ a := by aesop_cat

then everything works fine.

[Adam Topaz]

And of course the value of _ that gets filled in is ((𝟭 C).obj X.A).

[Adam Topaz]

Perhaps reassoc should do some dsimplification as well?

[Adam Topaz]

Because this works:

example : ∀ {C : Type u₁} [inst : Category C] {T : Monad C} (X : Algebra T) {Z : C} (h : X.A ⟶ Z),
  (η T).app X.A ≫ X.a ≫ h = h := by
  intros C _ T X Z h
  have e := eq_whisker X.unit h
  -- e: ((η T).app X.A ≫ X.a) ≫ h = 𝟙 X.A ≫ h
  dsimp at e
  simp only [id_comp, comp_id, Category.assoc] at e
  exact e

with the original definition

[Adam Topaz]

Let's see what @Scott Morrison thinks.

[Adam Topaz]

This came up in !4#3528 FWIW

[Adam Topaz]

Here's a mathlib4 branch which makes such a change to reassoc. Let's see what breaks:
https://github.com/leanprover-community/mathlib4/compare/reassoc_test

[Adam Topaz]

It allows reassoc to use Functor.id_obj and similar things in the simplification step.

[Adam Topaz]

Okay, I got all of mathlib4 to build with this change to reassoc (in the same branch). Most things were smooth, and even smoother than before. There was one timeout in CategoryTheory.Idempotents.FunctorExtension which wasn't too bad to fix (and it seemed like @Joël Riou was running into timeout issues there anyway).

[Kyle Miller]

@Adam Topaz The sister tactic to reassoc is elementwise, so it might be worth comparing implementations, though if adding these lemmas to reassoc's simp set is enough to handle everything you need, I think this is a perfect change as-is.

For reference, here's the corresponding function for elementwise. It's more complicated because it needs to be able to apply @[simp] lemmas associated to particular concrete categories to get things into simp normal form. I didn't make similar changes to reassoc because I figured there wouldn't be any such lemmas, but if anything comes up I guess it's worth remembering that elementwise has a solution.

[Adam Topaz]

I opened a PR for this at !4#3531