Difference between set and subtype

Stream: new members

[bottine]

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]

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]

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]

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]

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

[bottine]

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]

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]

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

[Yaël Dillies]

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

[bottine]

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]

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

[Riccardo Brasca]

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]

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]

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

[bottine]

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

[Yaël Dillies]

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]

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

[bottine]

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