## Stream: math-comp users

### Topic: partitions

#### Christian Doczkal (Mar 03 2021 at 12:34):

I started formalizing a proof that relies extensively on partitions (with extra properties for the classes) and I'm finding the theory of partitions in mathcomp to be somewhat underdeveloped. Does anyone know a development where the theory of partitions is developed further? I'm talking about things like removing a class from a partition or trimming down a partition to a subset of its domain. Nothing too fancy (yet).

#### Assia Mahboubi (Mar 15 2021 at 08:15):

I guess what you are referring to as underdevelopped is the content available in finset?

#### Assia Mahboubi (Mar 15 2021 at 08:16):

I would have expected the "trimming down to a subset" operation to be doable.

#### Assia Mahboubi (Mar 15 2021 at 08:18):

But I have not worked with these for a while I have to say. Of course one pitfall is that everything in this librar happens on a `finType` but this does not seem to be the restriction you complain about, or is it?

#### Christian Doczkal (Mar 15 2021 at 09:28):

Yes, I was talking about what's in `finset`, and my use case is coloring finite graphs, so I'm totally fine with finite sets. What I was taking about are basic lemmas like:

``````Lemma partitionD1 S :  partition P D -> S \in P -> partition (P :\ S) (D :\: S).
Lemma partitionU1 S :  partition P D -> S != set0 -> [disjoint S & D] -> partition (S |: P) (S :|: D).
``````

I proved these, but I had to also prove the underlying lemmas on `trivIset` and `cover`. If there is no know place where these things have already been proved, then I should probably create a PR once things have stabilized.

#### Assia Mahboubi (Mar 15 2021 at 17:03):

From my own personal point of view, it is indeed worth a PR. But I might miss part of the landscape here.

#### Christian Doczkal (Mar 15 2021 at 17:24):

Well, these are just examples, another one would be to lift partitions along injections, as in:

``````imset_partition : forall (T : finType) (P : {set {set T}}) (D : {set T}) (T' : finType) (f : T -> T'),
injective f -> partition P D = partition [set [set f x | x in S] | S in P] [set f x | x in D]
``````

This also goes the other way, but then one needs the domain of the partition to be included in `codom f`, and I'm not sure I have the ideal statement yet. (That's what I meant with "once things have stabilized".)

Last updated: Jul 25 2024 at 16:02 UTC