Multiset to set

Stream: Is there code for X?

[Anne Baanen]

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

[Adam Topaz]

You can always abuse the has_mem instance :)

[Adam Topaz]

I don't know how canonical that is.

[Anne Baanen]

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

[Adam Topaz]

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

[Anne Baanen]

Indeed.

[Anne Baanen]

I guess less inscrutability is another argument for to_finset.

[Adam Topaz]

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]

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]

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

[Kevin Buzzard]

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]

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

[Adam Topaz]

So why not use it?

[Adam Topaz]

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

[Reid Barton]

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]

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

[Adam Topaz]

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

[Reid Barton]

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

[Kyle Miller]

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]

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?

[Kyle Miller]

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]

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]

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

[Kyle Miller]

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

[Reid Barton]

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]

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]

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]

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]

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]

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]

@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]

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]

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]

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]

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]

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]

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]

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]

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]

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]

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]

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.