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

[Merged by Bors] - feat(algebra/ordered_semiring): relax 0 < 1 to 0 ≤ 1#4363

Closed
kim-em wants to merge 45 commits intomasterfrom
ordered_semiring_zero_le_one
Closed

[Merged by Bors] - feat(algebra/ordered_semiring): relax 0 < 1 to 0 ≤ 1#4363
kim-em wants to merge 45 commits intomasterfrom
ordered_semiring_zero_le_one

Conversation

@kim-em
Copy link
Copy Markdown
Collaborator

@kim-em kim-em commented Oct 2, 2020 •
edited by github-actions bot
Loading

@kim-em kim-em marked this pull request as ready for review October 2, 2020 11:45
gebner
gebner reviewed Oct 2, 2020
View reviewed changes
@kim-em @gebner
Update src/logic/nontrivial.lean
f2eb085 
Co-authored-by: Gabriel Ebner <gebner@gebner.org>
kim-em
kim-em commented Oct 2, 2020
View reviewed changes
kim-em
kim-em commented Oct 2, 2020
View reviewed changes
kim-em
kim-em commented Oct 2, 2020
View reviewed changes
@kim-em @gebner
Apply suggestions from code review
b17270f 
Co-authored-by: Gabriel Ebner <gebner@gebner.org>
gebner
gebner reviewed Oct 2, 2020
View reviewed changes
robertylewis
robertylewis reviewed Oct 2, 2020
View reviewed changes
@jcommelin
Copy link
Copy Markdown
Member

jcommelin commented Oct 2, 2020

Also introduces a nontriviality tactic

@semorrison Would you mind splitting the PR into two pieces?

@github-actions github-actions bot removed the merge-conflict Please `git merge origin/master` then a bot will remove this label. label Oct 15, 2020
@kim-em
Copy link
Copy Markdown
Collaborator Author

kim-em commented Oct 15, 2020

What's the advantage of implementing this by extending nontrivial rather than just adding the field (zero_lt_one : (0 : R) < 1) back? I didn't look through the PR closely but it seems to have been a rather invasive change.

@rwbarton, I did this largely because domain extends nontrivial; I thought this design would be a better parallel for things already in the library, and means that the instance linear_ordered_ring.to_domain can just copy over the relevant field.

I'm happy to try switching it over if anyone would prefer that.

@kim-em kim-em added awaiting-review The author would like community review of the PR and removed delegated The PR author may merge after reviewing final suggestions. labels Oct 15, 2020
@Vierkantor
Copy link
Copy Markdown
Collaborator

Vierkantor commented Oct 16, 2020

What's the advantage of implementing this by extending nontrivial rather than just adding the field (zero_lt_one : (0 : R) < 1) back? I didn't look through the PR closely but it seems to have been a rather invasive change.

@rwbarton, I did this largely because domain extends nontrivial; I thought this design would be a better parallel for things already in the library, and means that the instance linear_ordered_ring.to_domain can just copy over the relevant field.

I'm happy to try switching it over if anyone would prefer that.

I'm cautiously in favour of using nontrivial, it seems like it's better to use more generic concepts in definitions (also providing some better support for tooling, e.g. the nontriviality tactic).

Many of the changes in this PR go into fixing expressions of the form @zero_lt_one R _, do you think it would be a good idea (not for this PR) to make the type argument explicit for that family of declarations?

@kim-em
Copy link
Copy Markdown
Collaborator Author

kim-em commented Oct 17, 2020

Many of the changes in this PR go into fixing expressions of the form @zero_lt_one R _, do you think it would be a good idea (not for this PR) to make the type argument explicit for that family of declarations?

I don't think so --- there are 273 appearances of zero_lt_one in mathlib at the moment, and only 13 of those are @zero_lt_one.

@jcommelin jcommelin requested a review from Vierkantor October 17, 2020 18:22
urkud
urkud reviewed Oct 17, 2020
View reviewed changes
@github-actions github-actions bot added the merge-conflict Please `git merge origin/master` then a bot will remove this label. label Oct 17, 2020
@github-actions github-actions bot removed the merge-conflict Please `git merge origin/master` then a bot will remove this label. label Oct 19, 2020
Vierkantor
Vierkantor approved these changes Oct 19, 2020
View reviewed changes
Copy link
Copy Markdown
Collaborator

@Vierkantor Vierkantor left a comment

Choose a reason for hiding this comment

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

I'm happy with this except for the one open suggestion. Let's merge this before more conflicts arise.

bors d+

@bors
Copy link
Copy Markdown

bors bot commented Oct 19, 2020

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

@Vierkantor Vierkantor added delegated The PR author may merge after reviewing final suggestions. and removed awaiting-review The author would like community review of the PR labels Oct 19, 2020
@kim-em
Copy link
Copy Markdown
Collaborator Author

kim-em commented Oct 19, 2020

bors merge

@github-actions github-actions bot added the ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) label Oct 19, 2020
This was referenced Oct 19, 2020
Closed
Closed
Closed
Closed
Closed
bors bot pushed a commit that referenced this pull request Oct 19, 2020
@kim-em @robertylewis
feat(algebra/ordered_semiring): relax 0 < 1 to 0 ≤ 1 (#4363)
4140f78 
Per [discussion](#4296 (comment)) in #4296.



Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Co-authored-by: Rob Lewis <Rob.y.lewis@gmail.com>
@bors
Copy link
Copy Markdown

bors bot commented Oct 19, 2020

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat(algebra/ordered_semiring): relax 0 < 1 to 0 ≤ 1 [Merged by Bors] - feat(algebra/ordered_semiring): relax 0 < 1 to 0 ≤ 1 Oct 19, 2020
@bors bors bot closed this Oct 19, 2020
@bors bors bot deleted the ordered_semiring_zero_le_one branch October 19, 2020 13:52
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.

Reviewers

5 more reviewers

@urkud urkud urkud left review comments

@gebner gebner gebner left review comments

@robertylewis robertylewis robertylewis left review comments

@bryangingechen bryangingechen bryangingechen left review comments

@Vierkantor Vierkantor Vierkantor approved these changes

Reviewers whose approvals may not affect merge requirements

Assignees

No one assigned

Labels

delegated The PR author may merge after reviewing final suggestions. 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.

8 participants

@kim-em @jcommelin @rwbarton @Vierkantor @urkud @gebner @robertylewis @bryangingechen