Stream: new members

Topic: Difference between set and subtype

bottine (Jan 27 2022 at 08:28):

Hey! I'm struggling to understand the difference between sets and subtypes, and when should one be used instead of the other. I understand the type theoretic notion of considering a sigma type, and that if the dependent part is a proposition, then there is essentially no further information from an element lying in the sigma type, but I fail to understand the subtleties going on here. (Also, not sure what's the threshold for simple questions being considered "spam", so tell me before I reach it)

Yaël Dillies (Jan 27 2022 at 08:43):

One easy answer is you can take unions and intersections of sets, but you can't do that with subtypes. THe other way around, a set can always be coerced to the corresponding subtype.

Riccardo Brasca (Jan 27 2022 at 08:47):

I would say that the one of the main differences is that is S : set α and x ∈ S, then x is of type α. This is not true for subtypes. For example, if S = {n : ℝ | 0 ≤ n}, then (3 : ℝ) ∈ S as expected, but if you use S = {n : ℝ // 0 ≤ n} and take x : S, then x is not a real number, so you cannot use directly all the result you have for real numbers (you can of course coerc it to a real number, but this is sometimes a pain).

bottine (Jan 27 2022 at 08:47):

ah, mmh, yes, sets are all of a common type, hence the ability to have operations on them (that was RE Yaël's response)

Riccardo Brasca (Jan 27 2022 at 08:47):

Do you have a specific example where you don't know which one to use?

bottine (Jan 27 2022 at 08:49):

I have an example where I was wondering, but it's not really an important one (just trying to figure things out:)

variables {G : Type} [group G] {S : set G}

def signed (s : S) : bool → G
| tt := s
| ff := s⁻¹

def words (T : set G) := list (T × bool)

def val {T : set G} : words T → G
| [] := 1
| (⟨s , sgn⟩ :: tail) := (signed s sgn) * (val tail)

def words_for (T : set G) (g : G) : set (words T)
:= { w : (words T) | val w = g }
def geods_for (T : set G) (g : G) : set (words T)
:= { w ∈  (words_for T g) | ∀ u ∈ words_for T g, (length u) ≥ (length w) }


where I'm trying to define the word metric on a group.

Riccardo Brasca (Jan 27 2022 at 08:56):

I would say that s : S in the definition of signed is not a very good choice. s⁻¹ doesn't make sense, since the type of s (i.e. S) is not a group. Here probably Lean is smart enough to automatically insert the coercion for you, and s⁻¹ means "send s to G and then take the inverse", but if you start with (s : G) (hs : s ∈ S) this wouldn't be necessary.

Riccardo Brasca (Jan 27 2022 at 08:57):

But the best way is to try and see what happens.

Yaël Dillies (Jan 27 2022 at 08:58):

I mean, you can define signed on all of G, so why even bother mentioning S?

bottine (Jan 27 2022 at 08:59):

That's right, yes (though this snippet was just to show a place where I'm not sure of the best choice between subtype and set).

bottine (Jan 27 2022 at 08:59):

So, if I'm understanding the source right, subtype is really just a sigma type.

Riccardo Brasca (Jan 27 2022 at 09:00):

Here you are fixing a group G and working with its elements, so I suggest to take everything of type G, so using sets.

bottine (Jan 27 2022 at 09:01):

Now, when I do \forall x : subtype, I presumably have that x is a pair consisting of an element of the supertype, plus a proof of its satisfying the subtype-defining-predicate. What about \forall x \in set ?

bottine (Jan 27 2022 at 09:01):

Am I right that in the end, coercion and syntax sugar makes a lot of things look simpler than they are?

bottine (Jan 27 2022 at 09:05):

Also, what about the {{_}} notation?

Yaël Dillies (Jan 27 2022 at 09:08):

This is a semi implicit argument. It behaves like an explicit argument until you pass a later explicit argument, in which case it acts as an implicit one.

Yaël Dillies (Jan 27 2022 at 09:08):

Maybe looking at docs#monotone or docs#convex will make it make sense

bottine (Jan 27 2022 at 09:09):

OK, so nothing to do with sets/subtypes/membership… good to know

Last updated: Dec 20 2023 at 11:08 UTC