Ssreflect Users Discussion List

[BEGAY Pierre-leo <>]

Hello Georges,

After Florent reassured me, I went back to my use case, and it now  
happens that the set0 \notin P condition is rather contradictory with  
what I have in mind. I had already proved what I needed with a  
slightly weaker notion of partition, and using the "classical"  
SSReflect definition will prove more painful than satisfactory, so  
I'll just stick with my former version.

Sorry for all the fuss over a silly mistake, and thanks.
Pierre-Léo

Georges Gonthier 
<>
 a écrit :

> Hi Pierre-Léo,
> You should be able to use partition and trivIset for your purposes;  
> in particular the trivIsetP lemma says trivIset means “pairwise  
> disjoint”.
>    Do note that as P : {set A}, P is by construction duplicate free.  
> Indeed you have [set [set: A]; setT] = [set setT] - by lemma setUid.
>    Cheers,
> Georges
>
> Envoyé de mon iPhone
>
> > Le 16 déc. 2019 à 16:12, BEGAY Pierre-leo 
> > <>
> >  a écrit :
> >
> > 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