[Merged by Bors] - refactor: Make CompleteLinearOrder extend BiheytingAlgebra
#12731
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
In fact, linear orders themselves are biheyting algebras, but registering this as an instance causes a bit of a chicken and the egg problem which I'm not willing to try solving. `CompleteLinearOrder` really does need to extend `BiheytingAlgebra` if we are going to make `Frame` extend `HeytingAlgebra`.
4 tasks
eric-wieser
reviewed
May 7, 2024
Mathlib/Order/UpperLower/Basic.lean
Outdated
Comment on lines
1041
to
1043
| decidableLE := Classical.decRel _ | ||
| decidableEq := Classical.decRel _ | ||
| decidableLT := Classical.decRel _ |
There was a problem hiding this comment.
I worry this is going to create a diamond with the instLinearOrder instance above. Can't you use __ := instLinearOrder here?
There was a problem hiding this comment.
Both are definitely Classical.decRel _ because they prove decidability of inclusions of sets.
Spread notation seems to be broken/uncover a diamond. This works:
noncomputable instance UpperSet.instCompleteLinearOrder : CompleteLinearOrder (UpperSet α) where
__ := completelyDistribLattice
__ := instLinearOrder
himp := LinearOrder.toBiheytingAlgebra.himp
le_himp_iff := LinearOrder.toBiheytingAlgebra.le_himp_iff
compl := LinearOrder.toBiheytingAlgebra.compl
himp_bot := LinearOrder.toBiheytingAlgebra.himp_bot
sdiff := LinearOrder.toBiheytingAlgebra.sdiff
hnot := LinearOrder.toBiheytingAlgebra.hnot
sdiff_le_iff := LinearOrder.toBiheytingAlgebra.sdiff_le_iff
top_sdiff := LinearOrder.toBiheytingAlgebra.top_sdiff
This works too:
noncomputable instance UpperSet.instCompleteLinearOrder : CompleteLinearOrder (UpperSet α) :=
{ completelyDistribLattice, instLinearOrder, LinearOrder.toBiheytingAlgebra with }
This doesn't:
noncomputable instance UpperSet.instCompleteLinearOrder : CompleteLinearOrder (UpperSet α) where
__ := completelyDistribLattice
__ := instLinearOrder
__ := LinearOrder.toBiheytingAlgebra
There was a problem hiding this comment.
Is it possible to have "tests" to confirm the definitional equality (with_reducible_and_instances rfl?) of diamonds?
There was a problem hiding this comment.
How would that help here? I think it's a metavariable issue with the spread notation, not an actual non-defeq diamond.
mathlib-bors bot
pushed a commit
that referenced
this pull request
Jun 24, 2024
In fact, linear orders themselves are biheyting algebras, but registering this as an instance causes a bit of a chicken and the egg problem which I'm not willing to try solving. `CompleteLinearOrder` really does need to extend `BiheytingAlgebra` if we are going to make `Frame` extend `HeytingAlgebra`. This is a step towards #10560
|
Pull request successfully merged into master. Build succeeded: |
mathlib-bors
bot
changed the title
CompleteLinearOrder extend BiheytingAlgebraCompleteLinearOrder extend BiheytingAlgebra
kbuzzard
pushed a commit
that referenced
this pull request
Jun 26, 2024
In fact, linear orders themselves are biheyting algebras, but registering this as an instance causes a bit of a chicken and the egg problem which I'm not willing to try solving. `CompleteLinearOrder` really does need to extend `BiheytingAlgebra` if we are going to make `Frame` extend `HeytingAlgebra`. This is a step towards #10560
dagurtomas
pushed a commit
that referenced
this pull request
Jul 2, 2024
In fact, linear orders themselves are biheyting algebras, but registering this as an instance causes a bit of a chicken and the egg problem which I'm not willing to try solving. `CompleteLinearOrder` really does need to extend `BiheytingAlgebra` if we are going to make `Frame` extend `HeytingAlgebra`. This is a step towards #10560
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.
In fact, linear orders themselves are biheyting algebras, but registering this as an instance causes a bit of a chicken and the egg problem which I'm not willing to try solving.
CompleteLinearOrderreally does need to extendBiheytingAlgebraif we are going to makeFrameextendHeytingAlgebra.This is a step towards #10560