Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

[Merged by Bors] - feat: port CategoryTheory.Elementwise #2872

Closed
wants to merge 9 commits into from
Closed

[Merged by Bors] - feat: port CategoryTheory.Elementwise #2872

wants to merge 9 commits into from

Conversation

javra
Copy link
Collaborator

@javra javra commented Mar 14, 2023 •
edited by github-actions bot

@javra
feat: port CategoryTheory.Elementwise
12c8fb9
@javra
Initial file copy from mathport
3e585fd
@javra
automated fixes
c7d603c 
Mathbin -> Mathlib

fix certain import statements

move "by" to end of line

add import to Mathlib.lean
@javra javra added WIP Work in progress mathlib-port This is a port of a theory file from mathlib. labels Mar 14, 2023
@semorrison semorrison added the blocked-by-other-PR This PR depends on another PR which is still in the queue. label Mar 14, 2023
kmill
kmill reviewed Mar 14, 2023
View reviewed changes
Mathlib/CategoryTheory/Elementwise.lean Outdated
open CategoryTheory

-- This list is incomplete, and it would probably be useful to add more.
attribute [elementwise] iso.hom_inv_id iso.inv_hom_id is_iso.hom_inv_id is_iso.inv_hom_id
Copy link
Contributor

@kmill kmill Mar 14, 2023 •
edited

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I'm expecting that this line will be

set_option linter.existingAttributeWarning false in
attribute [elementwise] Iso.hom_inv_id Iso.inv_hom_id IsIso.hom_inv_id IsIso.inv_hom_id

There's a problem with the linter here though where the set_option line seems not to be turning it off, but that should all be sorted out by the time that the @[elementwise] attribute is merged.

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Hm, I did a workaround by first removing simp and then re-add it using elementwise (attr := simp), which then adds all the correct simp lemmas.

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Okay, fixed the linter option instead

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

@fpvandoorn I know we talked about how you might fix the linter option or re-implement the attribute handling for elementwise/reassoc, so here's a ping since @javra modified ToAdditive

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

applyAttributes should probably be moved out of Mathlib.Tactic.ToAdditive, if it's used elsewhere

Copy link
Contributor

@kmill kmill Mar 16, 2023 •
edited

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Floris was explaining to me that elementwise/reassoc shouldn't be using applyAttributes, since it does some very ToAdditive-specific things (including sometimes applying to_additive!).

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Ah, makes sense, my changes to applyAttributes are probably still reasonable

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Yes, this change is still sensible. Note there will be a small conflict with #2908

@semorrison semorrison removed the blocked-by-other-PR This PR depends on another PR which is still in the queue. label Mar 16, 2023
@semorrison
Copy link
Contributor

This PR/issue depends on:

@semorrison semorrison added the merge-conflict The PR has a merge conflict with master, and needs manual merging. label Mar 16, 2023
@semorrison semorrison removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. label Mar 16, 2023
@javra javra added awaiting-review The author would like community review of the PR and removed WIP Work in progress labels Mar 16, 2023
@ChrisHughes24
Copy link
Member

bors r+

@github-actions github-actions bot added ready-to-merge This PR has been sent to bors. and removed awaiting-review The author would like community review of the PR labels Mar 17, 2023
bors bot pushed a commit that referenced this pull request Mar 17, 2023
@javra
feat: port CategoryTheory.Elementwise (#2872)
92978c2
@bors
Copy link

bors bot commented Mar 17, 2023

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat: port CategoryTheory.Elementwise [Merged by Bors] - feat: port CategoryTheory.Elementwise Mar 17, 2023
@bors bors bot closed this Mar 17, 2023
@bors bors bot deleted the port/CategoryTheory.Elementwise branch March 17, 2023 14:05
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@kmill kmill kmill left review comments

@fpvandoorn fpvandoorn fpvandoorn left review comments

Assignees
No one assigned
Labels
mathlib-port This is a port of a theory file from mathlib. ready-to-merge This PR has been sent to bors.
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
5 participants
@javra @semorrison @ChrisHughes24 @kmill @fpvandoorn