Multiset.filter without DecidablePred

Stream: Is there code for X?

[Snir Broshi]

Is there a function that filters a Multiset (like docs#Multiset.filter) but that does not require the filter to be decidable?
Since docs#Multiset.filterMap exists and doesn't require decidability I'm not sure why filter without a map needs it.
I found this awkward solution:

import Mathlib
noncomputable def filter' {α : Type*} (s : Multiset α) (p : α → Prop) :=
  @Multiset.filter α p (Classical.decPred p) s

[Eric Wieser]

Snir said:

Since docs#Multiset.filterMap exists and doesn't require decidability

This doesn't require decidability because it returns an Option. You could write a version of filter that "doesn't need" decidability because it returns a Bool, but this just passes the problem to the caller who now needs decidability to produce the Bool

[Aaron Liu]

filtermap takes the a function returning Option, so it's decidable whether an option value equals none

[Eric Wieser]

What problem are you trying to solve here?

[Snir Broshi]

I see, so everything in Multiset requires decidability. I'll use decPred then, thanks!

Eric Wieser said:

What problem are you trying to solve here?

I was messing around with roots of polynomials (which are a Multiset) and I tried to prove something like this:

theorem map_roots_eq [IsDomain A] [IsDomain B] (p : A[X]) (f : A →+* B) :
    (p.map f).roots.filter (· ∈ f.range) = p.roots.map f := by
  sorry

and I was surprised by the error. I expected Multiset to behave like Set which allows undecidable filters.

[Robin Arnez]

Because it's in the theorem statement, you should probably make DecidablePred explicit:

import Mathlib

variable {A B : Type*} [CommRing A] [CommRing B]

open Polynomial

theorem map_roots_eq [IsDomain A] [IsDomain B] (p : A[X]) (f : A →+* B) [DecidablePred (· ∈ f.range)] :
    (p.map f).roots.filter (· ∈ f.range) = p.roots.map f := by
  sorry

In proofs, you can then just use the classical tactic