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).

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

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

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?

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.

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

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