Zulip Chat Archive

Stream: Is there code for X?

Topic: Multiset to set


view this post on Zulip Anne Baanen (Sep 04 2020 at 16:01):

What is the canonical way to get a set α containing the elements of s : multiset α? (∈ s), ↑s.to_finset, something else?

view this post on Zulip Adam Topaz (Sep 04 2020 at 16:16):

You can always abuse the has_mem instance :)

view this post on Zulip Adam Topaz (Sep 04 2020 at 16:16):

I don't know how canonical that is.

view this post on Zulip Anne Baanen (Sep 04 2020 at 16:21):

From some experimenting, to_finset has better support for rw and simp than (∈ s), but either way is not very nice.

view this post on Zulip Adam Topaz (Sep 04 2020 at 16:22):

Ah I see, that's exactly what you meant by (\in S).

view this post on Zulip Anne Baanen (Sep 04 2020 at 16:24):

Indeed.

view this post on Zulip Anne Baanen (Sep 04 2020 at 16:24):

I guess less inscrutability is another argument for to_finset.

view this post on Zulip Adam Topaz (Sep 04 2020 at 16:24):

This is completely a personal opinion (and clearly does not agree with what's done in mathlib), but I think the canonical way to produce a set from anything should always be via has_mem. This would at least provide some consistency.

view this post on Zulip Anne Baanen (Sep 04 2020 at 16:26):

I agree. In fact, I think there was a suggestion floating around that has_mem should only exist for set, and to access the syntax for other types, you should just provide the coercion to set.

view this post on Zulip Adam Topaz (Sep 04 2020 at 16:27):

has_mem should not even exist. It should just be notation for sets.

view this post on Zulip Kevin Buzzard (Sep 04 2020 at 16:31):

I wrote thousands of lines of group theory over the summer and I would have gone completely nuts if I couldn't write x \in H for H : subgroup G.

view this post on Zulip Adam Topaz (Sep 04 2020 at 16:32):

But you already introduced the coercion to set G as carrier right?

view this post on Zulip Adam Topaz (Sep 04 2020 at 16:32):

So why not use it?

view this post on Zulip Adam Topaz (Sep 04 2020 at 16:36):

This way you would never have to prove that {x : G | x \in H} = (H : set G).

view this post on Zulip Reid Barton (Sep 04 2020 at 16:38):

I tried making this change in core Lean once but things failed horribly :frown:
I think mainly what broke were things like (made up example) ∀ l, (∀ x, x ∉ l) ↔ list.length l = 0 where current Lean keeps an open mind about l until it sees list.length l, but with the change x ∉ l already makes Lean think l is a set and when it gets to list.length l it's too late.

view this post on Zulip Reid Barton (Sep 04 2020 at 16:40):

I gave up at that point but it's possible a more cunning approach would have worked.

view this post on Zulip Adam Topaz (Sep 04 2020 at 16:41):

In this case, wouldn't this be okay? ∀ l, list.length l = 0 ↔ (∀ x, x ∉ l)

view this post on Zulip Reid Barton (Sep 04 2020 at 16:42):

Probably, but there were many examples of this kind of thing

view this post on Zulip Kyle Miller (Sep 04 2020 at 17:37):

I wonder what it would be like if there were a mechanism to make every theorem and definition about set be automatically generalized to anything with a has_mem instance, since has_mem is basically a coercion to a set already:

def has_mem_to_set {α : Type*} {β : Type*} [has_mem α β] (y : β) : set α :=
set_of (λ x, x  y)

(It seems like it's more convenient proving things about sets rather than about types with has_mem instances, so that's why I'm suggesting the idea of automatic generalization. This is something an attribute could do, right?)

view this post on Zulip Kevin Buzzard (Sep 04 2020 at 17:39):

Adam Topaz said:

So why not use it?

Because then I get random up-arrows everywhere, which makes the code look more confusing to mathematicians?

view this post on Zulip Kyle Miller (Sep 04 2020 at 17:44):

I guess it wouldn't work to generalize every theorem/definition, because some rely on sets forming a lattice.

There are some big problems with this proposal, but I'm still curious about whether an attribute is able to do this kind of metaprogramming.

view this post on Zulip Reid Barton (Sep 04 2020 at 17:48):

I've also wondered whether there really needs to be a type class, or whether we could do some even more ad hoc thing like

notation a `` b := b.has a

and then rely on . notation to get what we want

view this post on Zulip Kyle Miller (Sep 04 2020 at 17:49):

Would that be like how :: is notation defined by vectors, multisets, lists, and others?

view this post on Zulip Kyle Miller (Sep 04 2020 at 17:50):

How does Lean disambiguate notation? It seems to do a reasonably good job at it, whatever it's doing.

view this post on Zulip Reid Barton (Sep 04 2020 at 18:01):

This is a different suggestion. More like duck typing.
The disadvantage is you could never abstract over a has_mem instance. But I could only find one such occurrence in the core library and mathlib, and it just relates and , which you could achieve anyways.

view this post on Zulip Adam Topaz (Sep 04 2020 at 18:01):

I understand that this opinion is controversial, but here is a related observation/question. Whenever we have two types X and Y with a has_mem X Y, you get a natural map from Y to set X given by sending y to {x : X | x \in y}. Is there any reasonable example where there is also a coercion from Y to set Xwhere these two are not defeq?

view this post on Zulip Reid Barton (Sep 04 2020 at 18:02):

I don't really understand how notation overloading works--it may appear to work well because the :: for multiset is used mostly in multiset.lean or whatever, which also defines it.

view this post on Zulip Kevin Buzzard (Sep 04 2020 at 18:06):

I think that Patrick fought hard to get the exact opposite behaviour for filters: he wanted s \in F because he felt it looked much more natural than s \in F.sets. IIRC his argument was the same as mine -- it just looks more like what a mathematician would write. I don't know any examples where there's a coercion which isn't defeq.

view this post on Zulip Reid Barton (Sep 04 2020 at 18:08):

Kevin, everyone wants to write s \in F and g \in H, I think. The question is how to implement it so that Lean isn't so frequently baffled by the relationship between the type of a set and the type of its elements, and maybe also to be able to apply lemmas about \forall x \in s, ... for sets to things that are not sets, etc.

view this post on Zulip Adam Topaz (Sep 04 2020 at 18:11):

import ring_theory.subring

notation a `∈₁` b := a  (b : set _)

variables (R : Type*) [ring R] (S : subring R) (r : R)

#check (r ∈₁ S)

Unfortunately the uparrow appears in the goal window.

view this post on Zulip Kyle Miller (Sep 04 2020 at 18:12):

@Adam Topaz That natural map is the has_mem_to_set that I wrote, though I used set_of rather than set builder notation for some reason. (The answer to your question ought to be "no," I'd hope!)

view this post on Zulip Kyle Miller (Sep 04 2020 at 18:14):

Reid Barton said:

I don't really understand how notation overloading works--it may appear to work well because the :: for multiset is used mostly in multiset.lean or whatever, which also defines it.

I was adding :: to data.sym, and some theorems involved :: for multisets, vectors, and lists, so I was impressed the overloading just worked.

view this post on Zulip Reid Barton (Sep 04 2020 at 18:15):

For example Lean doesn't understand what it should do with lemma h (s : set ℕ) : ∀ x ∈ s, x ∈ set.univ := sorry, but it works if you add local notation x ` ∈ ` s := @has_mem.mem _ _ set.has_mem x s. It's pretty frustrating because attaching a predicate _ ∈ t to some object t is exactly what it means to coerce t to a set!

view this post on Zulip Kyle Miller (Sep 04 2020 at 18:25):

Regarding @Adam Topaz's point, would it break anything to remove all has_coe _ (set _) instances and replace them all with the following single instance?

instance {α : Type*} {β : Type*} [has_mem α β] : has_coe β (set α) := ⟨λ s, {x | x  s}

Then to define a coercion, you implement has_mem.

view this post on Zulip Adam Topaz (Sep 04 2020 at 18:26):

Kyle Miller said:

Regarding Adam Topaz's point, would it break anything to remove all has_coe _ (set _) instances and replace them all with the following single instance?

instance {α : Type*} {β : Type*} [has_mem α β] : has_coe β (set α) := ⟨λ s, {x | x  s}

Then to define a coercion, you implement has_mem.

I'm fine with that too. I'm mostly asking for consistency.

view this post on Zulip Kyle Miller (Sep 04 2020 at 18:28):

Oh right, I forgot you were suggesting the other way. Here's that one, too, for completeness:

instance has_mem_from_coe {α : Type*} {β : Type*} [has_coe β (set α)] : has_mem α β :=
⟨λ x s, x  (s : set α)

view this post on Zulip Kyle Miller (Sep 04 2020 at 18:31):

Though at that point, it may as well be something like

infix `  ` := set.mem

abbreviation mem {α : Type*} {β : Type*} [has_coe β (set α)] (x : α) (s : β) :=
x  (s : set α)

infix `  ` := mem

removing has_mem entirely.

view this post on Zulip Gabriel Ebner (Sep 04 2020 at 20:36):

Kyle Miller said:

instance {α : Type*} {β : Type*} [has_mem α β] : has_coe_t β (set α) := ⟨λ s, {x | x  s}

This must be has_coe_t, or otherwise it would loop.

view this post on Zulip Scott Morrison (Sep 14 2020 at 02:59):

I spent a little while investigation dropping has_mem in favour of the coercion. Unfortunately the place it fails down is when you want to write a \mem s ++ t, say for s t : list X. Then Lean coerces the RHS to a set, and can no longer find ++.

view this post on Zulip Kyle Miller (Sep 14 2020 at 07:27):

Is there a way to "lock" a typeclass so only a fixed set of instances are allowed? (Community agreement counts :smile:) If so, then this could work to effectively drop has_mem:

universes u v

namespace new_has_mem

class has_mem (α : out_param $ Type u) (γ : Type v) := (mem : α  γ  Prop)

local infix         := has_mem.mem

instance {α : Type u} : has_mem α (set α) := set.mem
instance coe_has_mem {α : Type u} {β : Type v} [has_coe β (set α)] : has_mem α β :=
⟨λ x s, set.mem x s

-- then no other instances to has_mem ever!

@[simp] lemma mem_coe_eq {α : Type u} {β : Type v} [has_coe β (set α)] (x : α) (y : β) :
  x  (y : set α)  x  y := by refl

instance {α : Type*} : has_coe (list α) (set α) :=
⟨λ l, {x | l.mem x}

example (a b : list ) (n : ) (h : n  a) : n  a ++ b := sorry

example (a : list ) (h :  n  a,  m  a, n + 1  m) : a.empty := sorry

example (s : set ) (h :  n  s, n < 2) :  n  s, n < 3 := sorry

end new_has_mem

It turns out what I'd tried with infix before didn't work at all. I'd hoped it would make Lean prefer set.mem for sets, but it just caused it to not be able to disambiguate the notation. The above does effectively the same thing, but actually works. set.mem should have higher priority than the coercion (and if it's only working right now because there's no coersion from a set to a set, the priority could be set explicitly).

view this post on Zulip Kyle Miller (Sep 14 2020 at 07:28):

I'm not saying I'm in favor of dropping has_mem. It seems a bit nicer to me to keep has_mem but then replace all coercions to set with a single coercion that uses has_mem to implement it.

view this post on Zulip Anne Baanen (Sep 14 2020 at 09:49):

That is an interesting approach! It does not infer {y, z} : set ℕ in example (x y z : ℕ) : x ∈ {y, z} := sorry, which ideally I was hoping for. The current has_mem has the same issue though. So it looks like the coe_has_mem approach works at least as well as the current has_mem.


Last updated: May 17 2021 at 15:13 UTC