set notation

Stream: new members

[Patrick Thomas]

Could someone point me to or tell me what the underlying definition of {} is? For instance, the singleton set {x}. I haven't been able to find it in mathlib.

[Patrick Thomas]

Nevermind, I guess VIsual Code says it is singleton.

[Patrick Thomas]

Hmm, but then set.singleton uses the same notation.

[Bryan Gin-ge Chen]

(deleted, Pedro gave a better answer)

[Pedro Minicz]

{} is an empty "set comprehension," like {1, 2, 3} but with zero elements.

[Pedro Minicz]

Look at docs#is_lawful_singleton, it should give you an idea of what is happening behind the scenes.

[Patrick Thomas]

Is there any underlying definition somewhere for set comprehension?

[Patrick Thomas]

So it appears that a set is just a predicate?

[Pedro Minicz]

The notation {1, 2, 3} folds has_insert.insert with has_emptyc.emptyc.

[Pedro Minicz]

Yes, a set is just a predicate.

[Pedro Minicz]

{} is equal to ∅, which is equivalent to λ _, false.

[Pedro Minicz]

Pedro Minicz said:

The notation {1, 2, 3} folds has_insert.insert with has_emptyc.emptyc.

@Mario Carneiro is that correct? I can't seem to find a notation definition for `{` l:(foldr `, ` (x xs, insert x xs) ∅ `}`). Is it defined internally in C++?

[Patrick Thomas]

Does the following represent the proposition that a is a member of set s?

protected def mem (a : α) (s : set α) :=
s a

[Pedro Minicz]

Yes. Since sets are predicates (α → Prop) and a : α, s a : Prop, which is true or false depending on whether a "is in" s.

[Bryan Gin-ge Chen]

Pedro Minicz said:

I can't seem to find a notation definition for `{` l:(foldr `, ` (x xs, insert x xs) ∅ `}`). Is it defined internally in C++?

I think it's defined here: https://github.com/leanprover-community/lean/blob/master/src/frontends/lean/brackets.cpp

[Pedro Minicz]

Ah, yes, this looks like it.

[Patrick Thomas]

Would this be an equivalent definition: def singleton (α : Type) (a : α) (s : set α) := ∀ b : α, (set.mem b s) → b = a?

[Patrick Thomas]

Doesn't insert itself use the {} notation?

[Pedro Minicz]

set.insert uses { ... | ... } notation, which is different from {.., ..., ...}.

[Pedro Minicz]

set_option pp.notation false
#print set.insert -- λ {α : Type u} (a : α) (s : set α), set_of (λ (b : α), or (eq b a) (has_mem.mem b s))

If you disable notations when printing, you can see the definition of set.insert.

[Pedro Minicz]

Patrick Thomas said:

Would this be an equivalent definition: def singleton (α : Type) (a : α) (s : set α) := ∀ b : α, (set.mem b s) → b = a?

This is a predicate on sets. It says that the set s contains only one element.

[Pedro Minicz]

Sets are predicates on a type. Consider def singleton' (a : α) : set α := λ x, x = a, singleton' a is a set of α, that is, a predicate on α. While with your definition singleton a s says that s is a set that only contains a.

[Patrick Thomas]

That is what I was intending.

[Patrick Thomas]

That it was an equivalent definition to {a}.

[Patrick Thomas]

Wait, are you saying that singleton' is a set of alpha that only contains a?

[Pedro Minicz]

Yes, singleton' a is a set that only contains a.

[Patrick Thomas]

I guess I don't understand the difference between my def singleton (α : Type) (a : α) (s : set α) := ∀ b : α, (set.mem b s) → b = a and your def singleton' (a : α) : set α := λ x, x = a.

[Patrick Thomas]

Is it just that mine takes a set as a parameter?

[Pedro Minicz]

Observe the types of both definitions:

variable {α : Type}

def sing (a : α) (s : set α) : Prop :=
∀ b ∈ s, b = a

def sing' (a : α) : set α :=
-- Remember that `set α = α → Prop`.
λ b, a = b

variables (a : α) (s : set α)

#check sing a -- `set α → Prop`, that is, a predicate on `set α`.
#check sing' a -- `set α`, that is, a predicate on `α`.

[Patrick Thomas]

I see. Thank you.

[Pedro Minicz]

Your predicate talks about sets. It is true if and only if the set in question is a singleton set. My singleton' creates a set, that is, given an a : α it creates a predicate α → Prop.

[Patrick Thomas]

So...?

def union {α : Type} (s t : set α) : set α :=
λ x, (set.mem x s) ∨ (set.mem x t)

[Pedro Minicz]

Yes! That is exactly it!

[Patrick Thomas]

Cool. Thank you!

[Pedro Minicz]

I'd recommend using x ∈ s as it is a bit easier to read than set.mem.

[Patrick Thomas]

Ok.

[Pedro Minicz]

Also, since sets are predicates and predicates are functions, you can write λ x, s x ∨ t x to make what is happening under the hood explicit.

[Patrick Thomas]

Cool.

[Lúcás Meier]

So, I've seen that Lean has a kind of set notation: {a : nat | a >= 3} (modulo unicode syntax). Is this hard-coded into the language, or could you define a similar kind of notation for other things?

[Patrick Massot]

It's hardcoded.

[Mario Carneiro]

but you can define similar notation, as long as you don't start with {

[Alex Zhang]

Does lean recognise any kind of "dot notation" for sets?
def S (n: ℕ) :set ℕ:= {1,2,...,n}

[Kyle Miller]

@Alex Zhang No, not as far as I've seen. That set happens to be called set.Icc 1 n, though.

def S (n : ℕ) : set ℕ := {i | 1 ≤ i ∧ i ≤ n}
def S' (n : ℕ) : set ℕ := set.Icc 1 n
def S'' (n : ℕ) : set ℕ := (λ (i : fin n), (i : ℕ) + 1) '' set.univ

[Alex Zhang]

If I have a finite field F with card p (odd and large) say,
then is it possible to define a set to be say {0 , 1, ... (p-1)/2} :set F?

[Alex Zhang]

by defining to be the image of some function perhaps? any convenient way?

[Kyle Miller]

@Alex Zhang There's a natural map from natural numbers to a ring, which is given as a coercion instance, and you can take the image of set.Icc:

def S {F : Type*} [field F] (n : ℕ) : set F := coe '' set.Icc 0 n

It's up to you to pass in the upper bound you want.

[Kyle Miller]

More generally,

def S {R : Type*} [ring R] (n : ℕ) : set R := coe '' set.Icc 0 n

[Alex Zhang]

Very helpful, Kyle!

[Yakov Pechersky]

Will you be taking sums over these? There is also finset.Ico, and soon we will also have finset.Icc and all the other variants.