Julin Shaji (Apr 02 2024 at 05:44): 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.
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)
Julin Shaji (Apr 03 2024 at 06:08):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: Oct 13 2024 at 01:02 UTC