has_mem for subtype

Stream: Is there code for X?

[Adam Topaz]

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]

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

[Adam Topaz]

I want an instance of has_mem for subsets of a subtype

[Adam Topaz]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

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]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Adam Topaz]

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

[Kevin Buzzard]

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

[Adam Topaz]

It's easy to do once you have has_mem

[Kevin Buzzard]

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

[Adam Topaz]

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

[Adam Topaz]

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

[Kevin Buzzard]

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]

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]

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