[Merged by Bors] - refactor(Data/Finsupp): Make Finsupp.filter computable
#8979
Conversation
This doesn't have any significant downstream effect.
eric-wieser
added
awaiting-review
…-filter-decidable
leanprover-community-mathlib4-bot
added
the
merge-conflict
leanprover-community-mathlib4-bot
removed
the
merge-conflict
|
AFAIR, many definitions about Note: I'm definitely not an expert in computability; I think that it's better to discuss this on Zulip. |
urkud
added
RFC
eric-wieser
force-pushed
the
eric-wieser/finsupp-filter-decidable
branch
from
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.
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.
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.
Would the mathlib overview host a section on decidability?
There was a problem hiding this comment.
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.
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.
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 |
eric-wieser
force-pushed
the
eric-wieser/finsupp-filter-decidable
branch
from
3ec7517
to
71eb07c
Compare
|
bors merge |
github-actions
bot
added
ready-to-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: |
mathlib-bors
bot
changed the title
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