## Stream: Is there code for X?

### Topic: Multiset to set

#### 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?

#### Adam Topaz (Sep 04 2020 at 16:16):

You can always abuse the has_mem instance :)

#### Adam Topaz (Sep 04 2020 at 16:16):

I don't know how canonical that is.

#### 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.

#### Adam Topaz (Sep 04 2020 at 16:22):

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

Indeed.

#### Anne Baanen (Sep 04 2020 at 16:24):

I guess less inscrutability is another argument for to_finset.

#### 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.

#### 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.

#### Adam Topaz (Sep 04 2020 at 16:27):

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

#### 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.

#### Adam Topaz (Sep 04 2020 at 16:32):

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

#### Adam Topaz (Sep 04 2020 at 16:32):

So why not use it?

#### 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).

#### 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.

#### 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.

#### Adam Topaz (Sep 04 2020 at 16:41):

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

#### Reid Barton (Sep 04 2020 at 16:42):

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

#### 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?)

#### Kevin Buzzard (Sep 04 2020 at 17:39):

So why not use it?

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

#### 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.

#### 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

#### Kyle Miller (Sep 04 2020 at 17:49):

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

#### 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.

#### 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.

#### 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?

#### 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.

#### 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.

#### 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.

#### 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.

#### 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!)

#### 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.

#### 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!

#### 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.

#### 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.

#### 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 α)⟩


#### 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.

#### 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.

#### 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 ++.

#### 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).

#### 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.

#### 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