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(Data/Nat/Prime): add 2 theorems #11620

Closed
wants to merge 9 commits into from
Closed

[Merged by Bors] - feat(Data/Nat/Prime): add 2 theorems #11620

wants to merge 9 commits into from

Conversation

casavaca
Copy link
Collaborator

We have 2 exists_dvd_of_not_prime, but not the other way round. I found these 2 theorems useful when proving a number is not a prime number.

Open in Gitpod

@casavaca casavaca added awaiting-review The author would like community review of the PR new-feature Add features not present in Mathlib 3 RFC Request for comment labels Mar 24, 2024
@BoltonBailey
Copy link
Collaborator

Seems useful! Could you turn it into an iff lemma so that it can be used with rw?

@casavaca
Copy link
Collaborator Author

Sure. I added 2 iff lemmas.

Shreyas4991
Shreyas4991 reviewed Mar 28, 2024
View reviewed changes
Copy link
Collaborator

@Shreyas4991 Shreyas4991 left a comment

Choose a reason for hiding this comment

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

The lemmas and proofs seem fine to me. I believe it is worth asking an expert maintainer or someone who is familiar with simp's inner workings, whether the iff lemmas ought to be simp lemmas.

@tb65536 tb65536 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 Mar 29, 2024
@casavaca casavaca 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 Mar 30, 2024
tb65536
tb65536 reviewed Mar 30, 2024
View reviewed changes
Mathlib/Data/Nat/Prime.lean Outdated Show resolved Hide resolved
Mathlib/Data/Nat/Prime.lean Outdated Show resolved Hide resolved
@casavaca
Copy link
Collaborator Author

Rebased

@semorrison
Copy link
Contributor

whether the iff lemmas ought to be simp lemmas.

No.

@semorrison
Copy link
Contributor

I don't like the naming. Just adding a 2 is not very helpful. What about not_prime_of_dvd_of_le_of_lt, etc?

@semorrison semorrison 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 new-feature Add features not present in Mathlib 3 RFC Request for comment labels Apr 2, 2024
@semorrison
Copy link
Contributor

(Doesn't need new-feature or RFC labels for a standard PR adding theorems.)

tb65536
tb65536 reviewed Apr 2, 2024
View reviewed changes
Mathlib/Data/Nat/Prime.lean Outdated
simp only [← or_iff_not_imp_left]
exact h.eq_one_or_self_of_dvd

theorem not_prime_of_dvd2 (h : ∃ m, m ∣ n ∧ 2 ≤ m ∧ m < n) : ¬Prime n := by
Copy link
Collaborator

Choose a reason for hiding this comment

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

I feel like 1 < m is more natural than 2 ≤ m (this would need to be changed on all the lemmas, including the original two).

Copy link
Collaborator Author

Choose a reason for hiding this comment

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

Would like to hear other's opinion. When I wrote this, there's already theorem exists_dvd_of_not_prime2 {n : ℕ} (n2 : 2 ≤ n) (np : ¬Prime n) : .... I'm just mirroring existing code.

@casavaca
Copy link
Collaborator Author

casavaca commented Apr 2, 2024

I updated the name to be theorem not_prime_of_dvd_of_ne {m n : ℕ} (h1 : m ∣ n) (h2 : m ≠ 1) (h3 : m ≠ n) : ¬Prime n :=. compared to not_prime_of_dvd_of_ne_of_ne, the (h2 : m ≠ 1) is not in the name. When we think about it, or when we explain to others, we tend to omit the trivial m = 1 case. So, I also omitted in the name. I just feel it's more natural, but I'm totally OK if we want to stick to the name not_prime_of_dvd_of_ne_of_ne and similarly not_prime_of_dvd_of_le_of_lt for. (2<=m && m < n)

tb65536
tb65536 reviewed Apr 2, 2024
View reviewed changes
Mathlib/Data/Nat/Prime.lean Outdated Show resolved Hide resolved
Mathlib/Data/Nat/Prime.lean Outdated
⟨exists_dvd_of_not_prime h, fun ⟨_,h1,h2,h3⟩ => not_prime_of_dvd_of_ne h1 h2 h3⟩

theorem exists_dvd_lt_iff_not_prime {n : ℕ} (h : 2 ≤ n) : (¬Prime n) ↔ ∃ m, m ∣ n ∧ 2 ≤ m ∧ m < n :=
⟨exists_dvd_of_not_prime2 h, fun ⟨_,h1,h2,h3⟩ => not_prime_of_dvd_of_lt h1 h2 h3⟩
Copy link
Collaborator

Choose a reason for hiding this comment

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

Could you also rename exists_dvd_of_not_prime2?

Copy link
Collaborator Author

Choose a reason for hiding this comment

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

It's something we ported from Mathlib3. I have no objection but I'm not sure if we should do this. @semorrison

@casavaca casavaca 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 Apr 2, 2024
adomani
adomani reviewed Apr 2, 2024
View reviewed changes
Copy link
Collaborator

@adomani adomani left a comment

Choose a reason for hiding this comment

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

The spaces are probably more consistent with overall style.

I also agree that the 2 in the name is not great.

Mathlib/Data/Nat/Prime.lean Outdated Show resolved Hide resolved
Mathlib/Data/Nat/Prime.lean Outdated Show resolved Hide resolved
casavaca and others added 2 commits April 2, 2024 09:45
@casavaca @adomani
Update Mathlib/Data/Nat/Prime.lean
399921c 
style

Co-authored-by: damiano <adomani@gmail.com>
@casavaca @adomani
Update Mathlib/Data/Nat/Prime.lean
a41bc51 
style

Co-authored-by: damiano <adomani@gmail.com>
@casavaca casavaca requested a review from semorrison April 4, 2024 03:01
@jcommelin
Copy link
Member

Let's merge this as is. Change names of existing material can be done in another PR.

bors merge

@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 Apr 13, 2024
mathlib-bors bot pushed a commit that referenced this pull request Apr 13, 2024
@casavaca
feat(Data/Nat/Prime): add 2 theorems (#11620)
7e8cd2b
@mathlib-bors
Copy link

mathlib-bors bot commented Apr 13, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat(Data/Nat/Prime): add 2 theorems [Merged by Bors] - feat(Data/Nat/Prime): add 2 theorems Apr 13, 2024
@mathlib-bors mathlib-bors bot closed this Apr 13, 2024
@mathlib-bors mathlib-bors bot deleted the user_casavaca_3 branch April 13, 2024 20:23
Louddy pushed a commit that referenced this pull request Apr 15, 2024
@casavaca @Louddy
feat(Data/Nat/Prime): add 2 theorems (#11620)
73050b6
atarnoam pushed a commit that referenced this pull request Apr 16, 2024
@casavaca @atarnoam
feat(Data/Nat/Prime): add 2 theorems (#11620)
57862c4
uniwuni pushed a commit that referenced this pull request Apr 19, 2024
@casavaca @uniwuni
feat(Data/Nat/Prime): add 2 theorems (#11620)
67e2eba
callesonne pushed a commit that referenced this pull request Apr 22, 2024
@casavaca @callesonne
feat(Data/Nat/Prime): add 2 theorems (#11620)
90a62cb
Jun2M pushed a commit that referenced this pull request Apr 24, 2024
@casavaca @Jun2M
feat(Data/Nat/Prime): add 2 theorems (#11620)
93e6557
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@tb65536 tb65536 tb65536 left review comments

@adomani adomani adomani left review comments

@Shreyas4991 Shreyas4991 Shreyas4991 approved these changes

@BoltonBailey BoltonBailey BoltonBailey approved these changes

@semorrison semorrison Awaiting requested review from semorrison

Assignees
No one assigned
Labels
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
7 participants
@casavaca @BoltonBailey @semorrison @jcommelin @Shreyas4991 @tb65536 @adomani