FStar
FStar copied to clipboard
Added seq partition theory
This module contains utilities for sequence-based set partitions.
We call a sequence with no duplicates a set here;
We call a set of subsets of a given set s a partition, if and only if its set union contains all elements from the given set s (no matter their order), the parts have no intersections with each other, and the parts contain no duplicates as well (that is included in them being called subsets, but I'd rather make myself as clear as possible here).
We prove the natural (and intuitively obvious) fact that the sum of partition lengths must equal the length of the base set s.