proposition: Lemma separation_K4side G (V1 V2 : {set G}) : separation V1 V2 -> clique (V1 :&: V2) -> #|V1 :&: V2| <= 2 -> minor G K4 -> exists2 phi : K4 -> {set G}, minor_rmap phi & (forall x, phi x \subset V1) \/ (forall x, phi x \subset V2).
proof: Proof. move => sepV clV12 cardV12 /minorRE [phi] [P1 P2 P3 P4]. wlog/forallP cutV1 : V1 V2 sepV clV12 cardV12 / [forall x, phi x :&: V1 != set0]. { move => W. case: (boolP [forall x, phi x :&: V1 != set0]) => A; first exact: (W V1 V2). case: (boolP [forall x, phi x :&: V2 != set0]) => B. { setoid_rewrite <- or_comm. by apply: W; rewrite 1?setIC // separation_sym. } case: notF. case/forallPn : A => i /negPn Hi. case/forallPn : B => j /negPn Hj. case: (altP (i =P j)) => [E|E]. - subst j. case/set0Pn : (P1 i) => x Hx. case/setUP : (sepV.1 x) => Hx'. + move/eqP/setP/(_ x) : Hi. by rewrite !inE Hx Hx'. + move/eqP/setP/(_ x) : Hj. by rewrite !inE Hx Hx'. - move/neighborP : (P4 i j E) => [x] [y] [A B]. rewrite sgP sepV //. apply: contraTN Hj => Hy. by apply/set0Pn; exists y; rewrite inE B. apply: contraTN Hi => Hx. by apply/set0Pn; exists x; rewrite inE A. } set S := V1 :&: V2 in clV12 cardV12. have phiP i y : y \in phi i -> y \notin V1 -> phi i :&: S != set0. { case/set0Pn : (cutV1 i) => x /setIP [xpi xV1 ypi yV1]. case: (boolP (x \in V2)) => xV2; first by apply/set0Pn; exists x; rewrite !inE. case/connect_irredRP : (P2 i x y xpi ypi); first by apply: contraNneq yV1 => <-. move => p Ip subP. have [_ _ /(_ p)] := separation_separates sepV xV2 yV1. case => z /(subsetP subP) => ? ?. apply/set0Pn; exists z. by rewrite /S inD. } pose phi' (i : K4) := phi i :&: V1. exists phi'; first split. - move => i. exact:cutV1. - move => i. apply connectedI_clique with S => //. + move => x y p sub_phi Hx Hy. case: (boolP (x \in V2)) => Hx'. * exists x => //. by rewrite /S inD. * have [_ _ /(_ p) [z ? ?]] := (separation_separates sepV Hx' Hy). exists z => //. by rewrite /S inD. - move => i j /P3 => D. apply: disjointW D; exact: subsetIl. - move => i j ij. move/P4/neighborP : (ij) => [x] [y] [H1 H2 H3]. have S_link u v : u \in S -> v \in S -> u \in phi i -> v \in phi j -> u -- v. { have D: [disjoint phi i & phi j] by apply: P3; rewrite sg_edgeNeq. move => H *. apply: clV12 => //. by apply: contraTneq H => ?; set_tac. } have/subsetP subV : S \subset V1 by exact: subsetIl. have inS u v : u -- v -> u \in V1 -> v \notin V1 -> u \in S. { move => uv HVu HVv. apply: contraTT uv => /= C. subst S. by rewrite sepV // notinD. } apply/neighborP. case: (boolP (x \in V1)) => HVx; case: (boolP (y \in V1)) => HVy. + exists x; exists y. by rewrite !inE HVx HVy. + case/set0Pn : (phiP _ _ H2 HVy) => s /setIP [S1 S2]. exists x; exists s. rewrite !inE H1 HVx S1 S_link // ?subV //. exact: inS HVy. + case/set0Pn : (phiP _ _ H1 HVx) => s /setIP [S1 S2]. exists s; exists y. rewrite !inE H2 HVy S1 S_link // ?subV //. apply: inS HVx => //. by rewrite sgP. + case/set0Pn : (phiP _ _ H1 HVx) => s /setIP [S1 S2]. case/set0Pn : (phiP _ _ H2 HVy) => s' /setIP [S3 S4]. exists s; exists s'. by rewrite !inE S1 S3 S_link // !subV. - left => x. exact: subsetIr. Qed.
imports: Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries set_tac digraph) GraphTheory(sgraph treewidth minor connectivity)