Sep notation

Stream: mathlib4

[Johan Commelin]

In Lean 4, the notation {x | p x} is hard-coded to be about Set. This makes the docs4#Sep class useless. In Finset.Basic I have written a porting note:

-- Porting note: The notation `{ x ∈ s | p x }` in Lean 4 is hardcoded to be about `Set`.
-- So at the moment the whole `Sep`-class is useless, as it doesn't have notation.
-- /-- The following instance allows us to write `{x ∈ s | p x}` for `Finset.filter p s`.
--   We don't want to redo all lemmas of `Finset.filter` for `Sep.sep`, so we make sure that `simp`
--   unfolds the notation `{x ∈ s | p x}` to `Finset.filter p s`.
-- -/
-- noncomputable instance {α : Type _} : Sep α (Finset α) :=
--   ⟨fun p x => x.filter p⟩

-- -- @[simp] -- Porting note: not a simp-lemma until `Sep`-notation is fixed.
-- theorem sep_def {α : Type _} (s : Finset α) (p : α → Prop) : { x ∈ s | p x } = s.filter p := by
--   ext
--   simp
-- #align finset.sep_def Finset.sep_def

How important is sep notation on finsets?

[Kyle Miller]

Huh, that instance has been around for 3 years and I've never noticed it. I think all of us who use finset mathematically use finset.filter directly, and when we want to use separation notation then we use set and set.finite.

One reason I wouldn't use has_sep for finset (even though I'm now aware of it) is that all the lemmas are in terms of finset.filter. If this were notation that unfolded immediately to finset.filter, then that would be more practical.

[Ruben Van de Velde]

I guess that's why there's a simp lemma that converts to filter

[Kyle Miller]

Yep, but that's not enough since you can't write any simp lemmas that use sep notation on the LHS.

[Eric Wieser]

Its pointless noncomputability also makes using it undesirable

[Kyle Miller]

If somehow there could be separation notation that elaborates to finset.filter and picks up on a decidability instance, that'd be cool.

I'd also be cool if big unions and big intersections could work equally well for sets and finsets. That's something I'd tried doing with complicated typeclasses, but it never worked quite right -- I'm hopefully that we'll eventually exploit Lean 4 features to get this to work, though after everything's been ported.