Finset.univ.filter vs (setOf p).toFinset

Stream: general

[Niels Voss]

If I have a finite type T and a decidable predicate p : T -> Prop, what is the best way to make the Finset containing all elements satisfying p? Both Finset.univ.filter p and (setOf p).toFinset seem to work.

[Niels Voss]

Here's the proof that these are the same thing:

import Mathlib
example {α : Type*} [Fintype α] (p : α → Prop) [DecidablePred p] : Finset.univ.filter p = (setOf p).toFinset :=
  (Set.toFinset_setOf fun x => p x).symm

[Kyle Miller]

I think they're both fine. Not sure if one is preferred over the other.

I just noticed that there seems to be a problem with the simp set. The only way for the simple by ext; simp proof to go through is for docs#Set.mem_toFinset to take an implicit argument instead of an instance argument.

import Mathlib.Tactic

import Mathlib

@[simp]
theorem Set.mem_toFinset' {α : Type*} {s : Set α} {_ : Fintype s} {a : α} : a ∈ s.toFinset ↔ a ∈ s := by
  simp [toFinset]

example {α : Type*} [Fintype α] (p : α → Prop) [DecidablePred p] :
    Finset.univ.filter p = (setOf p).toFinset :=
  by ext; simp

[Yaël Dillies]

Personally, I much prefer Finset.univ.filter p and I am hoping we eventually can make {x | p x} notation for it.

[Yury G. Kudryashov]

It works only for Fintypes while Set.toFinset works if you have Fintype s (not Fintype α).

[Niels Voss]

If you have Fintype α do you automatically have Fintype (setOf p)?

[Yaël Dillies]

No, you also need DecidablePred p

[Niels Voss]

That's true. But DecidablePred p is also needed for Finset.univ.filter. So can (setOf p).toFinset be used in place of Finset.univ.filter, but not vice versa?

[Kyle Miller]

Yes, that's right.

You can also go through docs#Set.Finite to avoid needing DecidablePred. These use docs#Finite instances rather than docs#Fintype instances.

variable {α : Type*} [Fintype α] (p : α → Prop)

#check (setOf p).toFinite.toFinset -- `toFinset` alone causes an instance failure.

The cost of this is that it depends on the axiom of choice, and it's not computable in some sense.

[Niels Voss]

But that gets you a noncomputable Finset, which is what you would have ended up with anyways had you just used choice to produce a DecidablePred p instance. Although I guess this helps avoid situations where two different DecdiablePred instances are use and the terms don't unify.