Subset comprehension

Stream: new members

[Paul Rowe]

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]

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]

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]

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

[Eric Wieser]

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

[Paul Rowe]

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]

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]

You could also do:

[Yakov Pechersky]

variables (s : set ℕ) (f : ∀ n : ℕ, n ∈ s → set ℕ) (g : ∀ n : ℕ, n ∈ s → Prop)

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

[Paul Rowe]

Interesting. I'll give that a try.

[Paul Rowe]

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.

[Eric Wieser]

(deleted)

[Eric Wieser]

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

[Eric Wieser]

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]

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!