[Merged by Bors] - fix(order/complete_lattice): fix diamond in sup vs max and min vs inf #11309
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
eric-wieser
added
awaiting-CI
leanprover-community-bot-assistant
added
the
blocked-by-other-PR
github-actions
bot
removed
the
awaiting-CI
leanprover-community-bot-assistant
removed
the
blocked-by-other-PR
|
This PR/issue depends on: |
leanprover-community-bot-assistant
added
the
merge-conflict
leanprover-community-bot-assistant
removed
the
merge-conflict
eric-wieser
commented
Jan 11, 2022
src/data/real/ennreal.lean
Outdated
Comment on lines
87
to
88
| { max_def := rfl, | ||
| min_def := rfl, |
There was a problem hiding this comment.
I have no idea why rfl works here but the reflexivity auto_param does not. Either way, I'm inclined not to care. I can leave a TODO comment if someone else cares.
There was a problem hiding this comment.
These lines create a new diamond: now max on ennreal is not defeq sup, so we'll have two sups. Please derive linear_order and use it here. Or just use .. (infer_instance : linear_order ennreal).
There was a problem hiding this comment.
Oops, I must not have been paying attention. derive is the right choice here.
urkud
reviewed
Jan 12, 2022
| (or.inl ∘ coe_le_coe.2))), | ||
| (or.inl ∘ coe_le_coe.2))) } | ||
|
|
||
| noncomputable instance : linear_order enat := |
There was a problem hiding this comment.
Note that we have lattice.to_linear_order.
There was a problem hiding this comment.
I don't think a full lattice is available yet?
leanprover-community-bot-assistant
added
ready-to-merge
bors bot
pushed a commit
that referenced
this pull request
Jan 12, 2022
…#11309) `complete_linear_order` has separate `max` and `sup` fields. There is no need to have both, so this removes one of them by telling the structure compiler to merge the two fields. The same is true of `inf` and `min`. As well as diamonds being possible in the abstract case, a handful of concrete example of this diamond existed. `linear_order` instances with default-populated fields were usually to blame.
|
Build failed (retrying...): |
bors bot
pushed a commit
that referenced
this pull request
Jan 12, 2022
…#11309) `complete_linear_order` has separate `max` and `sup` fields. There is no need to have both, so this removes one of them by telling the structure compiler to merge the two fields. The same is true of `inf` and `min`. As well as diamonds being possible in the abstract case, a handful of concrete example of this diamond existed. `linear_order` instances with default-populated fields were usually to blame.
|
Pull request successfully merged into master. Build succeeded: |
bors
bot
changed the title
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
complete_linear_orderhas separatemaxandsupfields. There is no need to have both, so this removes one of them by telling the structure compiler to merge the two fields. The same is true ofinfandmin.As well as diamonds being possible in the abstract case, a handful of concrete example of this diamond existed.
linear_orderinstances with default-populated fields were usually to blame.