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 Algebra.Group.WithOne.Defs #841

Closed
wants to merge 10 commits into from
Closed

[Merged by Bors] - feat: port Algebra.Group.WithOne.Defs #841

wants to merge 10 commits into from

Conversation

kbuzzard
Copy link
Member

@kbuzzard kbuzzard commented Dec 3, 2022

mathlib3 commit hash e574b1a4e891376b0ef974b926da39e05da12a06

@kbuzzard kbuzzard added the WIP Work in progress label Dec 3, 2022
@kbuzzard kbuzzard mentioned this pull request Dec 3, 2022
Closed
2 tasks
@kbuzzard
Copy link
Member Author

kbuzzard commented Dec 3, 2022

Things of note here:

  1. Like WithBot, we add coe : α → WithOne α and tag it @[coe] for compatibility with Lean 4's coercion mechanism
  2. Neither @[coe, to_additive] nor @[to_additive, coe] seems to tag the additivised definition with coe; same for @[norm_cast, to_additive] (which used to work in Lean 3). I've had to manually tag some to-additivised declarations as a consequence.
  3. I had to comment out a CanLift instance, and also rewrite a proof, because there is still no lift tactic.
  4. There are some shows which might not be needed; I asked at https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/_proof_1/near/313734606 because I don't know how to test this.
  5. WithZero.zero_mul with WithZero.mul_zero used to be tagged @[simp] but a linter told me that simp only [zero_mul] proves it, so I removed the tags. This makes sense: WithZero alpha is an instance of MulZeroClass. I'm slightly surprised that the linter in mathlib3 doesn't flag this.

@kbuzzard kbuzzard added awaiting-review The author would like community review of the PR mathlib-port This is a port of a theory file from mathlib. and removed WIP Work in progress labels Dec 3, 2022
@kbuzzard kbuzzard changed the title feat: port Algebra.Group/WithOne.Defs feat: port Algebra.Group.WithOne.Defs Dec 3, 2022
semorrison
semorrison reviewed Dec 4, 2022
View reviewed changes
Mathlib/Algebra/Group/WithOne/Defs.lean Outdated
Comment on lines 177 to 180
-- example [Semigroup α] :
-- @Monoid.toMulOneClass _ (@instMonoidWithOne α _) = @instMulOneClassWithOne α _ :=
-- rfl

Copy link
Contributor

Choose a reason for hiding this comment

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

Delete?

Copy link
Member Author

Choose a reason for hiding this comment

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

I'd have to make a corresponding PR to mathlib3 then, right? https://github.com/leanprover-community/mathlib/blob/c982179ec21091d3e102d8a5d9f5fe06c8fafb73/src/algebra/group/with_one/defs.lean#L127-L128

@semorrison
Copy link
Contributor

If you can remember it, could you add a porting note to the proof you had to rewrite for lack of simp? It would be good, even if only as a test, to restore this when lift arrives, hopefully soon.

@semorrison
Copy link
Contributor

bors d+

Please update the wiki page when you merge.

@bors
Copy link

bors bot commented Dec 4, 2022

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

@github-actions github-actions bot added delegated and removed awaiting-review The author would like community review of the PR labels Dec 4, 2022
Ruben-VandeVelde
Ruben-VandeVelde reviewed Dec 4, 2022
View reviewed changes
Mathlib/Algebra/Group/WithOne/Defs.lean Outdated
Comment on lines 121 to 125
-- porting note: in Lean 4 this is a syntactic tautology
-- @[to_additive]
-- theorem some_eq_coe {a : α} : (some a : WithOne α) = ↑a :=
-- rfl
-- #align with_one.some_eq_coe WithOne.some_eq_coe
Copy link
Collaborator

Choose a reason for hiding this comment

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

Suggested change
-- porting note: in Lean 4 this is a syntactic tautology
-- @[to_additive]
-- theorem some_eq_coe {a : α} : (some a : WithOne α) = ↑a :=
-- rfl
-- #align with_one.some_eq_coe WithOne.some_eq_coe
#noalign with_one.some_eq_coe

Copy link
Member Author

Choose a reason for hiding this comment

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

And with_zero.some_eq_coe too!

Mathlib/Algebra/Group/WithOne/Defs.lean Outdated Show resolved Hide resolved
@zeramorphic zeramorphic mentioned this pull request Dec 4, 2022
Closed
2 tasks
@Ruben-VandeVelde Ruben-VandeVelde mentioned this pull request Dec 4, 2022
Closed
1 task
@kbuzzard
Copy link
Member Author

kbuzzard commented Dec 4, 2022

OK I just realised that every @[to_additive] followed by an #align needs to have a second #align added for the additivised definition. I've just added these but don't want to hit merge until the branch compiles and unfortunately it's time for bed.

@kbuzzard
Copy link
Member Author

kbuzzard commented Dec 5, 2022

Oh nice, it doesn't take hours to compile like mathlib3 :-)

@kbuzzard
Copy link
Member Author

kbuzzard commented Dec 5, 2022

bors r+

@github-actions github-actions bot mentioned this pull request Dec 5, 2022
Closed
@ChrisHughes24 ChrisHughes24 added the ready-to-merge This PR has been sent to bors. label Dec 5, 2022
@github-actions github-actions bot mentioned this pull request Dec 6, 2022
Open
@semorrison
Copy link
Contributor

bors merge

bors bot pushed a commit that referenced this pull request Dec 6, 2022
@kbuzzard
feat: port Algebra.Group.WithOne.Defs (#841)
5d30318 
mathlib3 commit hash e574b1a4e891376b0ef974b926da39e05da12a06
@bors
Copy link

bors bot commented Dec 6, 2022

Build failed (retrying...):

bors bot pushed a commit that referenced this pull request Dec 6, 2022
@kbuzzard
feat: port Algebra.Group.WithOne.Defs (#841)
3abe590 
mathlib3 commit hash e574b1a4e891376b0ef974b926da39e05da12a06
@bors
Copy link

bors bot commented Dec 6, 2022

Build failed (retrying...):

  • Build

bors bot pushed a commit that referenced this pull request Dec 6, 2022
@kbuzzard
feat: port Algebra.Group.WithOne.Defs (#841)
7aa1fc1 
mathlib3 commit hash e574b1a4e891376b0ef974b926da39e05da12a06
@bors
Copy link

bors bot commented Dec 6, 2022

Build failed:

@semorrison
Copy link
Contributor

bors merge

bors bot pushed a commit that referenced this pull request Dec 6, 2022
@kbuzzard @semorrison
feat: port Algebra.Group.WithOne.Defs (#841)
8a3baed 
mathlib3 commit hash e574b1a4e891376b0ef974b926da39e05da12a06

Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Co-authored-by: Scott Morrison <scott@tqft.net>
@bors
Copy link

bors bot commented Dec 6, 2022

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat: port Algebra.Group.WithOne.Defs [Merged by Bors] - feat: port Algebra.Group.WithOne.Defs Dec 6, 2022
@bors bors bot closed this Dec 6, 2022
@bors bors bot deleted the kbuzzard-port-algebra-group-with-one-defs branch December 6, 2022 04:00
bors bot pushed a commit to leanprover-community/mathlib that referenced this pull request Dec 6, 2022
@leanprover-community-bot @jcommelin
chore(*): add mathlib4 synchronization comments (#17806)
8770c84 
Regenerated from the [port status wiki page](https://github.com/leanprover-community/mathlib/wiki/mathlib4-port-status).
Relates to the following PRs:
* `algebra.divisibility.basic`: leanprover-community/mathlib4#833
* `algebra.group.with_one.defs`: leanprover-community/mathlib4#841
* `algebra.hom.commute`: leanprover-community/mathlib4#831
* `algebra.hom.group`: leanprover-community/mathlib4#659
* `algebra.hom.units`: leanprover-community/mathlib4#745
* `algebra.ring.basic`: leanprover-community/mathlib4#830
* `category_theory.natural_isomorphism`: leanprover-community/mathlib4#820
* `combinatorics.quiver.connected_component`: leanprover-community/mathlib4#836
* `combinatorics.quiver.subquiver`: leanprover-community/mathlib4#828



Co-authored-by: Johan Commelin <johan@commelin.net>
bors bot pushed a commit that referenced this pull request Dec 6, 2022
@kbuzzard @zeramorphic @semorrison
feat: port Algebra.Order.Monoid.WithZero (#851)
92593ea 
mathlib3 SHA: dad7ecf9a1feae63e6e49f07619b7087403fb8d4

Ports Algebra.Order.Monoid.WithZero.[Defs, Basic].

- [x] depends on #841
- [x] depends on leanprover-community/mathlib#17820

I'm planning to wait until leanprover-community/mathlib#17820 is approved before doing a final refactor to move lemmas where they're needed.

Co-authored-by: thirdsgames <thirdsgames2018@gmail.com>
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Co-authored-by: zeramorphic <zeramorphic@proton.me>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@semorrison semorrison semorrison left review comments

@Ruben-VandeVelde Ruben-VandeVelde Ruben-VandeVelde left review comments

Assignees
No one assigned
Labels
delegated 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
4 participants
@kbuzzard @semorrison @Ruben-VandeVelde @ChrisHughes24