[Merged by Bors] - feat(category_theory/monoidal): coherence tactic #13125

semorrison · 2022-04-02T06:24:37Z

This is an alternative to #12697 (although this one does not handle bicategories!)

From the docstring:

Use the coherence theorem for monoidal categories to solve equations in a monoidal equation,
where the two sides only differ by replacing strings of "structural" morphisms with
different strings with the same source and target.

That is, `coherence` can handle goals of the form
`a ≫ f ≫ b ≫ g ≫ c = a' ≫ f ≫ b' ≫ g ≫ c'`
where `a = a'`, `b = b'`, and `c = c'` can be proved using `coherence1`.

This PR additionally provides a "composition up to unitors+associators" operation, so you can write

example {U V W X Y : C} (f : U ⟶ V ⊗ (W ⊗ X)) (g : (V ⊗ W) ⊗ X ⟶ Y) : U ⟶ Y := f ⊗≫ g

Co-authored-by: Yuma Mizuno mizuno.y.aj@gmail.com
Co-authored-by: Oleksandr Manzyuk manzyuk@gmail.com

manzyuk · 2022-04-02T09:13:41Z

I love this approach! It's exactly what I envisioned when I wrote this comment, and I'm very pleased by how simple the implementation turned out to be.

semorrison · 2022-04-02T10:29:12Z

I love this approach! It's exactly what I envisioned when I wrote this comment, and I'm very pleased by how simple the implementation turned out to be.

Yes, I was very pleased. I added both you and @yuma-mizuno to the authors line as coherence1 is based on your suggestions. At first I thought the full coherence tactic was going to involve lots of nasty working with lists, but it turned out to have a very simple recursive implementation. I was quite happy when I had the idea to write liftable_prefixes.

src/category_theory/monoidal/coherence.lean

manzyuk · 2022-04-02T12:52:57Z

Very clean! I feel like I can even follow the definitions of the tactics although I haven't yet explored metaprogramming in Lean. I don't see any issues with this PR but I'm an unexperienced Lean user, so I've added @yuma-mizuno as a reviewer.

Co-authored-by: Oleksandr Manzyuk <manzyuk@gmail.com>

…y/mathlib into semorrison/coherence

yuma-mizuno

LGTM modulo some comments and questions.

src/category_theory/monoidal/coherence.lean

yuma-mizuno

Let me make an additional comment about the definition of coherence tactic. It might be better to place liftable_prefixes outside the recursive call as it actually rewrites the entire expression at once, not just the head of the expression. I think this change will improve performance and reduce the chance of unintended behavior. The following is just one suggestion.

meta def coherence_loop : tactic unit :=
  pure_coherence <|> do
  tactic.congr_core',
  focus1 pure_coherence <|>
    fail "`coherence` tactic failed, subgoal not true in the free bicategory",
  reflexivity <|> (do
    `(_ ≫ _ = _ ≫ _) ← target |
      fail "`coherence` tactic failed, non-structural morphisms don't match",
    tactic.congr_core',
    reflexivity <|> fail "`coherence` tactic failed, non-structural morphisms don't match",
    coherence_loop)

meta def coherence : tactic unit :=
do
  pure_coherence <|> do
  liftable_prefixes <|>
    fail ("Something went wrong in the `coherence` tactic: " ++
      "is the target an equation in a bicategory?"),
  coherence_loop

semorrison · 2022-04-03T22:18:42Z

It might be better to place liftable_prefixes outside the recursive call as it actually rewrites the entire expression at once, not just the head of the expression.

Thank you, I had missed this, and your proposed refactor is indeed clearer (and avoids pointless work). I've added that now.

yuma-mizuno · 2022-04-03T22:20:38Z

Umm, now I notice that liftable_prefixes needs to be executed in recursive calls when there is successive non-structural morphisms because this tactic inserts the identity.

…hisms (#13185) ## Problem The definition of bicategories contains the following axioms: ```lean associator_naturality_left : ∀ {f f' : a ⟶ b} (η : f ⟶ f') (g : b ⟶ c) (h : c ⟶ d), (η ▷ g) ▷ h ≫ (α_ f' g h).hom = (α_ f g h).hom ≫ η ▷ (g ≫ h) associator_naturality_middle : ∀ (f : a ⟶ b) {g g' : b ⟶ c} (η : g ⟶ g') (h : c ⟶ d), (f ◁ η) ▷ h ≫ (α_ f g' h).hom = (α_ f g h).hom ≫ f ◁ (η ▷ h) associator_naturality_right : ∀ (f : a ⟶ b) (g : b ⟶ c) {h h' : c ⟶ d} (η : h ⟶ h'), (f ≫ g) ◁ η ≫ (α_ f g h').hom = (α_ f g h).hom ≫ f ◁ (g ◁ η) left_unitor_naturality : ∀ {f g : a ⟶ b} (η : f ⟶ g), 𝟙 a ◁ η ≫ (λ_ g).hom = (λ_ f).hom ≫ η right_unitor_naturality : ∀ {f g : a ⟶ b} (η : f ⟶ g) : η ▷ 𝟙 b ≫ (ρ_ g).hom = (ρ_ f).hom ≫ η ``` By using these axioms, we can see that, for example, 2-morphisms `(f₁ ≫ f₂) ◁ (f₃ ◁ (η ▷ (f₄ ≫ f₅)))` and `f₁ ◁ ((𝟙_ ≫ f₂ ≫ f₃) ◁ ((η ▷ f₄) ▷ f₅))` are equal up to some associators and unitors. The problem is that the proof of this fact requires tedious rewriting. We should insert appropriate associators and unitors, and then rewrite using the above axioms manually. This tedious rewriting is also a problem when we use the (forthcoming) `coherence` tactic (bicategorical version of #13125), which only works if the non-structural 2-morphisms in the LHS and the RHS are the same. ## Main change The main proposal of this PR is to introduce a normal form of such 2-morphisms, and put simp attributes to suitable lemmas in order to rewrite any 2-morphism into the normal form. For example, the normal form of the previouse example is `f₁ ◁ (f₂ ◁ (f₃ ◁ ((η ▷ f₄) ▷ f₅)))`. The precise definition of the normal form can be found in the docs in `basic.lean` file. The new simp lemmas introduced in this PR are the following: ```lean whisker_right_comp : ∀ {f f' : a ⟶ b} (η : f ⟶ f') (g : b ⟶ c) (h : c ⟶ d), η ▷ (g ≫ h) = (α_ f g h).inv ≫ η ▷ g ▷ h ≫ (α_ f' g h).hom whisker_assoc : ∀ (f : a ⟶ b) {g g' : b ⟶ c} (η : g ⟶ g') (h : c ⟶ d), (f ◁ η) ▷ h = (α_ f g h).hom ≫ f ◁ (η ▷ h) ≫ (α_ f g' h).inv comp_whisker_left : ∀ (f : a ⟶ b) (g : b ⟶ c) {h h' : c ⟶ d} (η : h ⟶ h'), (f ≫ g) ◁ η = (α_ f g h).hom ≫ f ◁ g ◁ η ≫ (α_ f g h').inv id_whisker_left : ∀ {f g : a ⟶ b} (η : f ⟶ g), 𝟙 a ◁ η = (λ_ f).hom ≫ η ≫ (λ_ g).inv whisker_right_id : ∀ {f g : a ⟶ b} (η : f ⟶ g), η ▷ 𝟙 b = (ρ_ f).hom ≫ η ≫ (ρ_ g).inv ``` Logically, these are equivalent to the five axioms presented above. The point is that these equalities have the definite simplification direction. ## Improvement Some proofs that had been based on tedious rewriting are now automated. For example, the conditions in `oplax_nat_trans.id`, `oplax_nat_trans.comp`, and several functions in `functor_bicategory.lean` are now proved by `tidy`. ## Specific changes - The new simp lemmas `whisker_right_comp` etc. actually have been included in the definition of bicategories instead of `associate_naturality_left` etc. so that the latter lemmas are proved in later of the file just by `simp`. - The precedence of the whiskering notations "infixr ` ◁ `:70" and "infixr ` ◁ `:70" have been changed into "infixr ` ◁ `:81" and "infixr ` ◁ `:81", which is now higher than that of the composition `≫`. This setting is consistent with the normal form introduced in this PR in the sence that an expression is in normal form only if it has the minimal number of parentheses in this setting. For example, the normal form `f₁ ◁ (f₂ ◁ (f₃ ◁ ((η ▷ f₄) ▷ f₅)))` can be written as `f₁ ◁ f₂ ◁ f₃ ◁ η ▷ f₄ ▷ f₅`. - The unneeded parentheses caused by the precedence change have been removed. - The lemmas `whisker_right_id` and `whisker_right_comp` have been renamed to `id_whisker_right` and `comp_whisker_right` since these are more consistent with the notation. Note that the name `whisker_right_id` and `whisker_right_comp` are now used for the two of the five simp lemmas presented above. - The lemmas in `basic.lean` have been rearranged to be more logically consistent. ## Future work I would like to apply a similar strategy for monoidal categories.

src/category_theory/monoidal/coherence.lean

jcommelin · 2022-04-08T14:41:32Z

Do I understand correctly that this is a finishing tactic? That is, one shouldn't try to use it to normalize expressions in the middle of a proof? Could it be made to do that?

Co-authored-by: Johan Commelin <johan@commelin.net>

semorrison · 2022-04-09T01:07:23Z

Do I understand correctly that this is a finishing tactic? That is, one shouldn't try to use it to normalize expressions in the middle of a proof? Could it be made to do that?

Yes, for now it is a finishing tactic, and will fail unless it closes the goal. A normalization tactic would be a good subsequent addition.

jcommelin · 2022-04-09T06:28:46Z

bors d+

bors · 2022-04-09T06:28:47Z

✌️ semorrison can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

semorrison · 2022-04-10T00:50:12Z

bors merge

This is an alternative to #12697 (although this one does not handle bicategories!) From the docstring: ``` Use the coherence theorem for monoidal categories to solve equations in a monoidal equation, where the two sides only differ by replacing strings of "structural" morphisms with different strings with the same source and target. That is, `coherence` can handle goals of the form `a ≫ f ≫ b ≫ g ≫ c = a' ≫ f ≫ b' ≫ g ≫ c'` where `a = a'`, `b = b'`, and `c = c'` can be proved using `coherence1`. ``` This PR additionally provides a "composition up to unitors+associators" operation, so you can write ``` example {U V W X Y : C} (f : U ⟶ V ⊗ (W ⊗ X)) (g : (V ⊗ W) ⊗ X ⟶ Y) : U ⟶ Y := f ⊗≫ g ``` Co-authored-by: Scott Morrison <scott.morrison@gmail.com> Co-authored-by: yuma-mizuno <mizuno.y.aj@gmail.com>

bors · 2022-04-10T04:05:09Z

Build failed (retrying...):

Build mathlib

This is an alternative to #12697 (although this one does not handle bicategories!) From the docstring: ``` Use the coherence theorem for monoidal categories to solve equations in a monoidal equation, where the two sides only differ by replacing strings of "structural" morphisms with different strings with the same source and target. That is, `coherence` can handle goals of the form `a ≫ f ≫ b ≫ g ≫ c = a' ≫ f ≫ b' ≫ g ≫ c'` where `a = a'`, `b = b'`, and `c = c'` can be proved using `coherence1`. ``` This PR additionally provides a "composition up to unitors+associators" operation, so you can write ``` example {U V W X Y : C} (f : U ⟶ V ⊗ (W ⊗ X)) (g : (V ⊗ W) ⊗ X ⟶ Y) : U ⟶ Y := f ⊗≫ g ``` Co-authored-by: Scott Morrison <scott.morrison@gmail.com> Co-authored-by: yuma-mizuno <mizuno.y.aj@gmail.com>

bors · 2022-04-10T09:05:00Z

Build failed (retrying...):

Build mathlib

This is an alternative to #12697 (although this one does not handle bicategories!) From the docstring: ``` Use the coherence theorem for monoidal categories to solve equations in a monoidal equation, where the two sides only differ by replacing strings of "structural" morphisms with different strings with the same source and target. That is, `coherence` can handle goals of the form `a ≫ f ≫ b ≫ g ≫ c = a' ≫ f ≫ b' ≫ g ≫ c'` where `a = a'`, `b = b'`, and `c = c'` can be proved using `coherence1`. ``` This PR additionally provides a "composition up to unitors+associators" operation, so you can write ``` example {U V W X Y : C} (f : U ⟶ V ⊗ (W ⊗ X)) (g : (V ⊗ W) ⊗ X ⟶ Y) : U ⟶ Y := f ⊗≫ g ``` Co-authored-by: Scott Morrison <scott.morrison@gmail.com> Co-authored-by: yuma-mizuno <mizuno.y.aj@gmail.com>

bors · 2022-04-10T12:36:46Z

Build failed (retrying...):

Build mathlib

This is an alternative to #12697 (although this one does not handle bicategories!) From the docstring: ``` Use the coherence theorem for monoidal categories to solve equations in a monoidal equation, where the two sides only differ by replacing strings of "structural" morphisms with different strings with the same source and target. That is, `coherence` can handle goals of the form `a ≫ f ≫ b ≫ g ≫ c = a' ≫ f ≫ b' ≫ g ≫ c'` where `a = a'`, `b = b'`, and `c = c'` can be proved using `coherence1`. ``` This PR additionally provides a "composition up to unitors+associators" operation, so you can write ``` example {U V W X Y : C} (f : U ⟶ V ⊗ (W ⊗ X)) (g : (V ⊗ W) ⊗ X ⟶ Y) : U ⟶ Y := f ⊗≫ g ``` Co-authored-by: Scott Morrison <scott.morrison@gmail.com> Co-authored-by: yuma-mizuno <mizuno.y.aj@gmail.com>

bors · 2022-04-10T16:51:31Z

Build failed (retrying...):

Build mathlib

This is an alternative to #12697 (although this one does not handle bicategories!) From the docstring: ``` Use the coherence theorem for monoidal categories to solve equations in a monoidal equation, where the two sides only differ by replacing strings of "structural" morphisms with different strings with the same source and target. That is, `coherence` can handle goals of the form `a ≫ f ≫ b ≫ g ≫ c = a' ≫ f ≫ b' ≫ g ≫ c'` where `a = a'`, `b = b'`, and `c = c'` can be proved using `coherence1`. ``` This PR additionally provides a "composition up to unitors+associators" operation, so you can write ``` example {U V W X Y : C} (f : U ⟶ V ⊗ (W ⊗ X)) (g : (V ⊗ W) ⊗ X ⟶ Y) : U ⟶ Y := f ⊗≫ g ``` Co-authored-by: Scott Morrison <scott.morrison@gmail.com> Co-authored-by: yuma-mizuno <mizuno.y.aj@gmail.com>

bors · 2022-04-10T17:43:56Z

Build failed (retrying...):

Build mathlib

This is an alternative to #12697 (although this one does not handle bicategories!) From the docstring: ``` Use the coherence theorem for monoidal categories to solve equations in a monoidal equation, where the two sides only differ by replacing strings of "structural" morphisms with different strings with the same source and target. That is, `coherence` can handle goals of the form `a ≫ f ≫ b ≫ g ≫ c = a' ≫ f ≫ b' ≫ g ≫ c'` where `a = a'`, `b = b'`, and `c = c'` can be proved using `coherence1`. ``` This PR additionally provides a "composition up to unitors+associators" operation, so you can write ``` example {U V W X Y : C} (f : U ⟶ V ⊗ (W ⊗ X)) (g : (V ⊗ W) ⊗ X ⟶ Y) : U ⟶ Y := f ⊗≫ g ``` Co-authored-by: Scott Morrison <scott.morrison@gmail.com> Co-authored-by: yuma-mizuno <mizuno.y.aj@gmail.com>

bors · 2022-04-10T20:08:03Z

Pull request successfully merged into master.

Build succeeded:

…or bicategories (#13417) This PR extends the coherence tactic for monoidal categories #13125 to bicategories. The setup is the same as for monoidal case except for the following : we normalize 2-morphisms before running the coherence tactic. This normalization is achieved by the set of simp lemmas in `whisker_simps` defined in `coherence_tactic.lean`. As a test of the tactic in the real world, I have proved several properties of adjunction in bicategories in #13418. Unfortunately some proofs cause timeout, so it seems that we need to speed up the coherence tactic in the future. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

semorrison added 5 commits April 2, 2022 15:51

starting

c42c3a9

feat(category_theory/monoidal): coherence tactic

48b399b

minor

308b5f4

cleanup

3217c62

minor

61b7a3c

semorrison mentioned this pull request Apr 2, 2022

feat(category_theory/monoidal): define a monoidal structure on the tensor product functor of a braided monoidal category #13034

Closed

1 task

semorrison added 2 commits April 2, 2022 20:58

reformulate a proof using the coherence tactic

88475d0

another

4756883

manzyuk reviewed Apr 2, 2022

View reviewed changes

src/category_theory/monoidal/coherence.lean Outdated Show resolved Hide resolved

manzyuk requested a review from yuma-mizuno April 2, 2022 12:49

semorrison and others added 3 commits April 3, 2022 09:16

Update src/category_theory/monoidal/coherence.lean

86cf104

Co-authored-by: Oleksandr Manzyuk <manzyuk@gmail.com>

lint

f336001

Merge branch 'semorrison/coherence' of github.com:leanprover-communit…

7b34723

…y/mathlib into semorrison/coherence

semorrison added the awaiting-review The author would like community review of the PR label Apr 2, 2022

yuma-mizuno reviewed Apr 3, 2022

View reviewed changes

src/category_theory/monoidal/coherence.lean Outdated Show resolved Hide resolved

src/category_theory/monoidal/coherence.lean Outdated Show resolved Hide resolved

src/category_theory/monoidal/coherence.lean Show resolved Hide resolved

yuma-mizuno added awaiting-author A reviewer has asked the author a question or requested changes and removed awaiting-review The author would like community review of the PR labels Apr 3, 2022

suggestion from review

71219bd

semorrison added awaiting-review The author would like community review of the PR and removed awaiting-author A reviewer has asked the author a question or requested changes labels Apr 3, 2022

yuma-mizuno reviewed Apr 3, 2022

View reviewed changes

refactoring suggestions from Yuma

858bc3c

jcommelin reviewed Apr 8, 2022

View reviewed changes

src/category_theory/monoidal/coherence.lean Outdated Show resolved Hide resolved

src/category_theory/monoidal/coherence.lean Outdated Show resolved Hide resolved

Apply suggestions from code review

afffac0

Co-authored-by: Johan Commelin <johan@commelin.net>

github-actions bot added delegated The PR author may merge after reviewing final suggestions. and removed awaiting-review The author would like community review of the PR labels Apr 9, 2022

digama0 added the modifies-tactic-syntax This PR adds a new interactive tactic or modifies the syntax of an existing tactic. label Apr 9, 2022

github-actions bot added the ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) label Apr 10, 2022

bors bot changed the title ~~feat(category_theory/monoidal): coherence tactic~~ [Merged by Bors] - feat(category_theory/monoidal): coherence tactic Apr 10, 2022

bors bot closed this Apr 10, 2022

bors bot deleted the semorrison/coherence branch April 10, 2022 20:08

yuma-mizuno mentioned this pull request Apr 13, 2022

[Merged by Bors] - feat(category_theory/bicategory/coherence_tactic): coherence tactic for bicategories #13417

Closed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - feat(category_theory/monoidal): coherence tactic #13125

[Merged by Bors] - feat(category_theory/monoidal): coherence tactic #13125

semorrison commented Apr 2, 2022 •

edited

Loading

manzyuk commented Apr 2, 2022

semorrison commented Apr 2, 2022

manzyuk commented Apr 2, 2022

yuma-mizuno left a comment

yuma-mizuno left a comment

semorrison commented Apr 3, 2022

yuma-mizuno commented Apr 3, 2022

jcommelin commented Apr 8, 2022

semorrison commented Apr 9, 2022

jcommelin commented Apr 9, 2022

bors bot commented Apr 9, 2022

semorrison commented Apr 10, 2022

bors bot commented Apr 10, 2022

bors bot commented Apr 10, 2022

bors bot commented Apr 10, 2022

bors bot commented Apr 10, 2022

bors bot commented Apr 10, 2022

bors bot commented Apr 10, 2022

[Merged by Bors] - feat(category_theory/monoidal): coherence tactic #13125

[Merged by Bors] - feat(category_theory/monoidal): coherence tactic #13125

Conversation

semorrison commented Apr 2, 2022 • edited Loading

manzyuk commented Apr 2, 2022

semorrison commented Apr 2, 2022

manzyuk commented Apr 2, 2022

yuma-mizuno left a comment

Choose a reason for hiding this comment

yuma-mizuno left a comment

Choose a reason for hiding this comment

semorrison commented Apr 3, 2022

yuma-mizuno commented Apr 3, 2022

jcommelin commented Apr 8, 2022

semorrison commented Apr 9, 2022

jcommelin commented Apr 9, 2022

bors bot commented Apr 9, 2022

semorrison commented Apr 10, 2022

bors bot commented Apr 10, 2022

bors bot commented Apr 10, 2022

bors bot commented Apr 10, 2022

bors bot commented Apr 10, 2022

bors bot commented Apr 10, 2022

bors bot commented Apr 10, 2022

semorrison commented Apr 2, 2022 •

edited

Loading