Proof producing coherence tactic for monoidal categories

Stream: mathlib4

[Yuma Mizuno]

Recently I completely rewrote the coherence tactic in monoidal categories (and bicategories), which solves the goal like

example {C : Type} [Category C] [MonoidalCategory C] :
    (λ_ (𝟙_ C)).hom = (ρ_ (𝟙_ C)).hom := by
  monoidal_coherence

The current coherence tactic transport equalities from free monoidal categories by the monoidal functor F : FreeMonoidalCategory C ⥤ C. This example is a good explanation of what the tactic does. This approach works, but has a performance issue due to the heavy defeq at the transport. In fact, some proofs using coherence tacitc in mathlib almost reach the timeout.

The new coherence tactic is a proof producing tactic, which avoids heavy defeqs. It tunrs out that the new tactic is much faster than the current one especially when the expression is long.

Note that there is a similar comparison between the transporting tactic and the proof producing tactic in the case of ring, which is discussed at the thread #lean4 > Styles of reflective tactics .

The new coherence tactic combines the normalization procedure used in the string diagram widget to give us the general purpose tactic monoidal, which is similar to the current coherence tactic but much faster.

I have created a series of PRs about this new coherence tactic. These are somewhat lengthy meta PRs, but would someone be willing to review it? I believe the new tactic will be more useful in formalizing theorems formulated by the category theory.

• feat(CategoryTheory/MonoidalComp): change IsIso to Iso #16554
• feat(CategoryTheory): proof producing coherence tactic 1: datatypes #16562
• feat(CategoryTheory): proof producing coherence tactic 2-a: pureCoherence #16567
• feat(CategoryTheory): proof producing coherence tactic 2-b: normalize #16578
• feat(CategoryTheory): proof producing coherence tactic 3: main #16580
• feat(CategoryTheory): proof producing coherence tactic 4: integrate into mathlib #16606
• feat(CategoryTheory): proof producing coherence tactic 5: integrate into string diagram widget #16612
• feat(CategoryTheory): proof producing coherence tactic 6: bicategory #16629

[Johan Commelin]

cc @Heather Macbeth who was looking for examples of heavy rfls

[Kim Morrison]

@Yuma Mizuno, contrary to our usual practice of splitting into many small PRs, I think we may want to just merge this all in one go. I've had a very brief look, and am very positive so far.

Could you fix the missing module docs / merge conflicts, and run !bench on the final PR?

[Yuma Mizuno]

@Kim Morrison Thanks for the comment! I have made the all-in-one PR #16852.

[Yuma Mizuno]

Here is the benchmark result:

  Benchmark                                        Metric          Change
  =======================================================================
- build                                            compilation       5.2%
+ ~Mathlib.CategoryTheory.Bicategory.Adjunction    instructions    -86.5%
+ ~Mathlib.CategoryTheory.Monoidal.Bimod           instructions    -16.2%
+ ~Mathlib.CategoryTheory.Monoidal.Braided.Basic   instructions    -64.5%
+ ~Mathlib.CategoryTheory.Monoidal.Center          instructions    -51.8%
+ ~Mathlib.CategoryTheory.Monoidal.Rigid.Basic     instructions    -80.0%
- ~Mathlib.Tactic.Widget.StringDiagram             instructions   1021.1%

[Jakob von Raumer]

Sounds like I can finally close this call for students to do this as their master thesis. :octopus:

[Kim Morrison]

Okay! Any objections to merging? I have still only skimmed, but I'm not finding any problems, and it looks great.