[Merged by Bors] - feat: port CategoryTheory.Monad.Basic by Parcly-Taxel · Pull Request #2969 · leanprover-community/mathlib4

Parcly-Taxel · 2023-03-18T07:56:47Z

Mathbin -> Mathlib fix certain import statements move "by" to end of line add import to Mathlib.lean

…Basic

Mathlib/CategoryTheory/Monad/Basic.lean

jcommelin · 2023-03-22T14:13:06Z

Mathlib/CategoryTheory/Monad/Basic.lean

+/-- Porting note: removed @[simp] as the linter complains of the LHS being reducible to
+  (comonadToFunctor _).mapIso (Iso.mk (MonadHom.mk f.hom) (MonadHom.mk f.inv))
+  which does not even compile
+-/


That doesn't sound very promising. If you have set_option pp.all true, does it reduce to something that typechecks? Should we have a new simp-lemma for that LHS, so that the total behaviour of the simp-set doesn't change?

OK, consider monadToFunctor_mapIso_monad_iso_mk first. simpNF says the LHS is reducible to

CategoryTheory.Functor.mapIso (CategoryTheory.monadToFunctor C) (CategoryTheory.Iso.mk (CategoryTheory.MonadHom.mk f.hom) (CategoryTheory.MonadHom.mk f.inv))

But when I make a new theorem with this simplification

theorem monadToFunctor_mapIso_monad_iso_mk' {M N : Monad C} (f : (M : C ⥤ C) ≅ N) : CategoryTheory.Functor.mapIso (CategoryTheory.monadToFunctor C) (CategoryTheory.Iso.mk (CategoryTheory.MonadHom.mk f.hom) (CategoryTheory.MonadHom.mk f.inv)) = f := by aesop_cat

it is not the body of the proof that throws an error, but MonadHom.mk f.hom and MonadHom.mk f.inv in the "simplified" LHS itself!

tactic 'aesop' failed, failed to prove the goal after exhaustive search. T: Monad C G: Comonad C MN: Monad C f: M.toFunctor ≅ N.toFunctor ⊢ ∀ (X : C), (Monad.η M).app X ≫ f.hom.app X = (Monad.η N).app X Basic.lean:327:28 tactic 'aesop' failed, failed to prove the goal after exhaustive search. T: Monad C G: Comonad C MN: Monad C f: M.toFunctor ≅ N.toFunctor ⊢ ∀ (X : C), (Monad.μ M).app X ≫ f.hom.app X = (M.toFunctor.map (f.hom.app X) ≫ f.hom.app (N.toFunctor.obj X)) ≫ (Monad.μ N).app X Basic.lean:327:63 tactic 'aesop' failed, failed to prove the goal after exhaustive search. T: Monad C G: Comonad C MN: Monad C f: M.toFunctor ≅ N.toFunctor ⊢ ∀ (X : C), (Monad.η N).app X ≫ f.inv.app X = (Monad.η M).app X Basic.lean:327:63 tactic 'aesop' failed, failed to prove the goal after exhaustive search. T: Monad C G: Comonad C MN: Monad C f: M.toFunctor ≅ N.toFunctor ⊢ ∀ (X : C), (Monad.μ N).app X ≫ f.inv.app X = (N.toFunctor.map (f.inv.app X) ≫ f.inv.app (M.toFunctor.obj X)) ≫ (Monad.μ M).app X

So perhaps aesop is being run when it shouldn't be run.

I suggest you inspect the statement with pp.all enabled. That way you'll have @s all over the place, but it will also make clear what is actually going on.

Yeah, I can't make sense of all this:

tactic 'aesop' failed, failed to prove the goal after exhaustive search. T: @CategoryTheory.Monad.{v₁, u₁} C inst G: @CategoryTheory.Comonad.{v₁, u₁} C inst MN: @CategoryTheory.Monad.{v₁, u₁} C inst f: @CategoryTheory.Iso.{max u₁ v₁, max u₁ v₁} (@CategoryTheory.Functor.{v₁, v₁, u₁, u₁} C inst C inst) (@CategoryTheory.Functor.category.{v₁, v₁, u₁, u₁} C inst C inst) (@CategoryTheory.Monad.toFunctor.{v₁, u₁} C inst M) (@CategoryTheory.Monad.toFunctor.{v₁, u₁} C inst N) ⊢ ∀ (X : C), @Eq.{v₁ + 1} (@Quiver.Hom.{v₁ + 1, u₁} C (@CategoryTheory.CategoryStruct.toQuiver.{v₁, u₁} C (@CategoryTheory.Category.toCategoryStruct.{v₁, u₁} C inst)) (@Prefunctor.obj.{v₁ + 1, v₁ + 1, u₁, u₁} C (@CategoryTheory.CategoryStruct.toQuiver.{v₁, u₁} C (@CategoryTheory.Category.toCategoryStruct.{v₁, u₁} C inst)) C (@CategoryTheory.CategoryStruct.toQuiver.{v₁, u₁} C (@CategoryTheory.Category.toCategoryStruct.{v₁, u₁} C inst)) (@CategoryTheory.Functor.toPrefunctor.{v₁, v₁, u₁, u₁} C inst C inst (@CategoryTheory.Functor.id.{v₁, u₁} C inst)) X) (@Prefunctor.obj.{v₁ + 1, v₁ + 1, u₁, u₁} C (@CategoryTheory.CategoryStruct.toQuiver.{v₁, u₁} C (@CategoryTheory.Category.toCategoryStruct.{v₁, u₁} C inst)) C (@CategoryTheory.CategoryStruct.toQuiver.{v₁, u₁} C (@CategoryTheory.Category.toCategoryStruct.{v₁, u₁} C inst)) (@CategoryTheory.Functor.toPrefunctor.{v₁, v₁, u₁, u₁} C inst C inst (@CategoryTheory.Monad.toFunctor.{v₁, u₁} C inst N)) X)) (@CategoryTheory.CategoryStruct.comp.{v₁, u₁} C (@CategoryTheory.Category.toCategoryStruct.{v₁, u₁} C inst) (@Prefunctor.obj.{v₁ + 1, v₁ + 1, u₁, u₁} C (@CategoryTheory.CategoryStruct.toQuiver.{v₁, u₁} C (@CategoryTheory.Category.toCategoryStruct.{v₁, u₁} C inst)) C (@CategoryTheory.CategoryStruct.toQuiver.{v₁, u₁} C (@CategoryTheory.Category.toCategoryStruct.{v₁, u₁} C inst)) (@CategoryTheory.Functor.toPrefunctor.{v₁, v₁, u₁, u₁} C inst C inst (@CategoryTheory.Functor.id.{v₁, u₁} C inst)) X) (@Prefunctor.obj.{v₁ + 1, v₁ + 1, u₁, u₁} C (@CategoryTheory.CategoryStruct.toQuiver.{v₁, u₁} C (@CategoryTheory.Category.toCategoryStruct.{v₁, u₁} C inst)) C (@CategoryTheory.CategoryStruct.toQuiver.{v₁, u₁} C (@CategoryTheory.Category.toCategoryStruct.{v₁, u₁} C inst)) (@CategoryTheory.Functor.toPrefunctor.{v₁, v₁, u₁, u₁} C inst C inst (@CategoryTheory.Monad.toFunctor.{v₁, u₁} C inst M)) X) (@Prefunctor.obj.{v₁ + 1, v₁ + 1, u₁, u₁} C (@CategoryTheory.CategoryStruct.toQuiver.{v₁, u₁} C (@CategoryTheory.Category.toCategoryStruct.{v₁, u₁} C inst)) C (@CategoryTheory.CategoryStruct.toQuiver.{v₁, u₁} C (@CategoryTheory.Category.toCategoryStruct.{v₁, u₁} C inst)) (@CategoryTheory.Functor.toPrefunctor.{v₁, v₁, u₁, u₁} C inst C inst (@CategoryTheory.Monad.toFunctor.{v₁, u₁} C inst N)) X) (@CategoryTheory.NatTrans.app.{v₁, v₁, u₁, u₁} C inst C inst (@CategoryTheory.Functor.id.{v₁, u₁} C inst) (@CategoryTheory.Monad.toFunctor.{v₁, u₁} C inst M) (@CategoryTheory.Monad.η.{v₁, u₁} C inst M) X) (@CategoryTheory.NatTrans.app.{v₁, v₁, u₁, u₁} C inst C inst (@CategoryTheory.Monad.toFunctor.{v₁, u₁} C inst M) (@CategoryTheory.Monad.toFunctor.{v₁, u₁} C inst N) (@CategoryTheory.Iso.hom.{max u₁ v₁, max u₁ v₁} (@CategoryTheory.Functor.{v₁, v₁, u₁, u₁} C inst C inst) (@CategoryTheory.Functor.category.{v₁, v₁, u₁, u₁} C inst C inst) (@CategoryTheory.Monad.toFunctor.{v₁, u₁} C inst M) (@CategoryTheory.Monad.toFunctor.{v₁, u₁} C inst N) f) X)) (@CategoryTheory.NatTrans.app.{v₁, v₁, u₁, u₁} C inst C inst (@CategoryTheory.Functor.id.{v₁, u₁} C inst) (@CategoryTheory.Monad.toFunctor.{v₁, u₁} C inst N) (@CategoryTheory.Monad.η.{v₁, u₁} C inst N) X)

@jcommelin I've found that exactly four extra arguments – no more, no less – are needed for monadToFunctor_mapIso_monad_iso_mk' to type-check and from there compile:

@[simp] theorem monadToFunctor_mapIso_monad_iso_mk' {M N : Monad C} (f : (M : C ⥤ C) ≅ N) (f_η : ∀ (X : C), M.η.app X ≫ f.hom.app X = N.η.app X) (f_μ : ∀ (X : C), M.μ.app X ≫ f.hom.app X = (M.map (f.hom.app X) ≫ f.hom.app (N.obj X)) ≫ N.μ.app X) (f_η' : ∀ (X : C), N.η.app X ≫ f.inv.app X = M.η.app X) (f_μ' : ∀ (X : C), N.μ.app X ≫ f.inv.app X = (N.map (f.inv.app X) ≫ f.inv.app (M.obj X)) ≫ M.μ.app X): (monadToFunctor C).mapIso (Iso.mk (MonadHom.mk f.hom) (MonadHom.mk f.inv)) = f := by aesop_cat

But f_η' and f_μ' are not in the original theorem and I get a new simpNF error:

#check CategoryTheory.monadToFunctor_mapIso_monad_iso_mk' /- Left-hand side does not simplify, when using the simp lemma on itself. This usually means that it will never apply.

What do I do now?

Hmm, thanks for debugging. It's really quite annoying that this new statement is now also flagged by the simp linter. I had expected that it would be a good simp lemma.
Please report in the porting note that you made this attempt, but that the simp linter was still not satisfied.

ChrisHughes24 · 2023-03-24T13:43:32Z

bors merge

Co-authored-by: Parcly Taxel <reddeloostw@gmail.com> Co-authored-by: Joël Riou <joel.riou@universite-paris-saclay.fr>

bors · 2023-03-24T15:21:48Z

Pull request successfully merged into master.

Build succeeded:

Build
Lint style

This is a backport from mathlib4, where the simpNF (correctly) linter disapproves of these lemmas. Mostly this PR exists to verify that these are not needed in the simp set. leanprover-community/mathlib4#2969 Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

The [porting PR](#2969) removed two `@[simp]` that the simpNF linter complained about. Now that I've verified they are not actually needed downstream (see leanprover-community/mathlib3#18727), we may as well remove the comments. Co-authored-by: Scott Morrison <scott.morrison@gmail.com> Co-authored-by: Chris Hughes <chrishughes24@gmail.com>

This fixes a regression of `@[simps]` to `@[simp]` from #2969, per [zulip](https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/!4.232969.20simps.20bug.3F.20.28Monad.2EBasic.29). There are a few incidental changes to `@[simps]` arguments in this PR, just removing arguments that had no effect on behaviour. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

This is a backport from mathlib4, where the simpNF (correctly) linter disapproves of these lemmas. Mostly this PR exists to verify that these are not needed in the simp set. leanprover-community/mathlib4#2969 Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

This fixes a regression of `@[simps]` to `@[simp]` from #2969, per [zulip](https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/!4.232969.20simps.20bug.3F.20.28Monad.2EBasic.29). There are a few incidental changes to `@[simps]` arguments in this PR, just removing arguments that had no effect on behaviour. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

Parcly-Taxel added 4 commits March 18, 2023 01:59

feat: port CategoryTheory.Monad.Basic

22cb612

Initial file copy from mathport

c261525

automated fixes

ee7dcb6

Mathbin -> Mathlib fix certain import statements move "by" to end of line add import to Mathlib.lean

Fix most errors

2b3d110

Parcly-Taxel added help-wanted The author needs attention to resolve issues WIP Work in progress mathlib-port This is a port of a theory file from mathlib. labels Mar 18, 2023

various fixes

73a87a1

Parcly-Taxel added awaiting-review and removed help-wanted The author needs attention to resolve issues WIP Work in progress labels Mar 19, 2023

Merge remote-tracking branch 'origin' into port/CategoryTheory.Monad.…

966103e

…Basic

jcommelin reviewed Mar 21, 2023

View reviewed changes

Mathlib/CategoryTheory/Monad/Basic.lean Outdated Show resolved Hide resolved

Parcly-Taxel added 2 commits March 21, 2023 21:34

More detailed porting notes

dc01e1f

oops

c2b5fc5

jcommelin reviewed Mar 22, 2023

View reviewed changes

Parcly-Taxel added 3 commits March 22, 2023 22:36

Merge branch 'master' into port/CategoryTheory.Monad.Basic

d12b497

Merge branch 'master' into port/CategoryTheory.Monad.Basic

6b257da

Add porting notes about failing to please simpNF

89e10c4

github-actions bot added ready-to-merge This PR has been sent to bors. and removed awaiting-review labels Mar 24, 2023

bors bot pushed a commit that referenced this pull request Mar 24, 2023

feat: port CategoryTheory.Monad.Basic (#2969)

951fdcf

Co-authored-by: Parcly Taxel <reddeloostw@gmail.com> Co-authored-by: Joël Riou <joel.riou@universite-paris-saclay.fr>

bors bot changed the title ~~feat: port CategoryTheory.Monad.Basic~~ [Merged by Bors] - feat: port CategoryTheory.Monad.Basic Mar 24, 2023

bors bot closed this Mar 24, 2023

bors bot deleted the port/CategoryTheory.Monad.Basic branch March 24, 2023 15:22

Parcly-Taxel mentioned this pull request Mar 31, 2023

[Merged by Bors] - feat: port CategoryTheory.Grothendieck #3204

Closed

This was referenced Apr 4, 2023

[Merged by Bors] - chore(category_theory/monad/basic): remove some simp lemmas leanprover-community/mathlib3#18727

Closed

[Merged by Bors] - chore: CategoryTheory/Monad/Basic cleanup #3253

Closed

kim-em mentioned this pull request Apr 4, 2023

[Merged by Bors] - chore: fix simps projections in CategoryTheory.Monad.Basic #3269

Closed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - feat: port CategoryTheory.Monad.Basic#2969

[Merged by Bors] - feat: port CategoryTheory.Monad.Basic#2969
Parcly-Taxel wants to merge 11 commits intomasterfrom
port/CategoryTheory.Monad.Basic

Parcly-Taxel commented Mar 18, 2023

Uh oh!

Uh oh!

jcommelin Mar 22, 2023

Uh oh!

Parcly-Taxel Mar 22, 2023 •

edited

Loading

Uh oh!

jcommelin Mar 23, 2023

Uh oh!

Parcly-Taxel Mar 23, 2023

Uh oh!

Parcly-Taxel Mar 23, 2023

Uh oh!

jcommelin Mar 23, 2023

Uh oh!

Parcly-Taxel Mar 23, 2023

Uh oh!

ChrisHughes24 commented Mar 24, 2023

Uh oh!

bors bot commented Mar 24, 2023

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

Conversation

Parcly-Taxel commented Mar 18, 2023

Uh oh!

Uh oh!

jcommelin Mar 22, 2023

Choose a reason for hiding this comment

Uh oh!

Parcly-Taxel Mar 22, 2023 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

jcommelin Mar 23, 2023

Choose a reason for hiding this comment

Uh oh!

Parcly-Taxel Mar 23, 2023

Choose a reason for hiding this comment

Uh oh!

Parcly-Taxel Mar 23, 2023

Choose a reason for hiding this comment

Uh oh!

jcommelin Mar 23, 2023

Choose a reason for hiding this comment

Uh oh!

Parcly-Taxel Mar 23, 2023

Choose a reason for hiding this comment

Uh oh!

ChrisHughes24 commented Mar 24, 2023

Uh oh!

bors bot commented Mar 24, 2023

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

Parcly-Taxel Mar 22, 2023 •

edited

Loading