Coherence Tactic for Bicategories?

Stream: Is there code for X?

[Siddharth Bhat]

Prompted by @Emily Riehl 's requests for a tactic to discharge / simplify rewriting in bicategories, I've been reading through the files in Bicategory/, where I found a comment about a coherence tactic. Looking back at the history, it seems a categorical
coherence tactic existed in mathlib3, but did not seem to support bicategories (from my reading of the code. Please do correct me if I'm wrong, I don't know Lean3 at all).

I'm wondering if an extension of the tactic to bicategories was worked out on-paper, if not implemented? If there's an idea available I'd be happy to port/implement it to Lean4.

To motivate why we want this, consider a proof such as homEquiv₂, the calc blocks (shown below) should hopefully be obviated, and one should "simply be able" to rewrite with one of the triangle identities (adj.left_triangle), and have the tactic perform the appropriate rewrites?

-- https://github.com/leanprover-community/mathlib4/blob/45feb5a2692e7217df87d0a5e7efb1bb3b0cd881/Mathlib/CategoryTheory/Bicategory/Adjunction/Mate.lean#L88-L111
 def homEquiv₂ {g : a ⟶ b} {h : a ⟶ c} : (g ≫ l ⟶ h) ≃ (g ⟶ h ≫ r) where
   ...
   left_inv α :=
    calc
      _ = 𝟙 _ ⊗≫ g ◁ adj.unit ▷ l ⊗≫ (α ▷ (r ≫ l) ≫ h ◁ adj.counit) ⊗≫ 𝟙 _ := by
        bicategory
      _ = 𝟙 _ ⊗≫ g ◁ leftZigzag adj.unit adj.counit ⊗≫ α := by
        rw [← whisker_exchange]
        bicategory
      _ = α := by
        rw [adj.left_triangle]
        bicategory

[Kyle Miller]

There's a bicategory tactic in Mathlib (docs#Mathlib.Tactic.Bicategory.bicategory) that does coherence arguments for bicategories. There's also monoidal for monoidal categories.

[Siddharth Bhat]

Right, but in this particular case, what we really want to do is to rewrite with adj.left_triangle, and have the massaging of the proof goal be "automatically performed". If I understood the discussion with Emily correctly, the hard part is to convince Lean to figure out when to use whisker_exchange to correctly "isolate" the term that we want to perform adj.left_triangle on in the above proof.

[Kyle Miller]

I think I'm missing something — Is your question about whether there is a bicategorical coherence tactic? That seems like what you were asking, given that you were mentioning mathlib3's coherence and the porting history, and my understanding is the answer is "yes", it's bicategory. Or is it about mathlib3 coherence being able to do something that bicategory can't do? Or about getting bicategory to handle whisker_exchange automatically?

[Emily Riehl]

We're aware of @Yuma Mizuno's bicategory tactic. A question I've asked before, but still don't know the answer to, is whether it could be made more powerful to avoid the calculations needed for pasting diagram chases at present.

[Joël Riou]

As far as I understand the work of @Yuma Mizuno on this bicategory tactic which I have been using a little bit recently, it handles very well associators and unitors. Typical proofs are calc blocks where the user specifies the intermediate steps (without caring about associators and unitors which are automatically inserted by using ⊗≫). The proofs at each step usually involve a few rewrites (including whisker_exchange which is used in both directions) and a terminal bicategory.

Some serious mathematical insights are probably necessary in order to build a more powerful tactic!

[Yuma Mizuno]

Emily Riehl said:

A question I've asked before, but still don't know the answer to, is whether it could be made more powerful to avoid the calculations needed for pasting diagram chases at present.

I have several ideas I'd like to try, but I should say that in any case implementation requires some amount of programming. So I would say it can be done, but actually I'm not sure until I (or someone) have implemented it.

There are several possible things to do. For example, at the moment it's not possible to rw at 2-cells that are composed by ⊗≫. We have to write ≫ manually in the calc step. The direct manipulation on ⊗≫ requires some new feature. In my opinion, such rewriting feature will become part of a more powerful bicategory tactic rather than direct manual use.

One possible extension of bicategory tactic is that it can handle the reordering of 2-cells (by the above feature), just as the ring tactic handles multiplication in commutative rings.

[Yuma Mizuno]

(deleted)

[Yuma Mizuno]

Siddharth Bhat said:

Looking back at the history, it seems a categorical
coherence tactic existed in mathlib3, but did not seem to support bicategories (from my reading of the code. Please do correct me if I'm wrong, I don't know Lean3 at all).

The feature of the currect coherent tactic was already available in Lean 3 (but was slower).
https://leanprover-community.github.io/mathlib_docs/category_theory/bicategory/coherence_tactic.html

[Kim Morrison]

I am wondering if for many of these problems it would suffice to saturate with whisker_exchange via some form of congruence closure, and then see if anything in the the equivalence class can be dealt with via bicategory. My experience with these sort of proofs is that there are not that many (at most 10s?) of possibly orderings of the 2-morphisms that are reachable, so exhaustive search is pretty good.

[Siddharth Bhat]

Right. I tried throwing grind at it in an unprincipled fashion in the afternoon, and I was unable to find the correct set of rewrites to saturate. (I collected rewrites by scraping the included files, and rewrites from the coherence tactic).

I am surely missing some rewrites which are crucial. I planto mine the proof that bicategory generates carefully to see what rewrites I'm missing.

If someone wants to play with this, here's what I tried, taking an example from Mathlib/CategoryTheory/Bicategory/Adjunction/Mate.lean:

import Mathlib.CategoryTheory.Bicategory.Adjunction.Basic
import Mathlib.CategoryTheory.HomCongr
import Mathlib.CategoryTheory.Bicategory.Adjunction.Mate
import Mathlib.Tactic.CategoryTheory.Bicategory.PureCoherence
import Mathlib.CategoryTheory.Bicategory.Adjunction.Basic

universe w v u

namespace CategoryTheory
namespace Bicategory

open Mathlib Tactic
open Bicategory

variable {B : Type u} [Bicategory.{w, v} B]

variable {a b c d : B} {l : b ⟶ c} {r : c ⟶ b} (adj : l ⊣ r)


attribute [grind] leftZigzag rightZigzag
attribute [grind] whisker_exchange
attribute [grind] Adjunction.left_triangle
attribute[grind]
  whiskerLeft_id whiskerLeft_comp id_whiskerLeft comp_whiskerLeft id_whiskerRight comp_whiskerRight
  whiskerRight_id whiskerRight_comp whisker_assoc

attribute [grind] whiskerLeft_hom_inv


attribute [grind] hom_inv_whiskerRight
attribute [grind] whiskerLeft_inv_hom
attribute [grind] inv_hom_whiskerRight

attribute [grind] inv_whiskerRight
attribute [grind] pentagon_inv

attribute [grind] pentagon_inv_inv_hom_hom_inv
attribute [grind] pentagon_inv_hom_hom_hom_inv

attribute [grind] pentagon_hom_inv_inv_inv_inv
attribute [grind] pentagon_hom_hom_inv_hom_hom

attribute [grind] pentagon_hom_inv_inv_inv_hom

attribute [grind] pentagon_hom_hom_inv_inv_hom
attribute [grind] pentagon_inv_hom_hom_hom_hom
attribute [grind] pentagon_inv_inv_hom_inv_inv
attribute [grind] triangle_assoc_comp_left
attribute [grind] triangle_assoc_comp_right
attribute [grind] triangle_assoc_comp_right_inv
attribute [grind] associator_inv_naturality_left
attribute [grind] whiskerRight_comp_symm
attribute [grind] associator_naturality_middle
attribute [grind] associator_inv_naturality_middle
attribute [grind] whisker_assoc_symm
attribute [grind] associator_naturality_right
attribute [grind] associator_inv_naturality_right
attribute [grind] comp_whiskerLeft_symm
attribute [grind] leftUnitor_naturality
attribute [grind] leftUnitor_inv_naturality
attribute [grind] id_whiskerLeft_symm
attribute [grind] rightUnitor_naturality
attribute [grind] rightUnitor_inv_naturality
attribute [grind] whiskerRight_id_symm
attribute [grind] whiskerLeft_iff
attribute [grind] whiskerRight_iff
attribute [grind] leftUnitor_whiskerRight
attribute [grind] leftUnitor_inv_whiskerRight
attribute [grind] whiskerLeft_rightUnitor
attribute [grind] whiskerLeft_rightUnitor_inv
attribute [grind] leftUnitor_comp
attribute [grind] leftUnitor_comp_inv
attribute [grind] rightUnitor_comp
attribute [grind] rightUnitor_comp_inv
attribute [grind] unitors_equal
attribute [grind] unitors_inv_equal

attribute [grind] associatorNatIsoLeft
attribute [grind] associatorNatIsoMiddle
attribute [grind] associatorNatIsoRight
attribute [grind] leftUnitorNatIso
attribute [grind] rightUnitorNatIso

attribute [grind] Adjunction.unit
attribute [grind] Adjunction.counit
attribute [grind] Adjunction.left_triangle
attribute [grind] Adjunction.right_triangle

attribute [grind] Iso.symm
attribute [grind] Iso.refl
attribute [grind] Iso.trans
attribute [grind] Iso.trans_symm
attribute [grind] Iso.trans_refl


attribute [grind] naturality_associator
attribute [grind] naturality_leftUnitor
attribute [grind] naturality_rightUnitor
attribute [grind] naturality_id
-- attribute [grind] naturality_comp
attribute [grind] naturality_whiskerLeft
attribute [grind] naturality_whiskerRight
attribute [grind] naturality_inv


theorem CategoryTheory.Bicategory.homEquiv₁'.extracted_1 {b c d : B}
  {l : b ⟶ c} {r : c ⟶ b} (adj : l ⊣ r) {g : b ⟶ d} {h : c ⟶ d} (γ : g ⟶ l ≫ h) :
  (fun β => (λ_ g).inv ≫ adj.unit ▷ g ≫ (α_ l r g).hom ≫ l ◁ β)
      ((fun γ => r ◁ γ ≫ (α_ r l h).inv ≫ adj.counit ▷ h ≫ (λ_ h).hom) γ) =
    𝟙 g ⊗≫ (adj.unit ▷ g ≫ (l ≫ r) ◁ γ) ⊗≫ l ◁ adj.counit ▷ h ⊗≫ 𝟙 (l ≫ h) := by
    bicategory

#print CategoryTheory.Bicategory.homEquiv₁'.extracted_1

theorem CategoryTheory.Bicategory.homEquiv₁'.extracted_1' {b c d : B}
  {l : b ⟶ c} {r : c ⟶ b} (adj : l ⊣ r) {g : b ⟶ d} {h : c ⟶ d} (γ : g ⟶ l ≫ h) :
  (fun β => (λ_ g).inv ≫ adj.unit ▷ g ≫ (α_ l r g).hom ≫ l ◁ β)
      ((fun γ => r ◁ γ ≫ (α_ r l h).inv ≫ adj.counit ▷ h ≫ (λ_ h).hom) γ) =
    𝟙 g ⊗≫ (adj.unit ▷ g ≫ (l ≫ r) ◁ γ) ⊗≫ l ◁ adj.counit ▷ h ⊗≫ 𝟙 (l ≫ h) := by
    grind -- fails

#print CategoryTheory.Bicategory.homEquiv₁'.extracted_1


def homEquiv₁' {g : b ⟶ d} {h : c ⟶ d} : (g ⟶ l ≫ h) ≃ (r ≫ g ⟶ h) where
  toFun γ := r ◁ γ ≫ (α_ _ _ _).inv ≫ adj.counit ▷ h ≫ (λ_ _).hom
  invFun β := (λ_ _).inv ≫ adj.unit ▷ _ ≫ (α_ _ _ _).hom ≫ l ◁ β
  left_inv γ := by
    -- grind (config := {ematch := 10, gen := 10})

    calc
      _ = 𝟙 _ ⊗≫ (adj.unit ▷ g ≫ (l ≫ r) ◁ γ) ⊗≫ l ◁ adj.counit ▷ h ⊗≫ 𝟙 _:= by
        extract_goal
        bicategory
      _ = γ ⊗≫ leftZigzag adj.unit adj.counit ▷ h ⊗≫ 𝟙 _ := by
        rw [← whisker_exchange]
        bicategory
      _ = γ := by
        rw [adj.left_triangle]
        -- grind (config := {gen := 20}) [Adjunction, Bicategory, Quiver, Iso]
        bicategory
  right_inv β := by
    calc
      _ = 𝟙 _ ⊗≫ r ◁ adj.unit ▷ g ⊗≫ ((r ≫ l) ◁ β ≫ adj.counit ▷ h) ⊗≫ 𝟙 _ := by
        bicategory
      _ = 𝟙 _ ⊗≫ rightZigzag adj.unit adj.counit ▷ g ⊗≫ β := by
        rw [whisker_exchange]
        bicategory
      _ = β := by
        rw [adj.right_triangle]
        bicategory

end Bicategory

end CategoryTheory

[Kim Morrison]

Sorry, I don't have time to investigate grind in bicategories for at least a few months, but I like the idea, so good luck! :-)

[Kim Morrison]

Note that grind doesn't (yet? :fingers_crossed:) have support for arbitrary associative relations, so you are going to be saturating by Category.assoc before you even get to the 2-categorical layer. I would wait until we have that before trying seriously.

(Coming up with nice clean examples away from category theory that where normalizing arbitrary associative and/or commutative operations is helpful, would itself be helpful in getting this implemented in grind!)

[Siddharth Bhat]

From #lean4 > Quantifier Instantiation with Grind , it seems like I can't get grind to instantiate quantifiers, which seems quite crucial to get some proofs through. In particular, instantiating with Id strategically seems to be what's necessary in at least one proof I've been trying to grind down.

[Kim Morrison]

do you mean Category.id?

[Kim Morrison]

I've always done such proofs by hand as pure rewriting. e.g. docs#Hopf_Class.mul_antipode₂ is the sort of target you have in mind?

[Siddharth Bhat]

Kim Morrison said:

I've always done such proofs by hand as pure rewriting. e.g. docs#Hopf_Class.mul_antipode₂ is the sort of target you have in mind?

Ah, no, I was trying to automate id_of_comp_right_id:

theorem id_of_comp_right_id (f : X ⟶ X) (w : ∀ {Y : C} (g : Y ⟶ X), g ≫ f = g) : f = 𝟙 X := by
  convert w (𝟙 X)
  simp

The category theory proofs that I've surveyed seem instantiations with e.g. 𝟙. I don't follow how to do this with pure rewriting, as one needs to "invent" the constant 𝟙 to apply the rewrite?

[Kim Morrison]

I don't think that these proofs "scale". (i.e. you're quickly done with them all, so who cares if automation doesn't do them --- not to dismiss quantifier instantiation as an important goal, I just think this isn't the use case to motivate it.) Are there non-trivial calculations of this form?

[Siddharth Bhat]

@Kim Morrison That's a good point. Let me make a list of the category theory proofs that Emily was interested in, and see what kind of instantiation they needed.