-
Notifications
You must be signed in to change notification settings - Fork 298
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.
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
[Merged by Bors] - feat(algebra/order/absolute_value): Absolute values are multiplicative ring norms #16919
Closed
Closed
[Merged by Bors] - feat(algebra/order/absolute_value): Absolute values are multiplicative ring norms #16919
Changes from 6 commits
Commits
Show all changes
7 commits
Select commit
Hold shift + click to select a range
6f617c3
feat(algebra/order/absolute_value): Absolute values are multiplicativ…
YaelDillies f601adc
Merge remote-tracking branch 'origin/master' into absolute_value_mul_…
YaelDillies 3fe981f
fix analysis.seminorm
YaelDillies 5068670
fix analysis.normed.ring.seminorm
YaelDillies a5a4015
add docs
YaelDillies 2806e6f
Merge remote-tracking branch 'origin/master' into absolute_value_mul_…
YaelDillies 525e692
library note
YaelDillies File filter
Filter by extension
Conversations
Failed to load comments.
Jump to
Jump to file
Failed to load files.
Diff view
Diff view
There are no files selected for viewing
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
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
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
Oops, something went wrong.
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.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Could you explain what this means specifically? Do you have an example of this instance not applying when it should?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
If I do
typeclass search fails, even though
ring_seminorm_class.to_add_group_seminorm_class
andadd_group_seminorm_class.to_nonneg_hom_class
are both instances.There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Aha, this is because of diamond inheritance in instance parameters that depend on an
out_param
:add_group_seminorm_class.to_nonneg_hom_class
requires alinear_ordered_add_comm_monoid
instance, andring_seminorm_class.to_add_group_seminorm_class
requires aordered_semiring
instance. These have a common ancestor inordered_add_comm_monoid
so normally what happens is Lean wants to unify@linear_ordered_add_comm_monoid.to_ordered_add_comm_monoid β ?inst1 =?= @ordered_semiring.to_ordered_add_comm_monoid β ?inst2
, sees that it can unstuck by inferring instances for?inst1
and?inst2
, unfolds those instances, compares equality field-wise, and succeeds.Here, because
β
is anout_param
ofnonneg_hom_class
,β
becomes a metavariable that isn't solved until thering_seminorm_class
parameter is filled in. But we can't fill that in until we reachring_seminorm_class
fromadd_group_seminorm_class
. And we can't check that these are defeq because it requires getting unstuck, and it can't unstuck because the instance is full of metavariables, so Lean gives up the equality check.Hacking on mathlib4#888 has taught me the Lean 4 synthesis algorithm is even worse at instance params depending on
outParam
s so I expect the conclusion would have to be that this instance is required to help Lean get unstuck.There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Oh dear 😦
Then I guess this PR is ready
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Let's add a comment:
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I've edited the suggestion to add a pointer to a relevant Zulip thread. If we really want to get this working, I think the right solution is to forbid extending a class in conditions where this limitation applies, and instead use unbundled inheritance.
If you want to add a library note, I'd add it as a separate comment, specifying exactly what goes wrong and some options for dealing with it: