Skip to content

[Merged by Bors] - Refactor: use Option.map₂#1439

Closed
urkud wants to merge 6 commits intomasterfrom
YK-map2
Closed

[Merged by Bors] - Refactor: use Option.map₂#1439
urkud wants to merge 6 commits intomasterfrom
YK-map2

Conversation

@urkud
Copy link
Copy Markdown
Member

@urkud urkud commented Jan 9, 2023

This is a forward-port of leanprover-community/mathlib3#18081

@urkud urkud added awaiting-review mathlib3-pair This PR is a forward-port of a mathlib3 PR or part of one, either under review or recently merged labels Jan 9, 2023
@urkud urkud mentioned this pull request Jan 9, 2023
Closed
bors bot pushed a commit to leanprover-community/mathlib3 that referenced this pull request Jan 13, 2023
@urkud @eric-wieser @YaelDillies
refactor(*): use option.map₂ (#18081)
0fcd8a9 
Relevant parts are forward-ported as leanprover-community/mathlib4#1439



Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
bors bot pushed a commit to leanprover-community/mathlib3 that referenced this pull request Jan 13, 2023
@urkud @eric-wieser @YaelDillies
refactor(*): use option.map₂ (#18081)
be1712d 
Relevant parts are forward-ported as leanprover-community/mathlib4#1439



Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
bors bot pushed a commit to leanprover-community/mathlib3 that referenced this pull request Jan 13, 2023
@urkud @eric-wieser @YaelDillies
refactor(*): use option.map₂ (#18081)
53c1d99 
Relevant parts are forward-ported as leanprover-community/mathlib4#1439



Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
bors bot pushed a commit to leanprover-community/mathlib3 that referenced this pull request Jan 14, 2023
@urkud @eric-wieser @YaelDillies
refactor(*): use option.map₂ (#18081)
9f9d834 
Relevant parts are forward-ported as leanprover-community/mathlib4#1439



Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
bors bot pushed a commit to leanprover-community/mathlib3 that referenced this pull request Jan 14, 2023
@urkud @eric-wieser @YaelDillies
refactor(*): use option.map₂ (#18081)
67efc6b 
Relevant parts are forward-ported as leanprover-community/mathlib4#1439



Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
bors bot pushed a commit to leanprover-community/mathlib3 that referenced this pull request Jan 14, 2023
@urkud @eric-wieser @YaelDillies
refactor(*): use option.map₂ (#18081)
995b47e 
Relevant parts are forward-ported as leanprover-community/mathlib4#1439



Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
@kbuzzard
Copy link
Copy Markdown
Member

kbuzzard commented Jan 16, 2023 •
edited
Loading

In Mathlib/Algebra/Group/WithOne/Defs.lean, the shows can be removed in WithOne.mulOneClass (in your PR you change them to ids -- in mathlib4 they can be removed completely).

instance mulOneClass [Mul α] : MulOneClass (WithOne α) where
  mul := (· * ·)
  one := 1
  one_mul := (Option.liftOrGet_isLeftId _).1
  mul_one := (Option.liftOrGet_isRightId _).1

This also works:

instance noZeroDivisors [Mul α] : NoZeroDivisors (WithZero α) :=
  ⟨Option.map₂_eq_none_iff.1⟩

I mention these because they were changed in the mathlib3 PR but not the mathlib4 PR. Note that they're only proofs, but I think that in each case what I'm suggesting is better than what we have.

@kbuzzard
Copy link
Copy Markdown
Member

kbuzzard commented Jan 16, 2023

Algebra.Order.Ring.WithTop: in mathlib3 you removed the analogue of

instance noZeroDivisors [MulZeroClass α] [NoZeroDivisors α] : NoZeroDivisors (WithTop α) :=

(it's on line 154) and it should be removed here too I guess.

kbuzzard
kbuzzard reviewed Jan 16, 2023
View reviewed changes
Copy link
Copy Markdown
Member

@kbuzzard kbuzzard left a comment •
edited
Loading

Choose a reason for hiding this comment

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

I've ploughed through this to check that the PRs do coincide. I left two comments (above) about when they didn't. Modulo these I approve!

@kbuzzard kbuzzard added awaiting-author A reviewer has asked the author a question or requested changes. and removed awaiting-review labels Jan 19, 2023
@urkud
Copy link
Copy Markdown
Member Author

urkud commented Jan 20, 2023

@kbuzzard Thanks a lot for the review!

@urkud urkud added awaiting-review and removed awaiting-author A reviewer has asked the author a question or requested changes. labels Jan 20, 2023
@kim-em kim-em added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jan 24, 2023
@fpvandoorn
Copy link
Copy Markdown
Member

fpvandoorn commented Jan 25, 2023

Please merge master and double check that no new files of your PR have been ported.

bors d+

@bors
Copy link
Copy Markdown

bors bot commented Jan 25, 2023

✌️ urkud 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 This pull request has been delegated to the PR author (or occasionally another non-maintainer). and removed awaiting-review labels Jan 25, 2023
@urkud urkud removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jan 25, 2023
@urkud
Copy link
Copy Markdown
Member Author

urkud commented Jan 25, 2023

bors merge

@github-actions github-actions bot added the ready-to-merge This PR has been sent to bors. label Jan 25, 2023
bors bot pushed a commit that referenced this pull request Jan 25, 2023
@urkud
Refactor: use Option.map₂ (#1439)
da1e654 
This is a forward-port of leanprover-community/mathlib3#18081
@bors
Copy link
Copy Markdown

bors bot commented Jan 25, 2023

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title Refactor: use Option.map₂ [Merged by Bors] - Refactor: use Option.map₂ Jan 25, 2023
@bors bors bot closed this Jan 25, 2023
@bors bors bot deleted the YK-map2 branch January 25, 2023 20:51
@eric-wieser eric-wieser mentioned this pull request Feb 13, 2023
Closed
bors bot pushed a commit that referenced this pull request Feb 22, 2023
@joneugster @eric-wieser
chore: update SHA of already forward-ported files (#2181)
88c789e 
Update some SHAs of files that changed in mathlib3.

These 17 files need mainly only updated SHA as they've been only touched by backports or already have been forward-ported.

The relevant changes are:

* [Algebra.Group.Defs (#17884)](https://leanprover-community.github.io/mathlib-port-status/file/algebra/group/defs?range=41cf0cc2f528dd40a8f2db167ea4fb37b8fde7f3..2e0975f6a25dd3fbfb9e41556a77f075f6269748)
  * #945
* [Algebra.Group.WithOne.Defs (#18081)](https://leanprover-community.github.io/mathlib-port-status/file/algebra/group/with_one/defs?range=e574b1a4e891376b0ef974b926da39e05da12a06..995b47e555f1b6297c7cf16855f1023e355219fb)
  * #1439
* [Algebra.Module.Submodule.Basic (#18291) : backport](https://leanprover-community.github.io/mathlib-port-status/file/algebra/module/submodule/basic?range=f7fc89d5d5ff1db2d1242c7bb0e9062ce47ef47c..feb99064803fd3108e37c18b0f77d0a8344677a3)
* [Algebra.Order.Monoid.WithTop (#18149, #18081)](https://leanprover-community.github.io/mathlib-port-status/file/algebra/order/monoid/with_top?range=2258b40dacd2942571c8ce136215350c702dc78f..e7e2ba8aa216a5833b5ed85a93317263711a36b5)
  * #1508
  * #1439
* [Algebra.Order.Ring.WithTop (#18149, #18081)](https://leanprover-community.github.io/mathlib-port-status/file/algebra/order/ring/with_top?range=550b58538991c8977703fdeb7c9d51a5aa27df11..e7e2ba8aa216a5833b5ed85a93317263711a36b5)
  * #1508
  * #1439
* [Data.Finset.NAry (#18081)](https://leanprover-community.github.io/mathlib-port-status/file/data/finset/n_ary?range=9003f28797c0664a49e4179487267c494477d853..995b47e555f1b6297c7cf16855f1023e355219fb)
  * #1439
* [Data.Option.NAry (#18081)](https://leanprover-community.github.io/mathlib-port-status/file/data/option/n_ary?range=2258b40dacd2942571c8ce136215350c702dc78f..995b47e555f1b6297c7cf16855f1023e355219fb)
  * #1439
* [Data.Set.NAry (#18081)](https://leanprover-community.github.io/mathlib-port-status/file/data/set/n_ary?range=2ed7e4aec72395b6a7c3ac4ac7873a7a43ead17c..995b47e555f1b6297c7cf16855f1023e355219fb)
  * #1439
* [Data.SetLike.Basic (#18291) : backport](https://leanprover-community.github.io/mathlib-port-status/file/data/set_like/basic?range=fc2ed6f838ce7c9b7c7171e58d78eaf7b438fb0e..feb99064803fd3108e37c18b0f77d0a8344677a3)
* [Data.Sum.Basic (#18184)](https://leanprover-community.github.io/mathlib-port-status/file/data/sum/basic?range=d6aae1bcbd04b8de2022b9b83a5b5b10e10c777d..f4ecb599422baaf39055d8278c7d9ef3b5b72b88)
  * #1583
* [GroupTheory.GroupAction.SubMulAction  (#18291) : backport](https://leanprover-community.github.io/mathlib-port-status/file/group_theory/group_action/sub_mul_action?range=f93c11933efbc3c2f0299e47b8ff83e9b539cbf6..feb99064803fd3108e37c18b0f77d0a8344677a3)
* [GroupTheory.Submonoid.Basic (#18291) : backport](https://leanprover-community.github.io/mathlib-port-status/file/group_theory/submonoid/basic?range=207cfac9fcd06138865b5d04f7091e46d9320432..feb99064803fd3108e37c18b0f77d0a8344677a3)
* [ Logic.Basic (#18291): backport](https://leanprover-community.github.io/mathlib-port-status/file/logic/basic?range=1c521b4fb909320eca16b2bb6f8b5b0490b1cb5e..feb99064803fd3108e37c18b0f77d0a8344677a3)
  * #1509
* [Order.InitialSeg (#18198): backport](https://leanprover-community.github.io/mathlib-port-status/file/order/initial_seg?range=ee0c179cd3c8a45aa5bffbf1b41d8dbede452865..7c3269ca3fa4c0c19e4d127cd7151edbdbf99ed4)
* [Order.RelClasses (#17957)](https://leanprover-community.github.io/mathlib-port-status/file/order/rel_classes?range=c4658a649d216f57e99621708b09dcb3dcccbd23..bc7d81beddb3d6c66f71449c5bc76c38cb77cf9e)
  * #1047
* [Order.WithBot (#18081)](https://leanprover-community.github.io/mathlib-port-status/file/order/with_bot?range=70d50ecfd4900dd6d328da39ab7ebd516abe4025..995b47e555f1b6297c7cf16855f1023e355219fb)
  * #1439
* [RingTheory.Subsemiring.Basic (#18291) : backport](https://leanprover-community.github.io/mathlib-port-status/file/ring_theory/subsemiring/basic?range=f93c11933efbc3c2f0299e47b8ff83e9b539cbf6..feb99064803fd3108e37c18b0f77d0a8344677a3)



Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@kbuzzard kbuzzard kbuzzard left review comments

Assignees

No one assigned

Labels

delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). mathlib3-pair This PR is a forward-port of a mathlib3 PR or part of one, either under review or recently merged 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.

4 participants

@urkud @kbuzzard @fpvandoorn @kim-em