-
Notifications
You must be signed in to change notification settings - Fork 315
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] - refactor(Data/Finsupp): Make Finsupp.filter
computable
#8979
Conversation
This doesn't have any significant downstream effect.
…-filter-decidable
AFAIR, many definitions about Note: I'm definitely not an expert in computability; I think that it's better to discuss this on Zulip. |
200288b
to
71eb07c
Compare
support := | ||
haveI := Classical.decPred p | ||
f.support.filter fun a => p a | ||
def filter (p : α → Prop) [DecidablePred p] (f : α →₀ M) : α →₀ M where |
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 understand that if somebody wants to use Finsupp.filter
, either their predicate is decidable (possibly by adding that to the instances of the theorem), and then everything's OK, otherwise one invokes Classical.decPred
before using it, as you do below in coeff_weightedHomogeneousComponent
.
It would probably be interesting that there be a general page on mathlib's documentation about this, hoping that everybody will care and agree.
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.
Unfortunately I don't think we have any good mechanism at the moment to host such a general documentation page; library notes are not yet shown in doc-gen...
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.
Would the mathlib overview host a section on decidability?
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.
Unfortunately I don't think we have any good mechanism at the moment to host such a general documentation page; library notes are not yet shown in doc-gen...
At least temporarily the github wiki feature could host things like this?
@@ -966,9 +959,11 @@ theorem prod_div_prod_filter [CommGroup G] (g : α → M → G) : | |||
|
|||
end Zero | |||
|
|||
theorem filter_pos_add_filter_neg [AddZeroClass M] (f : α →₀ M) (p : α → Prop) : | |||
theorem filter_pos_add_filter_neg [AddZeroClass M] (f : α →₀ M) (p : α → Prop) [DecidablePred p] : |
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 think that we should also assume DecidablePred (¬p ·)
so that this lemma applies in case if the second filter
uses a classical instance.
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.
Otherwise LGTM. Thanks!
bors d+
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.
The current statement matches DFinsupp,filter_pos_add_filter_neg
, so I'd prefer to declare this out of scope. I think we should try doing this to everything that uses ¬p
at once, and see if anything breaks: in a separate PR.
✌️ eric-wieser can now approve this pull request. To approve and merge a pull request, simply reply with |
3ec7517
to
71eb07c
Compare
bors merge |
This doesn't have any significant downstream fallout, and removes some subsingleton elimination from one or two proofs. This enables some trivial computations on factorizations, eg finding the odd prime factors: ```lean /-- info: fun₀ | 3 => 2 | 5 => 1 -/ #guard_msgs in #eval (Nat.factorization 720).filter Odd ``` [Zulip thread](https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/.238979.20making.20Finsupp.2Efilter.20computable/near/420898226)
Pull request successfully merged into master. Build succeeded: |
Finsupp.filter
computableFinsupp.filter
computable
This doesn't have any significant downstream fallout, and removes some subsingleton elimination from one or two proofs. This enables some trivial computations on factorizations, eg finding the odd prime factors: ```lean /-- info: fun₀ | 3 => 2 | 5 => 1 -/ #guard_msgs in #eval (Nat.factorization 720).filter Odd ``` [Zulip thread](https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/.238979.20making.20Finsupp.2Efilter.20computable/near/420898226)
This doesn't have any significant downstream fallout, and removes some subsingleton elimination from one or two proofs. This enables some trivial computations on factorizations, eg finding the odd prime factors: ```lean /-- info: fun₀ | 3 => 2 | 5 => 1 -/ #guard_msgs in #eval (Nat.factorization 720).filter Odd ``` [Zulip thread](https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/.238979.20making.20Finsupp.2Efilter.20computable/near/420898226)
This doesn't have any significant downstream fallout, and removes some subsingleton elimination from one or two proofs. This enables some trivial computations on factorizations, eg finding the odd prime factors: ```lean /-- info: fun₀ | 3 => 2 | 5 => 1 -/ #guard_msgs in #eval (Nat.factorization 720).filter Odd ``` [Zulip thread](https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/.238979.20making.20Finsupp.2Efilter.20computable/near/420898226)
This doesn't have any significant downstream fallout, and removes some subsingleton elimination from one or two proofs. This enables some trivial computations on factorizations, eg finding the odd prime factors: ```lean /-- info: fun₀ | 3 => 2 | 5 => 1 -/ #guard_msgs in #eval (Nat.factorization 720).filter Odd ``` [Zulip thread](https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/.238979.20making.20Finsupp.2Efilter.20computable/near/420898226)
This doesn't have any significant downstream fallout, and removes some subsingleton elimination from one or two proofs. This enables some trivial computations on factorizations, eg finding the odd prime factors: ```lean /-- info: fun₀ | 3 => 2 | 5 => 1 -/ #guard_msgs in #eval (Nat.factorization 720).filter Odd ``` [Zulip thread](https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/.238979.20making.20Finsupp.2Efilter.20computable/near/420898226)
This doesn't have any significant downstream fallout, and removes some subsingleton elimination from one or two proofs.
This enables some trivial computations on factorizations, eg finding the odd prime factors:
Zulip thread