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: Mar 29 2024 at 12:02 UTC