Stream: math-comp users

Topic: partitions


view this post on Zulip 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).

view this post on Zulip Assia Mahboubi (Mar 15 2021 at 08:15):

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

view this post on Zulip Assia Mahboubi (Mar 15 2021 at 08:16):

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

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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: Feb 08 2023 at 08:02 UTC