Ssreflect Users Discussion List

[BEGAY Pierre-leo <>]

Hello everyone,

I was trying to prove straightforward lemmas using hypotheses about  
partition, but did not find the "no overlapping" condition (trivIset)  
strong enough to do so. I looked at the definition of trivIset

Definition trivIset P := \sum_(B in P) #|B| == #|cover P|.

and I think that multiple occurrences of a set in P are not captured  
by the sum. This can be sort of checked with the following lemma, that  
- as far as I understand the usual definition of a set partition -  
should be false:

From mathcomp
Require Import ssreflect ssrbool eqtype seq ssrfun choice fintype
finset bigop.

(* setT can be partitioned into two copies of itself *)
Lemma partitionF {A : finType} (wit : A) :  partition [set [set: A];  
setT] setT.
Proof.
apply/and3P;split.
  (* cover *)
- rewrite eqEsubset. apply/andP;split;apply/subsetP;
  move=>x Hx. apply in_setT.
  apply/bigcupP. exists setT.
  by apply/set2P;left.
  apply Hx.
  (* trivIset *)
- apply/trivIsetP.
  by move=>x y /set2P [->|->] /set2P [->|->];
  unfold negb; rewrite eq_refl.
  (* set0 \notin *)
- apply/memPn.
  move=>x /set2P [->|->];
  apply/set0Pn; exists wit; apply in_setT.
Qed.

(tested in Coq 8.9.1 with mathcomp 1.8.0)

I was then wondering if this was the intended behavior of partition,  
or if maybe I was missing something.

Thank you in advance,
Pierre-Léo Bégay
PhD student at Orange Labs & Verimag