Skip to content
This repository was archived by the owner on Jul 24, 2024. It is now read-only.

[Merged by Bors] - chore(algebra/order/lattice_group): Golf#18046

Closed
mans0954 wants to merge 19 commits intomasterfrom
mans0954/lattice_group-remove-simp
Closed

[Merged by Bors] - chore(algebra/order/lattice_group): Golf#18046
mans0954 wants to merge 19 commits intomasterfrom
mans0954/lattice_group-remove-simp

Conversation

@mans0954
Copy link
Copy Markdown
Collaborator

@mans0954 mans0954 commented Jan 2, 2023 •
edited by YaelDillies
Loading

Golf proofs and remove a duplicate lemma.

Match leanprover-community/mathlib4#2478

Open in Gitpod

@mans0954 mans0954 mentioned this pull request Jan 2, 2023
Closed
eric-wieser
eric-wieser reviewed Jan 2, 2023
View reviewed changes
eric-wieser
eric-wieser reviewed Jan 2, 2023
View reviewed changes
eric-wieser
eric-wieser reviewed Jan 2, 2023
View reviewed changes
eric-wieser
eric-wieser reviewed Jan 3, 2023
View reviewed changes
eric-wieser
eric-wieser reviewed Jan 3, 2023
View reviewed changes
mans0954 and others added 4 commits January 3, 2023 17:51
@mans0954 @eric-wieser
Update src/algebra/order/lattice_group.lean
bffa510 
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
@mans0954 @eric-wieser
Update src/algebra/order/lattice_group.lean
6ff4ce5 
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
@mans0954
Fix mul_sup
00fe2eb
@mans0954
Remove last nested by
e472124
@mans0954 mans0954 added the awaiting-review The author would like community review of the PR label Jan 3, 2023
@eric-wieser eric-wieser added awaiting-CI The author would like to see what CI has to say before doing more work. and removed awaiting-CI The author would like to see what CI has to say before doing more work. labels Jan 3, 2023
eric-wieser
eric-wieser reviewed Jan 3, 2023
View reviewed changes
eric-wieser
eric-wieser reviewed Jan 3, 2023
View reviewed changes
eric-wieser
eric-wieser reviewed Jan 3, 2023
View reviewed changes
mans0954 and others added 3 commits January 3, 2023 20:49
@alreadydone alreadydone changed the title refactor(algebra.order.lattice_group): Replace simps with direct proofs refactor(algebra/order/lattice_group): Replace simps with direct proofs Jan 7, 2023
@mans0954
Copy link
Copy Markdown
Collaborator Author

mans0954 commented Feb 22, 2023

@YaelDillies several of the changes replace two or three tactics with a single call to rw e.g.

by { rw le_antisymm_iff, simp only [one_le_neg, and_true], rw [neg_le_one_iff, inv_le_one'], }

is replaced by

by rw [le_antisymm_iff, neg_le_one_iff, inv_le_one', and_iff_left (one_le_neg _)]

I don't know whether the preference in mathlib is for explicit proofs or letting simp do as much work as possible?

The proof of sup_div_inf_eq_abs_div is reduced from seven lines to a single rw.

I'd agree that the mul_sup and mul_inf proofs look worse in this PR.

Either way, I don't think this PR is important now, so I'm happy to close it.

@mans0954 mans0954 closed this Feb 22, 2023
@YaelDillies
Copy link
Copy Markdown
Collaborator

YaelDillies commented Feb 22, 2023

This was not a rhetorical question. I genuinely didn't know whether the golfs had been applied to the port without backport. But now I've just found golfs that you mustn't have ported, so please open a matching PR to mathlib4.

@YaelDillies YaelDillies reopened this Feb 22, 2023
@YaelDillies YaelDillies added the modifies-synchronized-file This PR touches a files that has already been ported to mathlib4, and may need a synchronization PR. label Feb 22, 2023
@mans0954
Copy link
Copy Markdown
Collaborator Author

mans0954 commented Feb 22, 2023

This was not a rhetorical question. I genuinely didn't know whether the golfs had been applied to the port without backport. But now I've just found golfs that you mustn't have ported, so please open a matching PR to mathlib4.

Sorry, I'm still a little unclear what you want me to do? Do you mean I should backport these changes from mathlib4 to mathlib, or forward port the additional mathlib changes in this PR (including the ones you pushed today) to mathlib4?

If the latter, is there tooling to do this, or do I do it manually. From what I can see mathport only works on the master branch of mathlib?

@YaelDillies
Copy link
Copy Markdown
Collaborator

YaelDillies commented Feb 24, 2023

The ones from this PR. You shouldn't need to translate anything yourself. Simply open an empty PR to mathlib4, and reference it here.

@eric-wieser
Copy link
Copy Markdown
Member

eric-wieser commented Feb 24, 2023

@YaelDillies, how much of the PR is now your revised proofs rather than @mans0954? If it's mostly your work now, I think the onus is on you to forward port!

@YaelDillies YaelDillies mentioned this pull request Feb 24, 2023
Closed
@YaelDillies
Copy link
Copy Markdown
Collaborator

YaelDillies commented Feb 24, 2023

Sure: leanprover-community/mathlib4#2478

@YaelDillies YaelDillies changed the title refactor(algebra/order/lattice_group): Replace simps with direct proofs chore(algebra/order/lattice_group): Golf Feb 24, 2023
@YaelDillies YaelDillies added awaiting-review The author would like community review of the PR and removed awaiting-author A reviewer has asked the author a question or requested changes labels Feb 24, 2023
@mans0954
Copy link
Copy Markdown
Collaborator Author

mans0954 commented Feb 24, 2023

Sure: leanprover-community/mathlib4#2478

Thanks!

For the benefit of my understanding, how does an empty PR result in these changes getting forward ported to mathlib4?

@YaelDillies
Copy link
Copy Markdown
Collaborator

YaelDillies commented Feb 25, 2023

I will fill in the empty PR once mathport has run on those changes after merge.

@YaelDillies
Copy link
Copy Markdown
Collaborator

YaelDillies commented Mar 26, 2023

I think this is pretty clearly an improvement, so

maintainer merge

@github-actions
Copy link
Copy Markdown

github-actions bot commented Mar 26, 2023

🚀 Pull request has been placed on the maintainer queue by YaelDillies.

eric-wieser
eric-wieser approved these changes Mar 31, 2023
View reviewed changes
Copy link
Copy Markdown
Member

@eric-wieser eric-wieser left a comment

Choose a reason for hiding this comment

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

bors merge

Thanks!

@leanprover-community-bot-assistant leanprover-community-bot-assistant added ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) and removed awaiting-review The author would like community review of the PR labels Mar 31, 2023
bors bot pushed a commit that referenced this pull request Apr 1, 2023
@mans0954 @YaelDillies
chore(algebra/order/lattice_group): Golf (#18046)
474656f 
Golf proofs and remove a duplicate lemma.



Co-authored-by: Christopher Hoskin <mans0954@users.noreply.github.com>
Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
@bors
Copy link
Copy Markdown

bors bot commented Apr 1, 2023

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title chore(algebra/order/lattice_group): Golf [Merged by Bors] - chore(algebra/order/lattice_group): Golf Apr 1, 2023
@bors bors bot closed this Apr 1, 2023
@bors bors bot deleted the mans0954/lattice_group-remove-simp branch April 1, 2023 02:58
bors bot pushed a commit to leanprover-community/mathlib4 that referenced this pull request Apr 2, 2023
@YaelDillies
chore: Golf algebra.order.lattice_group (#2478)
8882e05 
Match leanprover-community/mathlib3#18046
MonadMaverick pushed a commit to leanprover-community/mathlib4 that referenced this pull request Apr 9, 2023
@YaelDillies @MonadMaverick
chore: Golf algebra.order.lattice_group (#2478)
8c611ed 
Match leanprover-community/mathlib3#18046
MonadMaverick pushed a commit to MonadMaverick/mathlib4 that referenced this pull request Apr 9, 2023
@YaelDillies @MonadMaverick
chore: Golf algebra.order.lattice_group (leanprover-community#2478)
7c31fb8 
Match leanprover-community/mathlib3#18046
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.

Reviewers

1 more reviewer

@eric-wieser eric-wieser eric-wieser approved these changes

Reviewers whose approvals may not affect merge requirements

Assignees

No one assigned

Labels

modifies-synchronized-file This PR touches a files that has already been ported to mathlib4, and may need a synchronization PR. ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.)

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

4 participants

@mans0954 @YaelDillies @eric-wieser @leanprover-community-bot-assistant