## Stream: new members

### Topic: Subset comprehension

#### 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?

#### 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?

#### 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.

#### Eric Wieser (Mar 01 2021 at 22:21):

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

#### Eric Wieser (Mar 01 2021 at 22:24):

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

#### 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}


#### 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


#### Yakov Pechersky (Mar 01 2021 at 22:25):

You could also do:

#### 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}


#### Paul Rowe (Mar 01 2021 at 22:27):

Interesting. I'll give that a try.

#### 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.

(deleted)

#### Eric Wieser (Mar 01 2021 at 22:38):

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

#### 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.

#### 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