proposition: Theorem Menger (G : diGraph) (A B : {set G}) s : (forall S, separator G A B S -> s <= #|S|) -> exists (p : 'I_s -> pathS G), connector A B p.
proof: Proof. move: G s A B. elim/(size_ind num_edges) => G IH s A B min_s. case: (boolP [exists x : G, exists y : G, x -- y]) => [E|E0]; last first. - suff Hs : s <= #|A :&: B|. { case: (trivial_connector A B) => p. exact: sub_connector. } apply: min_s. apply: separatorI => a b p aA bB. case: (altP (a =P b)) => [?|aDb]. + subst b. exists a => //. by set_tac. + move/existsPn : E0 => /(_ a). case: (splitL p aDb) => x [ax] _. move/existsPn => /(_ x). by rewrite ax. - case/existsP : E => x /existsP [y xy]. pose G' := del_edge x y. have HG' : num_edges G' < num_edges G by exact: card_del_edge. move/(_ _ HG' s) in IH. case: (boolP [exists S : {set G'}, separatorb G' A B S && (#|S| < s)]); last first. { move/exists_inPn => Hs. case: (IH A B) => [S sepS|p conn_p]. - rewrite leqNgt Hs //. exact/separatorP. - exists (fun i : 'I_s => del_edge_liftS (p i)). exact: del_edge_connector. } case/exists_inP => S /separatorP sepS ltn_s. pose P := x |: S. have xP : x \in P by rewrite /P; set_tac. pose Q := y |: S. have yQ : y \in Q by rewrite /Q; set_tac. have [sep_G_P sep_G_Q] : separator G A B P /\ separator G A B Q. { have Hp (a b : G) (p : Path a b) : irred p -> a \in A -> b \in B -> (x \in p /\ y \in p) \/ exists2 s, s \in S & s \in p. { move => Ip aA bB. case: (del_edge_path_case x y Ip). - move => [p1] [p2] [H1 H2 H3]. left. rewrite !mem_path H1 !mem_cat. by rewrite -!(@mem_path G') !inE. - move => [p1 Ep]. right. case/sepS : (p1) => // z Z1 Z2. exists z => //. by rewrite (@mem_path G) Ep -(@mem_path G'). } split; apply: separatorI => a b p Ip aA bB. all: case: (Hp _ _ _ Ip aA bB) => [[xp yp]|[s0 in_S in_p]]. all: solve [by exists x | by exists y | exists s0; rewrite /P /Q; set_tac]. } have lift_AP T : separator G' A P T -> separator G A B T. { move => sepT. apply/separatorI => a b p Ip aA bB. case: (del_edge_path_case x y Ip). - move => [p1] [p2] [E Nx Ny]. case/sepT : (p1) => // t T1 T2. exists t => //. by rewrite mem_path E mem_cat -(@mem_path G') T2. - case. case => p' Ip' /= E. case/sep_G_P : (p) => // z zP zp. have zp' : z \in p' by rewrite (@mem_path G') -E -(@mem_path G). case: (split_at_first (D := G') zP zp') => u [p1] [p2] [E' uP ?]. case/sepT : (p1) => // t tT tp1. exists t => //. by rewrite mem_path E -(@mem_path G') E' mem_pcat tp1. } have lift_QB T : separator G' Q B T -> separator G A B T. { move => sepT. apply/separatorI => a b p Ip aA bB. case/sep_G_Q : (p) => // z zP zp. case: (del_edge_path_case x y Ip). - move => [p1] [p2] [E Nx Ny]. case/sepT : (p2) => // t T1 T2. exists t => //. by rewrite mem_path E mem_cat -(@mem_path G') T2. - case. case => p' Ip' /= E. have zp' : z \in p' by rewrite (@mem_path G') -E -(@mem_path G). case: (split_at_first (D := G') zP zp') => u [p1] [p2] [E' uP ?]. case/sepT : (p2) => // t tT tp1. exists t => //. by rewrite mem_path E -(@mem_path G') E' mem_pcat tp1. } have size_AP T : separator G' A P T -> s <= #|T|. move/lift_AP. exact: min_s. have size_QB T : separator G' Q B T -> s <= #|T|. move/lift_QB. exact: min_s. have card_S u : separator G A B (u |: S) -> u \notin S /\ s = #|u |: S|. { move => HS. have Hu : u \notin S. { apply: contraTN ltn_s => uS. by rewrite -leqNgt min_s // -(setU1_mem uS). } split => //. apply: esym. apply/eqP. by rewrite eqn_leq min_s // andbT cardsU1 Hu /= add1n. } case: (IH _ _ size_AP) => X conn_X. case: (IH _ _ size_QB) => Y conn_Y. have [i Hi] : exists j, lst (X j) = x. { suff : x \in codom (fun j => lst (X j)) by case/mapP => j _ ->; exists j. apply: inj_card_onto_pred xP. - exact: lst_inj conn_X. - exact: connector_lst conn_X. - rewrite card_ord. by apply card_S. } have xB : x \notin B. { move: (connector_fst conn_X i) => HA. move: (conn_end conn_X i). rewrite Hi => HP. case: (card_S _ sep_G_P) => xS _. apply: contraNN xS => xB. have [u U1 U2] : exists2 u, u \in S & u \in X i. { rewrite -Hi in xB. case: (X i) HA xB => [[a b] /= p]. exact: sepS. } move/setP/(_ u)/esym : HP. by rewrite !inE U1 U2 orbT /= => /eqP <-. } move/del_edge_connector : (conn_X) => conn_X'. move/del_edge_connector : (conn_Y) => conn_Y'. case: (altP (x =P y)) => [?|xDy]. { subst y. apply: connector_cat conn_X' conn_Y' => //. by apply esym,card_S. } have [j jP] : exists i : 'I_s, fst (Y i) = y :> G. { suff : y \in codom (fun j => fst (Y j)) by case/mapP => j _ ->; exists j. apply: inj_card_onto_pred (_ : y \in Q). - exact: fst_inj conn_Y. - exact: connector_fst conn_Y. - rewrite card_ord. by apply card_S. - by rewrite !inE eqxx. } case: (connector_extend (G := G) (i := j) _ _ xy xB conn_Y') => //. + move => {j jP}. apply/negP => /bigcupP [j] _. rewrite inE mem_del_edge_liftS => xYj. case EYj : (Y j) => [[u v] /= p]. rewrite -/(PathS p) in EYj. have Ip : irred p. { move: (conn_irred conn_Y j). by rewrite EYj. } have xp : x \in p by rewrite EYj in xYj. case/(isplitP Ip) def_p : _ / xp => [p1 p2 Ip1 Ip2 I]. case EXi : (X i) => [[a x'] /= q]. rewrite -/(PathS q) in EXi. have ? : x' = x by rewrite -Hi EXi. subst x'. case: (sepS a v (pcat q p2)) => [||t t_in_S]. * move: (connector_fst conn_X i). by rewrite EXi. * move: (connector_lst conn_Y j). by rewrite EYj. * rewrite inE. case/orP => Ht. -- move: (t_in_S). rewrite [t](connector_right conn_X (i := i)) ?EXi ?inE ?t_in_S /lst //=. apply/negP. by apply card_S. -- move: (t_in_S). apply/negP. rewrite [t]I //; first by apply card_S. rewrite [t](connector_left conn_Y (i := j)) ?inE ?t_in_S //. ++ rewrite EYj /fst /=. by rewrite (@path_begin G'). ++ by rewrite EYj -[_ \in _]/(t \in p) def_p inE Ht. + by case: (Y j) jP => [[a b] p]. + move => Y'. rewrite [_ |: _](_ : _ = P) => [conn_xY|]. * apply: connector_cat conn_X' conn_xY => //. by apply esym,card_S. * apply/setP => u. rewrite /Q setU1K //. by apply card_S. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph mgraph sgraph set_tac)