Set of pairs, with and without repetitions

Question

I have two sets:

X = {a, b}
Y = {1, 2, 3}

I would like to generate the following set of sets of pairs:

{<<a, 1>>, <<a, 2>>, <<a, 3>>}
{<<a, 1>>, <<a, 2>>, <<b, 3>>}
{<<a, 1>>, <<b, 2>>, <<a, 3>>}
{<<a, 1>>, <<b, 2>>, <<b, 3>>}
...
{<<b, 1>>, <<b, 2>>, <<b, 3>>}

In each set the first element is from X and the second is from Y. X can be repeated, Y cannot. How to do it?

Answer 1

Using the \X operator gives us the set of all pairs: X \X Y = {<<a, 1>>, <<a, 2>>, ... <<b, 3>>}. SUBSET (X \X Y) gives us all possible sets. {s \in SUBSET (X \X Y): Cardinality(s) = 3} (from the FiniteSets module) gives us all 3-element sets.

We want to make this unique on the second element of each pair. Let's define a new operator:

UniqueBy(set, Op(_)) == Cardinality(set) = Cardinality({Op(s): s \in set})

If we do {x[2] : x \in {<<a, 1>>, <<a, 2>>, <<a, 2>>}}, we get {1, 2}, which has a smaller cardinality and will be filtered out. So our final expression is

{s \in SUBSET (X \X Y) : UniqueBy(s, LAMBDA x: x[2]) /\ Cardinality(s) = 3}

Note that without the cardinality check {<<a, 1>>} would be part of the set of sets, which isn't what you're looking for.

Answer 2

EXTENDS Functions, FiniteSets, Naturals

CONSTANTS a, b

X == {a, b}
Y == {1, 2, 3}

Dom == 1..Cardinality(Y)

Slice == {{<< xt[n], yt[n] >>:  n \in Dom}:
              << xt, yt >> \in [Dom -> X] \X Bijection(Dom, Y)}

The TLAPS distribution includes the module Functions. The modules FiniteSets and Naturals are part of the standard library of TLA+.