## Stream: math-comp users

### Topic: Filter {set A+B} to get {set A}

#### Julin Shaji (Apr 02 2024 at 05:44):

Given a {set A+B} value, is there a way to filter it to get a value of type {set A}?

#### Julin Shaji (Apr 02 2024 at 05:49):

Kind of like this list version?

Fixpoint getLeft {A B: Type} (l: seq (A + B)): seq A :=
match l with
| [::] => [::]
| (inl a) :: l' => a :: getLeft l'
| _ :: l' => getLeft l'
end.


#### Julin Shaji (Apr 02 2024 at 05:49):

But since we can't do pattern match on sets, I wasn't sure how to go about this.

#### Julin Shaji (Apr 02 2024 at 05:51):

Tried like  [set x in ab | is_inl x].  but that's still {set A+B}.

#### Quentin VERMANDE (Apr 02 2024 at 11:28):

Mathematically, this would be the union, for x in ab, of \{a\} if x is inl a and \emptyset otherwise.
Nevertheless, if you know an element of A, it is probably better to filter the set (as you did) and map its element by sending inr _ to your distinguished element of A.

#### Cyril Cohen (Apr 02 2024 at 11:35):

Quentin's right, and you can also write it in one go: given X : {set A + B} you can probably write [set a | inl a \in X].

#### Cyril Cohen (Apr 02 2024 at 11:36):

also known as inl @^-1: X

#### Cyril Cohen (Apr 02 2024 at 11:36):

(the preimage of X by inl)

Thanks!

#### Julin Shaji (Apr 03 2024 at 06:22):

What does \{a\} mean? It's not latex stuff, is it?

#### Julin Shaji (Apr 03 2024 at 06:23):

if you know an element of A, it is probably better to filter the set (as you did) and map its element by sending inr _ to your distinguished element of A.

I didn't get this part. Why do we need to have a particular element of A?

#### Quentin VERMANDE (Apr 03 2024 at 07:01):

Ah, yes, sorry, it is indeed LaTeX stuff, you can ignore the backslashes, I meant the singleton containing a.
You would do your map with a function from A+B to A. This function does not know that your set contains only elements of the form inl _, so you need to define where to send inputs of the form inr _, hence the distinguished element of A.

Last updated: Jul 23 2024 at 20:01 UTC