Zulip Chat Archive

Stream: new members

Topic: Subset comprehension


view this post on Zulip Paul Rowe (Mar 01 2021 at 22:10):

I'm trying to define the following function

def wp_set (P : Program) (S : State P) (w : WP) : set IDGA := sorry

I'd like to use set comprehension of the form:

{n  S.A | wpt d = some w}

where d : Defines P.D n. My structure S comes equipped with

S.a_def :  {I : IDGA}, I  S.A  Defines P.D I

so I'd like to make the set comprehension become

{n  S.A | wpt (S.a_def h) = some w}

where h records the fact that I have chosen n so that n ∈ S.A, but I the context doesn't contain any term h : n ∈ S.A.
Is there any way to restructure this set comprehension so that I can get such an h?

view this post on Zulip Yakov Pechersky (Mar 01 2021 at 22:13):

Do you really want set IDGA, which is the type of sets of IDGA, or perhaps the subtype of IDGA, where each term of the subtype satisfies wpt d = some w?

view this post on Zulip Paul Rowe (Mar 01 2021 at 22:16):

Well, I plan on taking intersections and set differences later, so I had envisioned using sets. But I'm open to seeing a solution that gives a subtype of IDGA if it's really easier here.

view this post on Zulip Eric Wieser (Mar 01 2021 at 22:21):

Does lean even allow \in on the left of | in a set comprehension (docs#has_sep)?

view this post on Zulip Eric Wieser (Mar 01 2021 at 22:24):

Huh, I guess it does. I've never seen that before!

view this post on Zulip Paul Rowe (Mar 01 2021 at 22:24):

I've use \in on the left in other parts of my project with no problem. I also tried moving it to the right of | at some point to see if that helped, but it still doesn't help me access any term h : n \in S.A. That is, I tried

{n | n  S.A \and  wpt (S.a_def h) = some w}

view this post on Zulip Yakov Pechersky (Mar 01 2021 at 22:24):

Yes, it does. Here, you need a Union:

variables (s : set ) (f :  n : , n  s  set )

#check  n (h : n  s), f n h

view this post on Zulip Yakov Pechersky (Mar 01 2021 at 22:25):

You could also do:

view this post on Zulip Yakov Pechersky (Mar 01 2021 at 22:25):

variables (s : set ) (f :  n : , n  s  set ) (g :  n : , n  s  Prop)

#check {n |  (h : n  s), g n h}

view this post on Zulip Paul Rowe (Mar 01 2021 at 22:27):

Interesting. I'll give that a try.

view this post on Zulip Paul Rowe (Mar 01 2021 at 22:35):

Ok, so the second option definitely type checks. I used

{ n |  (h : n  S.A), wpt (S.a_def h) = some w }

I'm somewhat worried about the existential though, because that might cause problems with computability down the line. So I'll try the first solutions as well.

view this post on Zulip Eric Wieser (Mar 01 2021 at 22:37):

(deleted)

view this post on Zulip Eric Wieser (Mar 01 2021 at 22:38):

Existentials with a hypothesis in their binder shouldn't affect computability

view this post on Zulip Eric Wieser (Mar 01 2021 at 22:39):

It's only when the binder/witness is in Type that that becomes a problem; Exist.rec is happy to eliminate into Prop without invoking choice.

view this post on Zulip Paul Rowe (Mar 01 2021 at 22:45):

Right. I had trouble when I knew something existed (even when I knew it was unique) and I was trying to use that fact to instantiate a term in a function. Since, as you say, it's being used in a hypothesis, I should be ok here.

I have a hard time anticipating where my mathematical intuition breaks down in the face of computability!

Thanks to both of you for your help!


Last updated: May 08 2021 at 09:11 UTC