## Stream: Is there code for X?

### Topic: has_mem for subtype

#### Adam Topaz (Jun 01 2020 at 15:29):

I'm not sure if this should go here, or in "new members"... is there a standard way of doing this? apply_instance didn't find anything.

instance foo (T : Type*) (S : set T) : has_mem T (set (subtype S)) := sorry


#### Kevin Buzzard (Jun 01 2020 at 15:29):

What are you trying to ask? This doesn't seem to make any sense.

#### Adam Topaz (Jun 01 2020 at 15:30):

I want an instance of has_mem for subsets of a subtype

#### Adam Topaz (Jun 01 2020 at 15:30):

I'm a bit surprised it doesn't exist in mathlib.

#### Kevin Buzzard (Jun 01 2020 at 15:30):

Oh I see, so if U : subtype S then you can imagine U as a subset of T.

#### Kevin Buzzard (Jun 01 2020 at 15:31):

You understand that there is some coercion happening when you write subtype S? S is a term, not a type.

#### Kevin Buzzard (Jun 01 2020 at 15:32):

You have disappeared into another topic, but I guess subtype S is a bit weird, because maybe if you wanted S to be a type you would have used a subtype of T instead of set T

#### Adam Topaz (Jun 01 2020 at 15:33):

I could get by with this too:

instance foo (T : Type*) (S : set T) : has_coe (set (subtype S)) (set T) := sorry


but apply_instance doesn't find anything for this either.

#### Adam Topaz (Jun 01 2020 at 15:34):

As you say, I just want to think of subsets of a subtype of T as subsets of T.

#### Kevin Buzzard (Jun 01 2020 at 15:34):

I see. Most of what I said was nonsense, sorry (I'd forgotten what subtype did).

#### Kevin Buzzard (Jun 01 2020 at 15:35):

Yeah, I agree that this looks like it could be a thing.

#### Kevin Buzzard (Jun 01 2020 at 15:37):

instance foo (T : Type*) (S : set T) : has_mem T (set (subtype S)) := ⟨λ t U, t ∈ subtype.val '' U⟩


#### Kevin Buzzard (Jun 01 2020 at 15:38):

instance bar (T : Type*) (S : set T) : has_coe (subtype S) T := by apply_instance exists

#### Kevin Buzzard (Jun 01 2020 at 15:40):

but you can't coerce from set (subtype S) to set T because these are terms, not types.

#### Adam Topaz (Jun 01 2020 at 15:41):

I thought set T is the type of subsets of T, no?

#### Kevin Buzzard (Jun 01 2020 at 15:41):

Oh yeah you're right again, so there could be a coercion

#### Adam Topaz (Jun 01 2020 at 15:41):

It's easy to do once you have has_mem

#### Kevin Buzzard (Jun 01 2020 at 15:41):

I haven't done any Lean for a few days, I need to warm up :-)

#### Adam Topaz (Jun 01 2020 at 15:42):

instance foo2 (T : Type*) (S : set T) : has_coe (set (subtype S)) (set T) :=
⟨ λ U t, t ∈ U ⟩


#### Adam Topaz (Jun 01 2020 at 15:43):

I wasn't familiar with the '' notation, though. Thanks for that!

#### Kevin Buzzard (Jun 01 2020 at 15:44):

or instance (T : Type*) (S : set T) : has_coe (set (subtype S)) (set T) := ⟨λ U t, t ∈ subtype.val '' U⟩ if the other instance isn't there. Yeah, at least I got the notation for set.image right :-)

#### Mario Carneiro (Jun 01 2020 at 21:37):

This instance is not okay, because set (subtype S) already has a has_mem, with subtype S on the left, and the left argument of has_mem is an out_param so there is only allowed to be one such instance.

#### Adam Topaz (Jun 02 2020 at 14:00):

Is this also an issue for the has_coe instance that Kevin mentioned?

Last updated: May 16 2021 at 05:21 UTC