proposition: Proposition contract_three_connected (G : sgraph) : 5 <= #|G| -> 3.-connected G -> exists x y, x -- y /\ 3.-connected (smerge2 G x y).
proof: Proof. move=> le5G connG. suff : ~ forall x y, x -- y -> ~ 3.-connected (smerge2 G x y). { move => A. setoid_rewrite (rwP (kconnectedP _ _)). setoid_rewrite (rwP andP). do 2 setoid_rewrite (rwP existsP). apply: contra_notT A => C x y xy. apply: contraNnot C => H. apply/existsP;exists x; apply/exists_inP;exists y => //. exact/kconnectedP. } move => not3xy. pose cmp3 (x y z : G) F := [/\ x -- y, vseparator [set x;y;z], connected F & [disjoint F & [set x;y;z]]]. have [x [y [z [F [[xy sepF connF disjF] max_xyF]]]]] : exists (x y z : G) (F : {set G}), cmp3 x y z F /\ forall x' y' z' F', cmp3 x' y' z' F' -> #|F'| <= #|F|. { pose p := [pred xyz : G * G * G | let: ((x,y),z) := xyz in x -- y && vseparatorb [set x;y;z]]. have [xyz0 p_xyz0] : exists xyz , p xyz. { have [x[y xy]] := kconnected_edge connG. have [z Hz] := edge_separator le5G connG xy (not3xy _ _ xy). by exists ((x,y),z); rewrite /= xy /= Hz. } pose p' (xyz : G * G * G) := [pred A | let: ((x,y),z) := xyz in connectedb A && [disjoint A & [set x;y; z]]]. pose mcmp (xyz : G * G * G) : nat := \max_(A | p' xyz A) #|A|. pose xyz := arg_max xyz0 p mcmp. have inh_p' (xyz' : G * G * G) : p' xyz' set0. { case: xyz' => -[x y] z /=; rewrite disjoints0 ?andbT. exact/connectedP/connected0. } pose F : {set G} := arg_max set0 (p' xyz) (fun x => #|x|). pose x := xyz.1.1; pose y := xyz.1.2; pose z := xyz.2. exists x, y,z, F. revert xyz F x y z. case: arg_maxnP => // -[[x y] z] /= /andP [P1 P2] max_xyz. case: arg_maxnP => // F /= /andP [/connectedP connF disF] maxF. split; first by split => //; exact/vseparatorP. move => x' y' z' F' [F1 /vseparatorP F2 /connectedP F3 F4]. have:= max_xyz (x',y',z'); rewrite F1 F2 => /(_ isT) le_mcp. apply: (@leq_trans (mcmp (x,y,z))). - apply: leq_trans le_mcp. by apply: leq_bigmax_cond => /=; rewrite F3. - by apply/bigmax_leqP => A; apply: maxF. } have [_ min3sep] := connG. pose H := [set x; y] :|: F. have min_xyz : smallest vseparator [set x;y;z]. { split => // V /min3sep. apply: leq_trans. exact: cards3. } move defXYZ : [set x;y;z] => XYZ. have /set0Pn[f f_F] : F != set0. { apply: contraTneq le5G => eqF0; rewrite -leqNgt. suff /subset_leq_card S : G \subset [set x;y;z]. by apply: leq_trans S _; rewrite leqW // cards3. apply: wlog_neg => /subsetPn [u _ Hu]. have:= max_xyF x y z [set u]; rewrite cards1 eqF0 cards0 ltnn. case/(_ _)/Wrap => //; split; rewrite ?disjoints1 //. exact: connected1. } have compF : {in F & ~: F, forall u v, u -- v -> v \in XYZ}. { move=> u v u_F; rewrite !inE -defXYZ => vNF uv. apply/negPn/negP => vXYZ. suff/max_xyF : cmp3 x y z (v |: F). by rewrite leqNgt cardsU1 vNF add1n leqnn. split => //; last by rewrite disjointsU // disjoints1. rewrite setUC; apply: connectedU_edge uv _ _ => //; last exact: connected1. by rewrite !inE eqxx. } have psepH : proper_separation (F :|: XYZ) (~: F :|: XYZ). { rewrite defXYZ in min_xyz disjF. exact: component_separation min_xyz f_F disjF connF compF. } have [u zu uNH] : exists2 u, z -- u & u \notin H. { rewrite defXYZ in min_xyz. have := @svseparator_neighbours _ _ _ z psepH. rewrite setUUC -{2}defXYZ !inE eqxx; case => // u [v] [_ Hz _ zv]. exists v => //. apply: contraNN Hz => {zv}. apply/subsetP : v. by rewrite /H setUC setUS // -defXYZ subsetUl. } have/andP [xDz yDz] : (x != z) && (y != z). { move/min3sep : sepF. rewrite -setUA !cardsU1 cards1 !inE (sg_edgeNeq xy) /=. by do 2 case: (_ == _). } have zNF : z \in F = false by rewrite (disjointFl disjF) // !inE eqxx. have zNH : z \notin H by rewrite !inE ![z == _]eq_sym !negb_or xDz yDz zNF. have x_H : x \in H by rewrite !inE eqxx. suff connH w : connected (H :\ w). { have [v /vseparatorP V2] := edge_separator le5G connG zu (not3xy _ _ zu). pose F' := H :\ v. have cmp3_F : cmp3 z u v F'. { split => //; first exact: connH; rewrite disjoint_sym disjoint_subset. apply/subsetP => i; rewrite !inE -orbA => /or3P[] /eqP->. - by rewrite ![z == _]eq_sym (negbTE xDz) (negbTE yDz) zNF. - by move: uNH; rewrite !inE => /negbTE ->. - by rewrite eqxx. } have:= max_xyF z u v F' cmp3_F. rewrite /F'/H -setUA => X; have {X} := leq_trans (leq_cardsD1 _ _) X. rewrite !cardsU1 !inE sg_edgeNeq //= !(disjointFl disjF) ?add1n ?ltnn //. all: by rewrite !inE eqxx. } case: (boolP (w \in [set x; y])) => [w_xy|]. { case/set2P : w_xy => ->. - have -> : H :\ x = F :|: [set y]. apply/setP => i; rewrite setUC !inE. case: (eqVneq i x) => // ->. by rewrite (sg_edgeNeq xy) /= (disjointFl disjF) // !inE eqxx. have [v vy v_F] : exists2 v, v -- y & v \in F. { rewrite defXYZ in min_xyz. have := @svseparator_neighbours _ _ _ y psepH. rewrite setUUC -{2}defXYZ !inE eqxx; case => // v [?] [Hv _ vy _]. exists v; rewrite 1?sgP //. by move: Hv; rewrite !inE negb_or negbK => /andP[]//. } apply: connectedU_edge vy _ _ => //. by rewrite inE eqxx. exact: connected1. - have -> : H :\ y = F :|: [set x]. apply/setP => i; rewrite setUC !inE. case: (eqVneq i y) => // ->. by rewrite [y==x]eq_sym (sg_edgeNeq xy) /= (disjointFl disjF) // !inE eqxx. have [v vx v_F] : exists2 v, v -- x & v \in F. { rewrite defXYZ in min_xyz. have := @svseparator_neighbours _ _ _ x psepH. rewrite setUUC -{2}defXYZ !inE eqxx; case => // v [?] [Hv _ vx _]. exists v; rewrite 1?sgP //. by move: Hv; rewrite !inE negb_or negbK => /andP[]//. } apply: connectedU_edge vx _ _ => //. by rewrite inE eqxx. exact: connected1. } rewrite !inE negb_or => /andP [wDx wDy]. pose Cx := [set v | connect (restrict (H :\ w) sedge) x v ]. wlog [s /setD1P [sNw s_H] sNCx] : / exists2 s, s \in H:\ w & s \notin Cx. { have [/exists_inP ?|] := boolP [exists s in H :\ w, s \notin Cx]; first by apply. move/exists_inPnn => C _. apply: (@connected_center _ x); last by rewrite !inE eqxx eq_sym wDx. by move=> v /C; rewrite !inE. } suff : separates x s [set w;z]. { by move/separates_vseparator/min3sep; rewrite cards2; case (_ == _). } have sDx : s != x by apply: contraNneq sNCx => ->; rewrite inE connect0. have sDy : s != y. { apply: contraNneq sNCx => ->; rewrite inE connect1 //= xy andbT. by rewrite !inE !eqxx ![_ == w]eq_sym wDx wDy. } have s_F : s \in F by move: s_H; rewrite !inE (negbTE sDx) (negbTE sDy). have sDz : s != z by apply: contraTneq s_F => ->; rewrite zNF. apply: separatesI; split. - by rewrite !inE negb_or xDz eq_sym wDx. - rewrite !inE negb_or sNw /=. by apply: contraNneq zNH => <-. - elim/card_ind => p IHp Ip. have [z_p|zNp] := boolP (z \in p); first by exists z => //; rewrite !inE eqxx. have W_xs (q : Path x s) : q \subset H -> w \in q. { move/subsetP => qH; apply: contraNT sNCx => wNq; rewrite inE. apply: (connectRI q) => i i_q. rewrite inE qH // andbT inE. by apply: contraNneq wNq => <-. } have [/W_xs|/subsetPn [i i_p iNH]] := boolP (p \subset H). { by exists w => //; rewrite !inE eqxx. } case def_p : _ / (isplitP Ip i_p) => [p1 p2 Ip1 Ip2 E1]. have y_p2 : y \in p2. { case: psepH => sepH _. have [] := @separation_separates _ s i _ _ sepH. - by rewrite !inE negb_or negbK s_F -defXYZ !inE (negbTE sDx) (negbTE sDy) sDz. - rewrite -defXYZ setUA [F :|: _]setUC -/H inE negb_or iNH inE. by apply: contraTneq i_p => ->. - move => _ _ /(_ (prev p2)) [y']; rewrite setUUC mem_prev -defXYZ => y'_p2. rewrite !inE -orbA => /or3P[] /eqP ?; subst y' => //. + by apply: contraNT iNH => _; rewrite -(E1 x). + by rewrite def_p !inE y'_p2 orbT in zNp. } case def_p2 : _ / (isplitP Ip2 y_p2) => [p21 p22 Ip21 Ip22 E2]. pose q := pcat (edgep xy) p22. have q_sub_p : {subset q <= p}. { by move=>j; case/edgeLP => [->|]; rewrite ?def_p ?def_p2 ?inE // => ->. } have [||j J1 J2] := IHp q. + apply/proper_card/properP; split; first exact/subsetP. exists i => //. apply: contraNN iNH => /edgeLP [->//|i_p22]. by rewrite [i]E2 ?inE // eqxx. + rewrite irred_edgeL Ip22 andbT. apply: contraTN iNH => x_p22. by rewrite -(E1 x) ?negbK // def_p2 inE x_p22. + exists j => //. rewrite -def_p2 -def_p. exact: q_sub_p. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph sgraph) GraphTheory(connectivity minor treewidth arc set_tac)