Zulip Chat Archive

Stream: general

Topic: finset.filter

Johan Commelin (Apr 28 2020 at 08:37):

I am often writing

let S : finset (σ → K) := univ.filter (λ x, x i = 0),

I don't really like this, for two reasons:

  1. It would be infinitely better if we could write { x | x i = 0 }.
  2. If you have hx : x ∈ S and rewrite mem_filter at hx, then you end up with hx : x ∈ univ ∧ x i = 0.

Of course (2) can be solved by a simp-lemma mem_filter_univ, but is there something that could be done about the aesthetics?

Mario Carneiro (Apr 28 2020 at 08:39):

I really want to have a has_sep instance for finset, but the type doesn't work - the predicate has to be decidable

Mario Carneiro (Apr 28 2020 at 08:39):

maybe we should just have a noncomputable instance

Johan Commelin (Apr 28 2020 at 08:48):

What are the consequences of doing that?

Johan Commelin (Apr 28 2020 at 08:49):

I guess we don't want to break computability for every fintype. Fintypes are a place where computation can be pretty useful.

Kenny Lau (Apr 28 2020 at 08:50):

I mean you can define a non-computable version of filter and call it ncfilter or something

Kenny Lau (Apr 28 2020 at 08:50):

and then the has_sep would call ncfilter

Johan Commelin (Apr 28 2020 at 08:50):

With a low priority?

Kenny Lau (Apr 28 2020 at 08:51):

I know nothing about priority

Johan Commelin (Apr 28 2020 at 08:51):

But we could still end up with the wrong { x | is_cool x } on fintypes with decidable eq etc, right?

Kenny Lau (Apr 28 2020 at 08:52):

I don't understand. We're using { x | some_nc_pred x }

Johan Commelin (Apr 28 2020 at 08:53):

Hmm, I guess I'm the one that is confused.

Johan Commelin (Apr 28 2020 at 08:54):

I just know that stuff is more complicated and ugly than it should be. And I would like some fairy or elf to fix it.

Kenny Lau (Apr 28 2020 at 09:01):

  1. looks like { x : ℕ | x = x } is hard-wired into Lean with C++ so we can't change it, and it isn't has_sep
  2. and we already have a has_sep for finset
  3. so the best we can do is { x ∈ univ | x i = 0 }

Johan Commelin (Apr 28 2020 at 09:03):

  1. "we can't change it" is no longer true
  2. ok, that's cool, thanks!
  3. which looks a lot better, thanks so much! But the ∈ univ is of course really silly

Kenny Lau (Apr 28 2020 at 09:17):

import data.fintype.basic

universes u

noncomputable def finset_of {α : Type u} [fintype α] (p : α → Prop) : finset α :=
@finset.filter α p (classical.dec_pred p) finset.univ

notation `{` binders ` | ` r:(scoped p, finset_of p) `}` := r

-- { (x : bool) | x = x} : finset bool
#check { x : bool | x = x }

... but the downside is that the set equivalent is no longer within reach

Gabriel Ebner (Apr 28 2020 at 09:19):

There's no need to make this noncomputable:

def finset.set_of {α} [fintype α] (p : α → Prop) [decidable_pred p] : finset α :=
univ.filter p

localized "notation `{` binders ` | ` r:(scoped p, finset.set_of p) `}` := r" in finset

#eval { x : bool | x = tt }

Patrick Massot (Apr 28 2020 at 09:20):

Would this break other uses of this notation?

Kenny Lau (Apr 28 2020 at 09:20):

yeah this still breaks the set equivalent

Gabriel Ebner (Apr 28 2020 at 09:21):

The bigger problem is that all the other bracket notations disappear as well. Think of { x // x > 0 } or {1,2,3}.

Kenny Lau (Apr 28 2020 at 09:21):

oh no

Gabriel Ebner (Apr 28 2020 at 09:22):

The obvious solution is to write ❴ x : bool | x = x ❵ instead.

Last updated: Dec 20 2023 at 11:08 UTC