proposition: Lemma big_validP (xs : seq I) : reflect [/\ forall i, i \in xs -> valid (f i), forall i k, i \in xs -> k \in dom (f i) -> count_mem i xs = 1 & forall i j, i \in xs -> j \in xs -> i <> j -> valid (f i \+ f j)] (valid (\big[PCM.join/Unit]_(i <- xs) f i)).
proof: Proof. elim: xs=>[|x xs IH] /=; first by rewrite big_nil valid_unit; constructor. rewrite big_cons validUnAE. case H1 : (valid (f x))=>/=; last first. - by constructor; case=>/(_ x); rewrite inE eqxx H1=>/(_ erefl). rewrite andbC; case: allP=>/= H2; last first. - constructor; case=>H3 H4 H5; apply: H2=>k; rewrite big_domUn inE. case/andP=>V /hasP [y]; case : (x =P y)=>[<- /[swap]|N X D]. - by move/(H4 x); rewrite inE eqxx add1n=>/(_ erefl) []/count_memPn/negbTE ->. by apply: dom_inNR (H5 _ _ _ _ N) D; rewrite inE ?eqxx ?X ?orbT. case: {2 3}(valid _) / IH (erefl (valid (\big[PCM.join/Unit]_(j <- xs) f j))) => H V; constructor; last first. - case=>H3 H4 H5; apply: H; split; last 1 first. - by move=>i k X1 X2; apply: H5; rewrite inE ?X1 ?X2 orbT. - by move=>i X; apply: H3; rewrite inE X orbT. move=>i k X1 X2; move: (H4 i k); rewrite inE X1 orbT=>/(_ erefl X2). case: (x =P i) X1 X2=>[<-{i} X1 X2|]; last by rewrite add0n. by rewrite add1n; case=>/count_memPn; rewrite X1. case: H=>H3 H4 H5; split; first by move=>i; rewrite inE=>/orP [/eqP ->|/H3]. - move=>i k; rewrite inE eq_sym; case: (x =P i)=>[<- _|X] /= D; last first. - by rewrite add0n; apply: H4 D. rewrite add1n; congr (_.+1); apply/count_memPn. apply: contraL (D)=>X; apply: H2; rewrite big_domUn V inE. by apply/hasP; exists x. move=>i j; rewrite !inE=>/orP [/eqP ->{i}| Xi] /orP [/eqP ->{j}|Xj] // N. - rewrite validUnAE H1 H3 //=; apply/allP=>k D; apply: H2. by rewrite big_domUn V inE; apply/hasP; exists j. - rewrite validUnAE H3 ?H1 //=; apply/allP=>k; apply: contraL=>D; apply: H2. by rewrite big_domUn V inE; apply/hasP; exists i. by apply: H5 Xi Xj N. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)