Inverse `finset.product`

Stream: Is there code for X?

[Marcus Rossel]

finset.product takes two finsets and creates a finset of all tuples over them.
Is there an inverse to this? I.e. a function that takes a finset over tuples and splits it into two?

[Mario Carneiro]

what two?

[Mario Carneiro]

you could do finset.image prod.fst s

[Mario Carneiro]

If you want it to be an inverse to finset.product it's not possible though because finset.product s empty = empty so there is no first projection

[Marcus Rossel]

Mario Carneiro said:

what two?

Say we have {(1, A), (3, B), (3, C), (5, C)} I would want the output to be ({1, 3, 5}, {A, B, C}).

[Eric Wieser]

I think a better example of Mario's point is that {(1, A), (2, B)} --your_fun--> ({1, 2}, {A, B}) --finset.product--> {(1, A), (2, A), (1, B), (2, B)}

[Eric Wieser]

So the thing you're looking for cannot be a two-sided inverse

[Marcus Rossel]

I guess (s.image prod.fst, s.image prod.snd) would work, but it doesn't feel nice.

[Eric Wieser]

If #5829 goes in and appropriate follow-up PRs made, then that could be changed to be spelt finset.product.symm s, since that's a left-inverse to finset.product edit: that's not true, because finset.product is a function of two arguments, and that PR is about single-argument functions

[Reid Barton]

Marcus Rossel said:

I guess (s.image prod.fst, s.image prod.snd) would work, but it doesn't feel nice.

I don't understand what's not nice about this

[Mario Carneiro]

Actually my point is that it can't even be a one-sided inverse because s * empty = empty, so a function f satisfying f (s * t) = s doesn't exist

[Mario Carneiro]

The reverse inverse definitely doesn't work because not all sets are rectangles