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] - chore(Algebra/Order/Group): change simp lemmas #7867

Closed
wants to merge 10 commits into from
Closed

[Merged by Bors] - chore(Algebra/Order/Group): change simp lemmas #7867

wants to merge 10 commits into from

Conversation

negiizhao
Copy link
Collaborator

Open in Gitpod

@negiizhao negiizhao added awaiting-review The author would like community review of the PR awaiting-CI t-algebra Algebra (groups, rings, fields etc) t-order Order hierarchy and removed awaiting-review The author would like community review of the PR labels Oct 23, 2023
@negiizhao negiizhao changed the title chore: change simp lemmas chore(Algebra/Order/Group): change simp lemmas Oct 23, 2023
@negiizhao
Copy link
Collaborator Author

!bench

@leanprover-bot
Copy link
Collaborator

Here are the benchmark results for commit c95afd7.
The entire run failed.
Found no significant differences.

@negiizhao
Copy link
Collaborator Author

!bench

@leanprover-bot
Copy link
Collaborator

Here are the benchmark results for commit 01e08d8.
There were significant changes against commit e4247f2:

  Benchmark                                                  Metric         Change
  ================================================================================
+ ~Mathlib.RepresentationTheory.GroupCohomology.Resolution   instructions    -1.4%

@negiizhao negiizhao added the awaiting-review The author would like community review of the PR label Oct 23, 2023
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. label Oct 30, 2023
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. label Nov 15, 2023
j-loreaux
j-loreaux reviewed Dec 4, 2023
View reviewed changes
Mathlib/Algebra/Order/Sub/Defs.lean
@[simp]
theorem tsub_le_iff_right : a - b ≤ c ↔ a ≤ c + b :=
theorem tsub_le_iff_right [LE α] [Add α] [Sub α] [OrderedSub α] {a b c : α} :
Copy link
Collaborator

Choose a reason for hiding this comment

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

Is there any actual reason to use [LE α] here instead of [Preorder α]? This seems like needless generalization. (I know it means we don't need the extra conditions, but I'm just wondering if we ever have an OrderedSub instance where we don't have a Preorder instance. It seems rather unlikely.

Copy link
Collaborator Author

@negiizhao negiizhao Dec 16, 2023 •
edited

Choose a reason for hiding this comment

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

I don't know but some lemmas in Algebra.Order.Group.Defs use LE. After using LE here, simpNF linter asks to delete some @[simp] there.

@j-loreaux j-loreaux 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 Dec 4, 2023
@negiizhao negiizhao removed the awaiting-author A reviewer has asked the author a question or requested changes label Dec 17, 2023
@negiizhao negiizhao added the awaiting-review The author would like community review of the PR label Dec 17, 2023
@j-loreaux
Copy link
Collaborator

I think this is fine, but I would like someone else to see it:

maintainer merge

@github-actions GitHub Actions
Copy link

🚀 Pull request has been placed on the maintainer queue by j-loreaux.

jcommelin
jcommelin approved these changes Dec 18, 2023
View reviewed changes
Copy link
Member

@jcommelin jcommelin left a comment

Choose a reason for hiding this comment

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

Thanks 🎉

bors merge

@leanprover-community-mathlib4-bot leanprover-community-mathlib4-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 Dec 18, 2023
mathlib-bors bot pushed a commit that referenced this pull request Dec 18, 2023
@negiizhao
chore(Algebra/Order/Group): change simp lemmas (#7867)
608404e
@mathlib-bors
Copy link

mathlib-bors bot commented Dec 18, 2023

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title chore(Algebra/Order/Group): change simp lemmas [Merged by Bors] - chore(Algebra/Order/Group): change simp lemmas Dec 18, 2023
@mathlib-bors mathlib-bors bot closed this Dec 18, 2023
@mathlib-bors mathlib-bors bot deleted the FR_order_simp branch December 18, 2023 07:15
awueth pushed a commit that referenced this pull request Dec 19, 2023
@negiizhao @awueth
chore(Algebra/Order/Group): change simp lemmas (#7867)
55550ea
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@eric-wieser eric-wieser eric-wieser left review comments

@j-loreaux j-loreaux j-loreaux left review comments

@jcommelin jcommelin jcommelin approved these changes

Assignees
No one assigned
Labels
ready-to-merge This PR has been sent to bors. t-algebra Algebra (groups, rings, fields etc) t-order Order hierarchy
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
6 participants
@negiizhao @leanprover-bot @j-loreaux @eric-wieser @jcommelin @leanprover-community-mathlib4-bot