Cardinality of Finite Enumerated Sets, |Set(a, b, ..., n)|

[wdcraft01]

trafficstars

The cardinality class Card(S), representing the cardinality of a set $S$, has a computation() equalityprover method that relies on a deduce_cardinality() method of the domain set $S$. Our enumerated set class Set() does not yet have such a deduce_cardinality() method and it could be nice to have that rectified, at least for simple cases of Set() objects.

In reviewing some of the previous work on the enumerated set Set() class, it seems there might be easy and not-so-obvious cases for a deduce_cardinality() method, some of the issues being:

1. The Set() class allows multiplicity of elements, but such multiplicity is an illusion, with any multi-set-appearing set actually being equivalent to its underlying non-repetition support set. For example, Set(one, two, three, one) will appear as $\{1, 2, 3, 1\}$ but is equivalent to the set $\{1, 2, 3\}$. The Set.reduction() method helps deal with this little idiosyncracy of the Set() class.
2. Sets of Literals, like $\{'a', 'b', '3'\}$, or sets of irreducibles, like $\{1, 2, 3\}$ should be straightforward.
3. Sets containing variables could be more challenging. For example consider the set $A = \{a, b, c\}$ for variables $a$, $b$, $c$. If we know nothing about $a$, $b$, $c$ except that they are "unassigned variables," it might not be clear what the cardinality of $A$ should be, if we think of cardinality as being a constant or conserved property of a set. If at some point one sets the variables to be $a = b = 1$ and $c = 2$, the set reduces to $\{1, 2\}$ with cardinality 2 instead of the "naive" cardinality of 3 we might have originally assigned.
4. ExprRanges are convenient for expressing set elements but can present their own challenges, with some cases like $\{1, 2, ..., 100\}$ seeming quite clear, and others like $\{i, i+1, ..., j-1, j\}$ being much less clear. In such cases it is tempting to use the underling ExprRange indexing variable to "count" the elements, but it's not clear that always produces valid or distinct elements of the set.
5. Related: some obvious theorems and related methods could be added. For example, I don't think we have an inclusion-exclusion principle theorem yet, nor Card() methods for working with cardinalities of unions and intersections.