proposition: Lemma separation_decomp (G:sgraph) (V1 V2 : {set G}) T1 T2 B1 B2 : @sdecomp T1 (induced V1) B1 -> @sdecomp T2 (induced V2) B2 -> separation V1 V2 -> clique (V1 :&: V2) -> exists T B, @sdecomp T G B /\ width B <= maxn (width B1) (width B2).
proof: Proof. move => dec1 dec2 sepV clV. have dec12 := join_decomp dec1 dec2. set G' := sjoin _ _ in dec12. set T := tjoin T1 T2 in dec12. set B : tjoin T1 T2 -> {set G'}:= decompU B1 B2 in dec12. pose h (x : G') : G := match x with inl x => val x | inr x => val x end. case: (boolP (0 < #|V1 :&: V2|)) => [cliquen0|clique0]. - case/card_gt0P : cliquen0 => v0 /setIP [v01 v02]. have HVx (V : {set G}) : (V = V1) \/ V = V2 -> v0 \in V -> let V' := val @^-1: (V1 :&: V2) : {set induced V} in 0 < #|V'| /\ clique V'. { move => HV xV /=. split. - apply/card_gt0P; exists (Sub v0 xV). rewrite inE /=. case: HV => ?; by set_tac. - move => u v. rewrite [_:&:_]lock !inE -lock -val_eqE. exact: clV. } set S := V1 :&: V2 in HVx. pose S1 := val @^-1: S : {set induced V1}. pose S2 := val @^-1: S : {set induced V2}. have [cln01 clS1] : 0 < #|S1| /\ clique S1 by apply: HVx; auto. have [cln02 clS2] : 0 < #|S2| /\ clique S2 by apply: HVx; auto. case: (decomp_clique dec1 cln01 clS1) => t1 Ht1. case: (decomp_clique dec2 cln02 clS2) => t2 Ht2. have dis_t1_t2 : ~~ connect (@sedge T)(inl t1) (inr t2) by rewrite join_disc. set T' := Forest (add_edge_is_forest dis_t1_t2). have dec12' : sdecomp T' G' B. { apply: sdecomp_tree_subrel dec12. exact: subrelUl. } case/Wrap: (rename_decomp dec12' h). case/(_ _ _ _ _)/Wrap. + by move => [u|u] [v|v]. + move => v. case/setUP : (sepV.1 v) => Hv; apply/codomP; by [exists (inl (Sub v Hv))|exists (inr (Sub v Hv))]. + move => x y xy. suff: x \in V1 /\ y \in V1 \/ x \in V2 /\ y \in V2. { case => [[Hx Hy]|[Hx Hy]]. - by exists (inl (Sub x Hx)); exists (inl (Sub y Hy)). - by exists (inr (Sub x Hx)); exists (inr (Sub y Hy)). } case: (boolP (x \in V1));case: (boolP (y \in V1)) => Hy Hx; first [by left|right; apply/andP]. * rewrite [y \in _](sep_inR sepV) // andbT. apply: contraTT xy => H. by rewrite sepV. * rewrite [x \in _](sep_inR sepV) //=. apply: contraTT xy => H. by rewrite sgP sepV. * by rewrite !(sep_inR sepV). + case: dec1 => dec1A dec1B dec1C. case: dec2 => dec2A dec2B dec2C. have X (x : induced V1) (y : induced V2) : val x = val y -> ((inl x \in B (inl t1) = true) * (inr y \in B (inr t2) = true))%type. { move => Exy. rewrite /B /decompU /= !imset_f //. - apply: (subsetP Ht2). rewrite !inE -{1}Exy. apply/andP; split; exact: valP. - apply: (subsetP Ht1). rewrite !inE {2}Exy. apply/andP; split; exact: valP. } move => [x|x] [y|y]; simpl h. * move/val_inj => ?;subst y. case: (dec1A x) => t Ht. left. exists (inl t). by rewrite /B /decompU /= imset_f. * move => Exy. right. exists (inl t1). exists (inr t2). by rewrite /edge_rel/= !(X _ _ Exy) /= !eqxx. * move/esym => Eyx. right. exists (inr t2). exists (inl t1). by rewrite /edge_rel/= !(X _ _ Eyx) /= !eqxx. * move/val_inj => ?;subst y. case: (dec2A x) => t Ht. left. exists (inr t). by rewrite /B /decompU /= imset_f. + move => decRB. do 2 eexists. split. eapply decRB. apply: leq_trans (rename_width _ _) _. exact: join_width. - suff iso: diso G' G. + case: (decomp_iso dec12 iso) => B' sdecB' wB'B. exists T; exists B'. split => //. by rewrite wB'B join_width. + suff HH: V2 = ~:V1. { rewrite /G' HH. apply ssplit_disconnected. move => x y xV1 yNV1. rewrite (sepV.2 x y) => //. by rewrite HH inE xV1. } apply/setP => z. rewrite inE. case: (boolP (z \in V1)) => Hz. * apply: contraNF clique0 => H. apply/card_gt0P. exists z. by set_tac. * apply: contraTT (sepV.1 z). by set_tac. Qed.
imports: Coq(RelationClasses) mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph sgraph) GraphTheory(connectivity set_tac)