Zulip Chat Archive

Stream: new members

Topic: coercion from set of subtype to set


view this post on Zulip Jason KY. (May 26 2020 at 12:35):

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}

view this post on Zulip Reid Barton (May 26 2020 at 12:37):

In each example, you have two variables called x

view this post on Zulip Reid Barton (May 26 2020 at 12:38):

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

view this post on Zulip Jason KY. (May 26 2020 at 12:39):

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

view this post on Zulip Reid Barton (May 26 2020 at 12:41):

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

view this post on Zulip Jason KY. (May 26 2020 at 12:45):

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

view this post on Zulip Reid Barton (May 26 2020 at 12:46):

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

view this post on Zulip Reid Barton (May 26 2020 at 12:46):

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

view this post on Zulip Jason KY. (May 26 2020 at 12:48):

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}

view this post on Zulip Kenny Lau (May 26 2020 at 12:49):

  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

view this post on Zulip Jason KY. (May 26 2020 at 12:53):

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


Last updated: May 14 2021 at 23:14 UTC