coercion from set of subtype to set

Stream: new members

[Jason KY.]

I am trying to create a coercion from a set of subtype A to set and I somehow got it to work but I don't understand why it does work :/
Here is my #mwe

variables {X : Type*}

instance {A : set X} : has_coe (set (subtype A)) (set X) :=
⟨λ U, {x | ∀ x : subtype A, x ∈ U}⟩

If I hover over x in vs code, it says x : X but I would expect x to have type subtype A.

On the other hand I would expect the following code to work since I would think x.1 will have type X but it doesn't seem to be the case.

variables {X : Type*}

instance {A : set X} : has_coe (set (subtype A)) (set X) :=
⟨λ U, {x.1 | ∀ x : subtype A, x ∈ U}⟩

[Reid Barton]

In each example, you have two variables called x

[Reid Barton]

{x | already binds x, which I think you were trying to achieve again with the forall. For example {x | x >= 0} makes sense.

[Jason KY.]

Something like this? ⟨λ U, {x.1 | x : subtype A, x ∈ U}⟩

[Reid Barton]

You can only put a variable before the |, not an expression

[Jason KY.]

I don't think I understand how to extract the value of x : subtype A, i.e. get something of type X from x.

instance {A : set X} : has_coe (set (subtype A)) (set X) :=
⟨λ U, {y | ∃ x ∈ U, x.1 = y}⟩

I thought the above should work but its complaining invalid field notation

[Reid Barton]

I think that's because Lean is dense about inference involving ∈? Otherwise it looks correct to me

[Reid Barton]

The error message is probably telling you that Lean doesn't know x is a subtype A

[Jason KY.]

Vs code says it's of type subtype A when I hover over it so it's very strange lean doesn't know.
I got it to work by adding it though :)

variables {X : Type*}

instance {A : set X} : has_coe (set (subtype A)) (set X) :=
⟨λ U, {y | ∃ (x : subtype A) (H : x ∈ U), x.val = y}⟩

[Kenny Lau]

1. subtype A isn't idiomatic. just use coercion
   2.

import data.set.basic

variables {X : Type*}

instance {A : set X} : has_coe (set A) (set X) :=
⟨λ S, subtype.val '' S⟩

[Jason KY.]

Wow, I did not expect lean would convert set X to Type* (which is what I needed) so easily. Nice!