Library GraphTheory.connectivity
From mathcomp Require Import all_ssreflect.
Require Import edone preliminaries digraph sgraph mgraph set_tac.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Set Bullet Behavior "Strict Subproofs".
Require Import edone preliminaries digraph sgraph mgraph set_tac.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Set Bullet Behavior "Strict Subproofs".
Graph Connectivty
Connectors, Separators, and Separations
Section SeparatorConnector.
Variables (G : diGraph).
Implicit Types (x y z u v : G) (A B S U V : {set G}).
There are two notions af separators used in the literature,
"AB-separators" (i.e., sets disconnecting two not necessariliy
disjoint sets of vertices) and "(vertex) separarors" (i.e., sets of
vertices disconnecting a given graph).
Definition separator (A B S : {set G}) :=
∀ (a b : G) (p : Path a b), a \in A → b \in B → exists2 s, s \in S & s \in p.
Lemma separatorI A B S :
(∀ (a b : G) (p : Path a b), irred p → a \in A → b \in B → exists2 s, s \in S & s \in p)
→ separator A B S.
Proof.
move ⇒ H a b p aA bB. case: (uncycle p) ⇒ p' sub_p Ip. case: (H _ _ p') ⇒ //.
move ⇒ s sS /sub_p sp. by ∃ s.
Qed.
Definition separatorb (A B S : {set G}) :=
[∀ a in A, ∀ b in B, ∀ p : IPath a b, ∃ s in S, s \in p].
Lemma separatorP (A B S : {set G}) : reflect (separator A B S) (separatorb A B S).
Proof.
rewrite /separatorb. apply: (iffP forall_inP) ⇒ [H|H a aA].
- apply: separatorI ⇒ a b p Ip aA bB.
move/(_ _ aA) : H ⇒ /forall_inP /(_ _ bB) /forallP /(_ (Sub p Ip)) /exists_inP [s sS in_p].
by ∃ s.
- apply/forall_inP ⇒ b bB. apply/forallP ⇒ [[p ?]]. apply/exists_inP.
case: (H a b p) ⇒ // s S1 S2. by ∃ s.
Qed.
Lemma separatorPn (A B S : {set G}) :
reflect (∃ x y (p: IPath x y), [/\ x \in A, y \in B & [disjoint p & S]]) (~~ separatorb A B S).
Proof.
rewrite negb_forall_in. apply: (iffP exists_inP).
- case ⇒ x xA /forall_inPn [y] yB /forallPn [p] /exists_inPn H.
∃ x; ∃ y; ∃ p; split ⇒ //. apply/disjointP ⇒ z Z1 /H. by rewrite Z1.
- case ⇒ x [y] [p] [aA yB /disjointP D]. ∃ x ⇒ //. apply/forall_inPn; ∃ y ⇒ //.
apply/forallPn; ∃ p. apply/exists_inPn ⇒ z /D H. exact/negP.
Qed.
Lemma separator_cap A B S : separator A B S → A :&: B \subset S.
Proof.
move ⇒ sepS. apply/subsetP ⇒ x /setIP [xA xB].
case: (sepS _ _ (idp x)) ⇒ // s in_S. by rewrite mem_idp ⇒ /eqP <-.
Qed.
Lemma separator_min A B S : separator A B S → #|A :&: B| ≤ #|S|.
Proof. move/separator_cap. exact: subset_leq_card. Qed.
Definition separates x y U := [/\ x \notin U, y \notin U & ∀ p : Path x y, exists2 z, z \in p & z \in U].
Standard trick to show decidability: quantify only over irredundant paths
Definition separatesb x y U := [&& x \notin U, y \notin U & [∀ p : IPath x y, ∃ z in p, z \in U]].
Lemma separatesI x y (U : {set G}) :
[/\ x \notin U, y \notin U & ∀ p : Path x y, irred p → exists2 z, z \in p & z \in U] → separates x y U.
Proof.
case ⇒ S1 S2 S3. split ⇒ // p. case: (uncycle p) ⇒ p' sub_p Ip'.
case: (S3 _ Ip') ⇒ z Z1 Z2. ∃ z ⇒ //. exact: sub_p.
Qed.
Lemma separatesP x y U : reflect (separates x y U) (separatesb x y U).
Proof.
apply: (iffP and3P) ⇒ [[? ? A]|[? ? A]].
- apply: separatesI. split ⇒ // p Ip.
move/forallP/(_ (Build_IPath Ip)) : A.
case/exists_inP ⇒ z Z1 Z2. by ∃ z.
- split ⇒ //. apply/forallP ⇒ p. by move/exists_inP : (A p).
Qed.
Arguments separatesP {x y U}.
Fact separatesNeq x y U : separates x y U → x != y.
Proof.
case ⇒ Hx _ Hp. apply: contraNN Hx ⇒ /eqP C. subst y. case: (Hp (idp x)).
move ⇒ ?. by rewrite mem_idp ⇒ /eqP→.
Qed.
Lemma separatesI x y (U : {set G}) :
[/\ x \notin U, y \notin U & ∀ p : Path x y, irred p → exists2 z, z \in p & z \in U] → separates x y U.
Proof.
case ⇒ S1 S2 S3. split ⇒ // p. case: (uncycle p) ⇒ p' sub_p Ip'.
case: (S3 _ Ip') ⇒ z Z1 Z2. ∃ z ⇒ //. exact: sub_p.
Qed.
Lemma separatesP x y U : reflect (separates x y U) (separatesb x y U).
Proof.
apply: (iffP and3P) ⇒ [[? ? A]|[? ? A]].
- apply: separatesI. split ⇒ // p Ip.
move/forallP/(_ (Build_IPath Ip)) : A.
case/exists_inP ⇒ z Z1 Z2. by ∃ z.
- split ⇒ //. apply/forallP ⇒ p. by move/exists_inP : (A p).
Qed.
Arguments separatesP {x y U}.
Fact separatesNeq x y U : separates x y U → x != y.
Proof.
case ⇒ Hx _ Hp. apply: contraNN Hx ⇒ /eqP C. subst y. case: (Hp (idp x)).
move ⇒ ?. by rewrite mem_idp ⇒ /eqP→.
Qed.
TOTHINK: conn_disjoint could also be expressed as x \in p i → x \in p j → i = j NOTE: Unlike the definition of Göring, we do not allow single edge paths inside A :&: B
Record connector (A B : {set G}) n (p : 'I_n → pathS G) : Prop :=
{ conn_irred : ∀ i, irred (tagged (p i));
conn_begin : ∀ i, [set x in p i] :&: A = [set fst (p i)];
conn_end : ∀ i, [set x in p i] :&: B = [set lst (p i)];
conn_disjoint : ∀ i j, i != j → [set x in p i] :&: [set x in p j] = set0 }.
Section ConnectorTheory.
Variables (A B : {set G}) (n : nat) (p : 'I_n → pathS G).
Hypothesis conn_p : connector A B p.
Lemma connector_fst i : fst (p i) \in A.
Proof.
move/setP : (conn_begin conn_p i) ⇒ /(_ (fst (p i))).
rewrite !inE eqxx. by case/andP.
Qed.
Lemma connector_lst i : lst (p i) \in B.
Proof.
move/setP : (conn_end conn_p i) ⇒ /(_ (lst (p i))).
rewrite !inE eqxx. by case/andP.
Qed.
Lemma connector_left i x : x \in p i → x \in A → x = fst (p i).
Proof.
move ⇒ in_pi in_A. move/setP : (conn_begin conn_p i) ⇒ /(_ x).
rewrite !inE in_pi in_A /=. by move/esym/eqP.
Qed.
Lemma connector_right i x : x \in p i → x \in B → x = lst (p i).
Proof.
move ⇒ in_pi in_B. move/setP : (conn_end conn_p i) ⇒ /(_ x).
rewrite !inE in_pi in_B /=. by move/esym/eqP.
Qed.
Lemma lst_idp i : lst (p i) \in A → lst (p i) = fst (p i).
Proof.
move ⇒ H. move/setP : (conn_begin conn_p i) ⇒ /(_ (lst (p i))).
rewrite !inE H. by move/esym/eqP.
Qed.
Lemma fst_idp i : fst (p i) \in B → fst (p i) = lst (p i).
Proof.
move ⇒ H. move/setP : (conn_end conn_p i) ⇒ /(_ (fst (p i))).
rewrite !inE H. by move/esym/eqP.
Qed.
Lemma connector_eq i j x : x \in p i → x \in p j → i = j.
Proof.
move ⇒ Hi Hj. apply: contraTeq isT ⇒ /(conn_disjoint conn_p)/setP/(_ x).
by rewrite !inE Hi Hj.
Qed.
Lemma fst_lst_eq i j : fst (p i) = lst (p j) → i = j.
Proof.
move ⇒ E. apply: (connector_eq (x := fst (p i))); first exact: fst_mem.
by rewrite E lst_mem.
Qed.
Lemma fst_inj : injective (@fst G \o p).
Proof.
apply/injectiveP.
apply: wlog_neg ⇒ /injectivePn [i] [j] /(conn_disjoint conn_p)/setP S /= H.
move/(_ (fst (p i))) : S. by rewrite !inE H fst_mem.
Qed.
Lemma lst_inj : injective (@lst G \o p).
Proof.
apply/injectiveP.
apply: wlog_neg ⇒ /injectivePn [i] [j] /(conn_disjoint conn_p)/setP S /= H.
move/(_ (lst (p i))) : S. by rewrite !inE H lst_mem.
Qed.
End ConnectorTheory.
Lemma connector_extend A B n (p : 'I_n → pathS G) x y i :
x \notin \bigcup_i [set z in p i] → fst (p i) = y → x -- y → x \notin B →
connector A B p → ∃ q : 'I_n → pathS G, connector (x |: (A :\ y)) B q.
Proof.
move ⇒ Hx Hy xy xB conn_p.
have xDy : x != y.
{ apply: contraNneq Hx ⇒ →. apply/bigcupP; ∃ i ⇒ //. by rewrite inE -Hy fst_mem. }
set A' := _ |: _.
pose q (j : 'I_n) := if j == i then pcatS (PathS (edgep xy)) (p j) else p j.
have Hj (j : 'I_n) u : j != i → u \in tagged (p j) → (u == y = false)*(u == x = false).
{ move ⇒ jDi u_pi. split.
- apply: contra_eqF (conn_disjoint conn_p jDi) ⇒ /eqP ?; subst.
apply/set0Pn; ∃ (fst (p i)). by rewrite !inE u_pi.
- apply: contraNF Hx ⇒ /eqP <-. apply/bigcupP; ∃ j ⇒ //. by rewrite inE. }
∃ q. split.
- move ⇒ j. rewrite /q /=.
case: (altP (j =P i)) ⇒ [E|D]; last exact: (conn_irred conn_p).
subst j. rewrite [p i]pathS_eta. subst y. rewrite pcatSE /= irred_edgeL.
rewrite (conn_irred conn_p) andbT. apply: contraNN Hx ⇒ Hx.
apply/bigcupP. ∃ i ⇒ //. by rewrite inE.
- move ⇒ j. rewrite /q. case: (altP (j =P i)) ⇒ [E|D].
+ subst j. rewrite [p i]pathS_eta. subst y. rewrite pcatSE /=.
apply/setP ⇒ u. rewrite [A']lock !inE -lock. apply/andP/idP.
× rewrite !inE mem_edgep /=. case: (altP (u =P x)) ⇒ [-> //|/=].
rewrite -/(fst (p i)). case: (altP (u =P fst (p i))) ⇒ [_ _ [_ ?] //|].
rewrite /= -/(fst (p i)) ⇒ [H1 H2 [H3 H4]].
by rewrite -(connector_left conn_p _ H4) ?eqxx in H1.
× move/eqP→. by rewrite mem_edgep /= !inE eqxx.
+ rewrite -(conn_begin conn_p).
apply/setP ⇒ u. rewrite !inE. case e: (u \in _) ⇒ //=. by rewrite !(Hj j) /=.
- move ⇒ j. rewrite /q. case: (altP (j =P i)) ⇒ [E|D]; last exact: (conn_end conn_p).
subst j. rewrite [p i]pathS_eta. subst y. rewrite pcatSE /= -/(lst _).
apply/setP ⇒ u. rewrite -(conn_end conn_p i) !inE -mem_pcat. case uB : (u \in B) ⇒ //.
rewrite !andbT. apply/edgeLP/idP ⇒ /=; last by right. case ⇒ [?|//].
subst. by rewrite uB in xB.
- move ⇒ j1 j2. rewrite /q.
have jP j : i != j → [set x0 in pcatS (PathS (edgep xy)) (p i)] :&: [set x0 in p j] = set0.
{ move ⇒ jDi. rewrite [p i]pathS_eta. subst y. rewrite pcatSE.
apply: contra_eq (conn_disjoint conn_p jDi). case/set0Pn ⇒ u /setIP [].
rewrite 2!inE /=. case/edgeLP ⇒ /= [-> Hx'|Hu ?].
× apply: contraNN Hx ⇒ _. apply/bigcupP; ∃ j ⇒ //. by rewrite inE.
× apply/set0Pn. ∃ u. by rewrite !inE Hu. }
case: (altP (j1 =P i)); case: (altP (j2 =P i)).
+ move ⇒ → → . by rewrite eqxx.
+ rewrite eq_sym ⇒ Hj2 →. exact: jP.
+ rewrite eq_sym setIC. move ⇒ → Hj2 _. exact: jP.
+ move ⇒ _ _. exact: (conn_disjoint conn_p).
Qed.
Lemma connector_sep P A B n (p q : 'I_n → pathS G) i j x :
separator A B P → connector A P p → connector P B q →
x \in p i → x \in q j → (x \in P) .
Proof.
move ⇒ sep_P con_p con_q x_pi x_qj.
case def_pi : (p i) ⇒ [[u v] /= pi].
case def_qj : (q j) ⇒ [[u' v'] /= qj]. rewrite -!/(PathS _) in def_pi def_qj.
have [x_pi' x_qj'] : x \in pi ∧ x \in qj by rewrite def_pi def_qj in x_pi x_qj.
have Ip : irred pi. { move: (conn_irred con_p i). by rewrite def_pi. }
have Iq : irred qj. { move: (conn_irred con_q j). by rewrite def_qj. }
case/(isplitP Ip) def_p : _ / x_pi' ⇒ {Ip} [p1 p2 Ip1 Ip2 Ip].
case/(isplitP Iq) def_q : _ / x_qj' ⇒ {Iq} [q1 q2 Iq1 Iq2 Iq].
case: (sep_P _ _ (pcat p1 q2)).
- move: (connector_fst con_p i). by rewrite def_pi.
- move: (connector_lst con_q j). by rewrite def_qj.
- move ⇒ s in_P. rewrite inE. case/orP ⇒ [in_p1|in_q2].
+ suff ? : s = v by subst s; rewrite [v]Ip // inE in in_P.
rewrite [s](connector_right con_p (i := i)) // def_pi //.
change (s \in pi). by rewrite def_p inE in_p1.
+ suff ? : s = u' by subst s; rewrite [u']Iq // inE in in_P.
rewrite [s](connector_left con_q (i := j)) // def_qj //.
change (s \in qj). by rewrite def_q inE in_q2.
Qed.
Lemma connector_cat (P A B : {set G}) n (p q : 'I_n → pathS G) :
#|P| = n → separator A B P →
connector A P p → connector P B q →
∃ (r : 'I_n → pathS G), connector A B r.
Proof.
move ⇒ card_P. subst n. move ⇒ sep_P con_p con_q.
have mtch i : { j | fst (q j) = lst (p i) }.
{ pose x := lst (p i).
have Hx : x \in codom (@fst G \o q).
{ apply: (inj_card_onto_pred (P := mem P)).
- exact: fst_inj con_q.
- move ⇒ j. exact: connector_fst con_q _.
- by rewrite card_ord.
- exact: connector_lst con_p _. }
∃ (iinv Hx). rewrite -[fst _]/((@fst G \o q) (iinv Hx)). by rewrite f_iinv. }
have mtch_inj : injective (fun i ⇒ sval (mtch i)).
{ move ⇒ i i' E. move: (svalP (mtch i')). rewrite -E (svalP (mtch i)).
exact : (lst_inj con_p). }
pose pq i := pcatS (p i) (q (sval (mtch i))).
have pqE i : ∃ j x y z (pi : Path x y) (qi : Path y z),
[/\ p i = PathS pi, j = sval (mtch i), q j = PathS qi & pq i = PathS (pcat pi qi) ].
{ pose j := sval (mtch i).
have jP := svalP (mtch i) : fst (q j) = lst (p i).
∃ j. ∃ (fst (p i)). ∃ (lst (p i)). ∃ (lst (q j)).
∃ (tagged (p i)). ∃ (castL jP (tagged (q j))). split ⇒ //.
- by rewrite {1}[p i]pathS_eta.
- rewrite {1}[q j]pathS_eta. move: (jP). rewrite -jP ⇒ jP'.
by rewrite (eq_irrelevance jP' erefl).
- rewrite /pq -/j. rewrite -pcatSE -pathS_eta. move: (jP). rewrite -jP ⇒ jP'.
by rewrite (eq_irrelevance jP' erefl) /= -pathS_eta. }
have sepP i j x : x \in p i → x \in q j → x \in P.
{ exact: connector_sep sep_P con_p con_q. }
∃ pq. split.
- move ⇒ i. move: (pqE i) ⇒ [j] [x] [y] [z] [pi] [qj] [Ep Ej Eq ->] /=.
apply: irred_catI ⇒ [u u_p u_q||].
+ have uP : u \in P. apply: (sepP i j u); rewrite ?Ep ?Eq //.
move: (conn_end con_p i) ⇒ /setP/(_ u). rewrite Ep !inE /= u_p uP /=.
by move/esym/eqP.
+ move: (conn_irred con_p i). by rewrite Ep.
+ move: (conn_irred con_q j). by rewrite Eq.
- move ⇒ i. move: (pqE i) ⇒ [j] [x] [y] [z] [pi] [qj] [Ep Ej Eq ->] /=.
apply/setP ⇒ u. rewrite !inE /=. apply/andP/eqP ⇒ [[/orP[u_pi|u_qj] uA]|->].
+ move/(_ i u): (connector_left con_p). rewrite Ep /= u_pi uA. by apply.
+ suff ? : u = y.
{ subst. suff: lst (p i) = fst (p i) by rewrite Ep.
apply: (lst_idp con_p _). by rewrite !Ep. }
have Iq : irred qj. move: (conn_irred con_q j). by rewrite Eq.
case/(isplitP Iq) def_q : _ / u_qj ⇒ [q1 q2 _ _ I].
have zB : z \in B. { move: (connector_lst con_q j). by rewrite Eq. }
case: (sep_P _ _ q2) ⇒ // s sP in_q2.
have ? : s = y.
{ by rewrite [s](connector_left con_q (i := j)) // Eq // def_q mem_pcat in_q2. }
subst s. by rewrite [y]I // inE.
+ by rewrite inE /fst/= [x](_ : _ = fst (p i)) ?(connector_fst con_p) // Ep.
-
move ⇒ i. move: (pqE i) ⇒ [j] [x] [y] [z] [pi] [qj] [Ep Ej Eq ->] /=.
apply/setP ⇒ u. rewrite !inE /=. apply/andP/eqP ⇒ [[/orP[u_pi|u_qj] uB]|->].
+ have uz : u = y.
{ have Ip : irred pi. move: (conn_irred con_p i). by rewrite Ep.
case/(isplitP Ip) def_p : _ / u_pi ⇒ [p1 p2 _ _ I].
have xA : x \in A. { move: (connector_fst con_p i). by rewrite Ep. }
case: (sep_P _ _ p1) ⇒ // s sP in_p1.
have ? : s = y.
{ by rewrite [s](connector_right con_p (i := i)) // Ep // def_p mem_pcat in_p1. }
subst s. by rewrite [y]I // inE. }
subst u.
suff: fst (q j) = lst (q j). by rewrite Eq.
apply: (fst_idp con_q _). by rewrite Eq.
+ move/(_ j u): (connector_right con_q). rewrite Eq /= u_qj uB. by apply.
+ by rewrite inE /lst/= [z](_ : _ = lst (q j)) ?(connector_lst con_q) // Eq.
- move ⇒ i j iDj.
move: (pqE i) ⇒ [i2] [x] [y] [z] [pi] [qi2] [Ep Ei Eq ->] /=.
move: (pqE j) ⇒ [j2] [x'] [y'] [z'] [pj] [qj2] [Ep' Ej Eq' ->] /=.
apply/eqP. apply: wlog_neg. case/set0Pn ⇒ u. rewrite !inE ⇒ /andP[].
case/orP ⇒ Hi; case/orP ⇒ Hj; case: notF.
+ move/setP/(_ u): (conn_disjoint con_p iDj). by rewrite Ep Ep' !inE Hi Hj.
+ have uP : u \in P.
{ apply: (@connector_sep P A B _ p q i j2 u) ⇒ //; by rewrite ?Ep ?Eq'. }
have [? ?] : y' = u ∧ y = u.
{ split.
- by rewrite {1}[u](connector_left con_q (i := j2)) ?Eq'.
- by rewrite {1}[u](connector_right con_p (i := i)) ?Ep. }
subst y' y. apply: contraNT iDj ⇒ _. apply/eqP. apply: mtch_inj.
rewrite -Ei -Ej. apply: (connector_eq con_q (x := u)); by rewrite ?Eq ?Eq' inE.
+ have uP : u \in P.
{ apply: (@connector_sep P A B _ p q j i2 u) ⇒ // ; by rewrite ?Ep' ?Eq. }
have [? ?] : y' = u ∧ y = u.
{ split.
- by rewrite {1}[u](connector_right con_p (i := j)) ?Ep'.
- by rewrite {1}[u](connector_left con_q (i := i2)) ?Eq. }
subst y' y. apply: contraNT iDj ⇒ _. apply/eqP. apply: mtch_inj.
rewrite -Ei -Ej. apply: (connector_eq con_q (x := u)); by rewrite ?Eq ?Eq' inE.
+ apply: contraNT iDj ⇒ _. apply/eqP. apply: mtch_inj. rewrite -Ei -Ej.
apply: contraTeq isT ⇒ iDj.
move/setP/(_ u): (conn_disjoint con_q iDj). by rewrite Eq Eq' !inE Hi Hj.
Qed.
Lemma trivial_connector A B : ∃ p : 'I_#|A :&: B| → pathS G, connector A B p.
Proof.
∃ (fun i ⇒ PathS (idp (enum_val i))). split.
- move ⇒ i /=. exact: irred_idp.
- move ⇒ i /=. case/setIP : (enum_valP i) ⇒ iA iB. apply/setP ⇒ z.
rewrite !inE /= mem_idp. case e: (_ == _) ⇒ //. by rewrite (eqP e).
- move ⇒ i /=. case/setIP : (enum_valP i) ⇒ iA iB. apply/setP ⇒ z.
rewrite !inE /= mem_idp. case e: (_ == _) ⇒ //. by rewrite (eqP e).
- move ⇒ i j. apply: contraNeq ⇒ /set0Pn [x /setIP[]].
by rewrite !inE /= !mem_idp ⇒ /eqP→ /eqP /enum_val_inj→.
Qed.
Lemma sub_connector A B n m (p : 'I_m → pathS G) :
n ≤ m → connector A B p → ∃ q : 'I_n → pathS G, connector A B q.
Proof.
move ⇒ n_leq_m conn_p. pose W := widen_ord n_leq_m. ∃ (fun i ⇒ p (W i)).
case: conn_p ⇒ C1 C2 C3 C4. split ⇒ // i j. exact:(C4 (W i) (W j)).
Qed.
End SeparatorConnector.
Arguments separatesP {G x y U}.
Section VSeparator.
Variable (G : sgraph).
Implicit Types (x y z u v : G) (S U V : {set G}).
Fact separates0P x y : reflect (separates x y set0) (~~ connect edge_rel x y).
Proof.
apply:(iffP idP) ⇒ [nconn_xy|].
- rewrite /separates !inE. split ⇒ // p. by rewrite Path_connect in nconn_xy.
- case ⇒ _ _ H. apply/negP. case/connect_irredP ⇒ p _. case: (H p) ⇒ z. by rewrite inE.
Qed.
{ conn_irred : ∀ i, irred (tagged (p i));
conn_begin : ∀ i, [set x in p i] :&: A = [set fst (p i)];
conn_end : ∀ i, [set x in p i] :&: B = [set lst (p i)];
conn_disjoint : ∀ i j, i != j → [set x in p i] :&: [set x in p j] = set0 }.
Section ConnectorTheory.
Variables (A B : {set G}) (n : nat) (p : 'I_n → pathS G).
Hypothesis conn_p : connector A B p.
Lemma connector_fst i : fst (p i) \in A.
Proof.
move/setP : (conn_begin conn_p i) ⇒ /(_ (fst (p i))).
rewrite !inE eqxx. by case/andP.
Qed.
Lemma connector_lst i : lst (p i) \in B.
Proof.
move/setP : (conn_end conn_p i) ⇒ /(_ (lst (p i))).
rewrite !inE eqxx. by case/andP.
Qed.
Lemma connector_left i x : x \in p i → x \in A → x = fst (p i).
Proof.
move ⇒ in_pi in_A. move/setP : (conn_begin conn_p i) ⇒ /(_ x).
rewrite !inE in_pi in_A /=. by move/esym/eqP.
Qed.
Lemma connector_right i x : x \in p i → x \in B → x = lst (p i).
Proof.
move ⇒ in_pi in_B. move/setP : (conn_end conn_p i) ⇒ /(_ x).
rewrite !inE in_pi in_B /=. by move/esym/eqP.
Qed.
Lemma lst_idp i : lst (p i) \in A → lst (p i) = fst (p i).
Proof.
move ⇒ H. move/setP : (conn_begin conn_p i) ⇒ /(_ (lst (p i))).
rewrite !inE H. by move/esym/eqP.
Qed.
Lemma fst_idp i : fst (p i) \in B → fst (p i) = lst (p i).
Proof.
move ⇒ H. move/setP : (conn_end conn_p i) ⇒ /(_ (fst (p i))).
rewrite !inE H. by move/esym/eqP.
Qed.
Lemma connector_eq i j x : x \in p i → x \in p j → i = j.
Proof.
move ⇒ Hi Hj. apply: contraTeq isT ⇒ /(conn_disjoint conn_p)/setP/(_ x).
by rewrite !inE Hi Hj.
Qed.
Lemma fst_lst_eq i j : fst (p i) = lst (p j) → i = j.
Proof.
move ⇒ E. apply: (connector_eq (x := fst (p i))); first exact: fst_mem.
by rewrite E lst_mem.
Qed.
Lemma fst_inj : injective (@fst G \o p).
Proof.
apply/injectiveP.
apply: wlog_neg ⇒ /injectivePn [i] [j] /(conn_disjoint conn_p)/setP S /= H.
move/(_ (fst (p i))) : S. by rewrite !inE H fst_mem.
Qed.
Lemma lst_inj : injective (@lst G \o p).
Proof.
apply/injectiveP.
apply: wlog_neg ⇒ /injectivePn [i] [j] /(conn_disjoint conn_p)/setP S /= H.
move/(_ (lst (p i))) : S. by rewrite !inE H lst_mem.
Qed.
End ConnectorTheory.
Lemma connector_extend A B n (p : 'I_n → pathS G) x y i :
x \notin \bigcup_i [set z in p i] → fst (p i) = y → x -- y → x \notin B →
connector A B p → ∃ q : 'I_n → pathS G, connector (x |: (A :\ y)) B q.
Proof.
move ⇒ Hx Hy xy xB conn_p.
have xDy : x != y.
{ apply: contraNneq Hx ⇒ →. apply/bigcupP; ∃ i ⇒ //. by rewrite inE -Hy fst_mem. }
set A' := _ |: _.
pose q (j : 'I_n) := if j == i then pcatS (PathS (edgep xy)) (p j) else p j.
have Hj (j : 'I_n) u : j != i → u \in tagged (p j) → (u == y = false)*(u == x = false).
{ move ⇒ jDi u_pi. split.
- apply: contra_eqF (conn_disjoint conn_p jDi) ⇒ /eqP ?; subst.
apply/set0Pn; ∃ (fst (p i)). by rewrite !inE u_pi.
- apply: contraNF Hx ⇒ /eqP <-. apply/bigcupP; ∃ j ⇒ //. by rewrite inE. }
∃ q. split.
- move ⇒ j. rewrite /q /=.
case: (altP (j =P i)) ⇒ [E|D]; last exact: (conn_irred conn_p).
subst j. rewrite [p i]pathS_eta. subst y. rewrite pcatSE /= irred_edgeL.
rewrite (conn_irred conn_p) andbT. apply: contraNN Hx ⇒ Hx.
apply/bigcupP. ∃ i ⇒ //. by rewrite inE.
- move ⇒ j. rewrite /q. case: (altP (j =P i)) ⇒ [E|D].
+ subst j. rewrite [p i]pathS_eta. subst y. rewrite pcatSE /=.
apply/setP ⇒ u. rewrite [A']lock !inE -lock. apply/andP/idP.
× rewrite !inE mem_edgep /=. case: (altP (u =P x)) ⇒ [-> //|/=].
rewrite -/(fst (p i)). case: (altP (u =P fst (p i))) ⇒ [_ _ [_ ?] //|].
rewrite /= -/(fst (p i)) ⇒ [H1 H2 [H3 H4]].
by rewrite -(connector_left conn_p _ H4) ?eqxx in H1.
× move/eqP→. by rewrite mem_edgep /= !inE eqxx.
+ rewrite -(conn_begin conn_p).
apply/setP ⇒ u. rewrite !inE. case e: (u \in _) ⇒ //=. by rewrite !(Hj j) /=.
- move ⇒ j. rewrite /q. case: (altP (j =P i)) ⇒ [E|D]; last exact: (conn_end conn_p).
subst j. rewrite [p i]pathS_eta. subst y. rewrite pcatSE /= -/(lst _).
apply/setP ⇒ u. rewrite -(conn_end conn_p i) !inE -mem_pcat. case uB : (u \in B) ⇒ //.
rewrite !andbT. apply/edgeLP/idP ⇒ /=; last by right. case ⇒ [?|//].
subst. by rewrite uB in xB.
- move ⇒ j1 j2. rewrite /q.
have jP j : i != j → [set x0 in pcatS (PathS (edgep xy)) (p i)] :&: [set x0 in p j] = set0.
{ move ⇒ jDi. rewrite [p i]pathS_eta. subst y. rewrite pcatSE.
apply: contra_eq (conn_disjoint conn_p jDi). case/set0Pn ⇒ u /setIP [].
rewrite 2!inE /=. case/edgeLP ⇒ /= [-> Hx'|Hu ?].
× apply: contraNN Hx ⇒ _. apply/bigcupP; ∃ j ⇒ //. by rewrite inE.
× apply/set0Pn. ∃ u. by rewrite !inE Hu. }
case: (altP (j1 =P i)); case: (altP (j2 =P i)).
+ move ⇒ → → . by rewrite eqxx.
+ rewrite eq_sym ⇒ Hj2 →. exact: jP.
+ rewrite eq_sym setIC. move ⇒ → Hj2 _. exact: jP.
+ move ⇒ _ _. exact: (conn_disjoint conn_p).
Qed.
Lemma connector_sep P A B n (p q : 'I_n → pathS G) i j x :
separator A B P → connector A P p → connector P B q →
x \in p i → x \in q j → (x \in P) .
Proof.
move ⇒ sep_P con_p con_q x_pi x_qj.
case def_pi : (p i) ⇒ [[u v] /= pi].
case def_qj : (q j) ⇒ [[u' v'] /= qj]. rewrite -!/(PathS _) in def_pi def_qj.
have [x_pi' x_qj'] : x \in pi ∧ x \in qj by rewrite def_pi def_qj in x_pi x_qj.
have Ip : irred pi. { move: (conn_irred con_p i). by rewrite def_pi. }
have Iq : irred qj. { move: (conn_irred con_q j). by rewrite def_qj. }
case/(isplitP Ip) def_p : _ / x_pi' ⇒ {Ip} [p1 p2 Ip1 Ip2 Ip].
case/(isplitP Iq) def_q : _ / x_qj' ⇒ {Iq} [q1 q2 Iq1 Iq2 Iq].
case: (sep_P _ _ (pcat p1 q2)).
- move: (connector_fst con_p i). by rewrite def_pi.
- move: (connector_lst con_q j). by rewrite def_qj.
- move ⇒ s in_P. rewrite inE. case/orP ⇒ [in_p1|in_q2].
+ suff ? : s = v by subst s; rewrite [v]Ip // inE in in_P.
rewrite [s](connector_right con_p (i := i)) // def_pi //.
change (s \in pi). by rewrite def_p inE in_p1.
+ suff ? : s = u' by subst s; rewrite [u']Iq // inE in in_P.
rewrite [s](connector_left con_q (i := j)) // def_qj //.
change (s \in qj). by rewrite def_q inE in_q2.
Qed.
Lemma connector_cat (P A B : {set G}) n (p q : 'I_n → pathS G) :
#|P| = n → separator A B P →
connector A P p → connector P B q →
∃ (r : 'I_n → pathS G), connector A B r.
Proof.
move ⇒ card_P. subst n. move ⇒ sep_P con_p con_q.
have mtch i : { j | fst (q j) = lst (p i) }.
{ pose x := lst (p i).
have Hx : x \in codom (@fst G \o q).
{ apply: (inj_card_onto_pred (P := mem P)).
- exact: fst_inj con_q.
- move ⇒ j. exact: connector_fst con_q _.
- by rewrite card_ord.
- exact: connector_lst con_p _. }
∃ (iinv Hx). rewrite -[fst _]/((@fst G \o q) (iinv Hx)). by rewrite f_iinv. }
have mtch_inj : injective (fun i ⇒ sval (mtch i)).
{ move ⇒ i i' E. move: (svalP (mtch i')). rewrite -E (svalP (mtch i)).
exact : (lst_inj con_p). }
pose pq i := pcatS (p i) (q (sval (mtch i))).
have pqE i : ∃ j x y z (pi : Path x y) (qi : Path y z),
[/\ p i = PathS pi, j = sval (mtch i), q j = PathS qi & pq i = PathS (pcat pi qi) ].
{ pose j := sval (mtch i).
have jP := svalP (mtch i) : fst (q j) = lst (p i).
∃ j. ∃ (fst (p i)). ∃ (lst (p i)). ∃ (lst (q j)).
∃ (tagged (p i)). ∃ (castL jP (tagged (q j))). split ⇒ //.
- by rewrite {1}[p i]pathS_eta.
- rewrite {1}[q j]pathS_eta. move: (jP). rewrite -jP ⇒ jP'.
by rewrite (eq_irrelevance jP' erefl).
- rewrite /pq -/j. rewrite -pcatSE -pathS_eta. move: (jP). rewrite -jP ⇒ jP'.
by rewrite (eq_irrelevance jP' erefl) /= -pathS_eta. }
have sepP i j x : x \in p i → x \in q j → x \in P.
{ exact: connector_sep sep_P con_p con_q. }
∃ pq. split.
- move ⇒ i. move: (pqE i) ⇒ [j] [x] [y] [z] [pi] [qj] [Ep Ej Eq ->] /=.
apply: irred_catI ⇒ [u u_p u_q||].
+ have uP : u \in P. apply: (sepP i j u); rewrite ?Ep ?Eq //.
move: (conn_end con_p i) ⇒ /setP/(_ u). rewrite Ep !inE /= u_p uP /=.
by move/esym/eqP.
+ move: (conn_irred con_p i). by rewrite Ep.
+ move: (conn_irred con_q j). by rewrite Eq.
- move ⇒ i. move: (pqE i) ⇒ [j] [x] [y] [z] [pi] [qj] [Ep Ej Eq ->] /=.
apply/setP ⇒ u. rewrite !inE /=. apply/andP/eqP ⇒ [[/orP[u_pi|u_qj] uA]|->].
+ move/(_ i u): (connector_left con_p). rewrite Ep /= u_pi uA. by apply.
+ suff ? : u = y.
{ subst. suff: lst (p i) = fst (p i) by rewrite Ep.
apply: (lst_idp con_p _). by rewrite !Ep. }
have Iq : irred qj. move: (conn_irred con_q j). by rewrite Eq.
case/(isplitP Iq) def_q : _ / u_qj ⇒ [q1 q2 _ _ I].
have zB : z \in B. { move: (connector_lst con_q j). by rewrite Eq. }
case: (sep_P _ _ q2) ⇒ // s sP in_q2.
have ? : s = y.
{ by rewrite [s](connector_left con_q (i := j)) // Eq // def_q mem_pcat in_q2. }
subst s. by rewrite [y]I // inE.
+ by rewrite inE /fst/= [x](_ : _ = fst (p i)) ?(connector_fst con_p) // Ep.
-
move ⇒ i. move: (pqE i) ⇒ [j] [x] [y] [z] [pi] [qj] [Ep Ej Eq ->] /=.
apply/setP ⇒ u. rewrite !inE /=. apply/andP/eqP ⇒ [[/orP[u_pi|u_qj] uB]|->].
+ have uz : u = y.
{ have Ip : irred pi. move: (conn_irred con_p i). by rewrite Ep.
case/(isplitP Ip) def_p : _ / u_pi ⇒ [p1 p2 _ _ I].
have xA : x \in A. { move: (connector_fst con_p i). by rewrite Ep. }
case: (sep_P _ _ p1) ⇒ // s sP in_p1.
have ? : s = y.
{ by rewrite [s](connector_right con_p (i := i)) // Ep // def_p mem_pcat in_p1. }
subst s. by rewrite [y]I // inE. }
subst u.
suff: fst (q j) = lst (q j). by rewrite Eq.
apply: (fst_idp con_q _). by rewrite Eq.
+ move/(_ j u): (connector_right con_q). rewrite Eq /= u_qj uB. by apply.
+ by rewrite inE /lst/= [z](_ : _ = lst (q j)) ?(connector_lst con_q) // Eq.
- move ⇒ i j iDj.
move: (pqE i) ⇒ [i2] [x] [y] [z] [pi] [qi2] [Ep Ei Eq ->] /=.
move: (pqE j) ⇒ [j2] [x'] [y'] [z'] [pj] [qj2] [Ep' Ej Eq' ->] /=.
apply/eqP. apply: wlog_neg. case/set0Pn ⇒ u. rewrite !inE ⇒ /andP[].
case/orP ⇒ Hi; case/orP ⇒ Hj; case: notF.
+ move/setP/(_ u): (conn_disjoint con_p iDj). by rewrite Ep Ep' !inE Hi Hj.
+ have uP : u \in P.
{ apply: (@connector_sep P A B _ p q i j2 u) ⇒ //; by rewrite ?Ep ?Eq'. }
have [? ?] : y' = u ∧ y = u.
{ split.
- by rewrite {1}[u](connector_left con_q (i := j2)) ?Eq'.
- by rewrite {1}[u](connector_right con_p (i := i)) ?Ep. }
subst y' y. apply: contraNT iDj ⇒ _. apply/eqP. apply: mtch_inj.
rewrite -Ei -Ej. apply: (connector_eq con_q (x := u)); by rewrite ?Eq ?Eq' inE.
+ have uP : u \in P.
{ apply: (@connector_sep P A B _ p q j i2 u) ⇒ // ; by rewrite ?Ep' ?Eq. }
have [? ?] : y' = u ∧ y = u.
{ split.
- by rewrite {1}[u](connector_right con_p (i := j)) ?Ep'.
- by rewrite {1}[u](connector_left con_q (i := i2)) ?Eq. }
subst y' y. apply: contraNT iDj ⇒ _. apply/eqP. apply: mtch_inj.
rewrite -Ei -Ej. apply: (connector_eq con_q (x := u)); by rewrite ?Eq ?Eq' inE.
+ apply: contraNT iDj ⇒ _. apply/eqP. apply: mtch_inj. rewrite -Ei -Ej.
apply: contraTeq isT ⇒ iDj.
move/setP/(_ u): (conn_disjoint con_q iDj). by rewrite Eq Eq' !inE Hi Hj.
Qed.
Lemma trivial_connector A B : ∃ p : 'I_#|A :&: B| → pathS G, connector A B p.
Proof.
∃ (fun i ⇒ PathS (idp (enum_val i))). split.
- move ⇒ i /=. exact: irred_idp.
- move ⇒ i /=. case/setIP : (enum_valP i) ⇒ iA iB. apply/setP ⇒ z.
rewrite !inE /= mem_idp. case e: (_ == _) ⇒ //. by rewrite (eqP e).
- move ⇒ i /=. case/setIP : (enum_valP i) ⇒ iA iB. apply/setP ⇒ z.
rewrite !inE /= mem_idp. case e: (_ == _) ⇒ //. by rewrite (eqP e).
- move ⇒ i j. apply: contraNeq ⇒ /set0Pn [x /setIP[]].
by rewrite !inE /= !mem_idp ⇒ /eqP→ /eqP /enum_val_inj→.
Qed.
Lemma sub_connector A B n m (p : 'I_m → pathS G) :
n ≤ m → connector A B p → ∃ q : 'I_n → pathS G, connector A B q.
Proof.
move ⇒ n_leq_m conn_p. pose W := widen_ord n_leq_m. ∃ (fun i ⇒ p (W i)).
case: conn_p ⇒ C1 C2 C3 C4. split ⇒ // i j. exact:(C4 (W i) (W j)).
Qed.
End SeparatorConnector.
Arguments separatesP {G x y U}.
Section VSeparator.
Variable (G : sgraph).
Implicit Types (x y z u v : G) (S U V : {set G}).
Fact separates0P x y : reflect (separates x y set0) (~~ connect edge_rel x y).
Proof.
apply:(iffP idP) ⇒ [nconn_xy|].
- rewrite /separates !inE. split ⇒ // p. by rewrite Path_connect in nconn_xy.
- case ⇒ _ _ H. apply/negP. case/connect_irredP ⇒ p _. case: (H p) ⇒ z. by rewrite inE.
Qed.
TODO: this does not actually depend on G being simple
Lemma separatesNE x y (U : {set G}) :
x \notin U → y \notin U → ¬ separates x y U → connect (restrict [predC U] edge_rel) x y.
Proof.
move ⇒ xU yU /(introN separatesP). rewrite /separatesb xU yU !negb_and //= negb_forall.
case: (altP (x =P y)) ⇒ [<-|xDy H]; first by rewrite connect0.
apply/connect_irredRP ⇒ //. case/existsP : H ⇒ p Hp. ∃ p ⇒ //.
exact/subsetP/(exists_inPn Hp).
Qed.
Definition vseparator U := ∃ x y, separates x y U.
Lemma vseparatorNE U x y : ¬ vseparator U → ¬ separates x y U.
Proof. move ⇒ nsepU sepU. by apply nsepU; ∃ x; ∃ y. Qed.
Lemma svseparator_connected S :
smallest vseparator S → 0 < #|S| → connected [set: G].
Proof.
move ⇒ SS gt0 x y _ _.
have: (connect (restrict [predC set0] sedge) x y).
{ apply (@separatesNE x y set0); rewrite ?inE ⇒ //. rewrite -(@cards0 G) in gt0.
move: (below_smallest SS gt0). exact: vseparatorNE. }
rewrite !restrictE //; intro; rewrite !inE //.
Qed.
x \notin U → y \notin U → ¬ separates x y U → connect (restrict [predC U] edge_rel) x y.
Proof.
move ⇒ xU yU /(introN separatesP). rewrite /separatesb xU yU !negb_and //= negb_forall.
case: (altP (x =P y)) ⇒ [<-|xDy H]; first by rewrite connect0.
apply/connect_irredRP ⇒ //. case/existsP : H ⇒ p Hp. ∃ p ⇒ //.
exact/subsetP/(exists_inPn Hp).
Qed.
Definition vseparator U := ∃ x y, separates x y U.
Lemma vseparatorNE U x y : ¬ vseparator U → ¬ separates x y U.
Proof. move ⇒ nsepU sepU. by apply nsepU; ∃ x; ∃ y. Qed.
Lemma svseparator_connected S :
smallest vseparator S → 0 < #|S| → connected [set: G].
Proof.
move ⇒ SS gt0 x y _ _.
have: (connect (restrict [predC set0] sedge) x y).
{ apply (@separatesNE x y set0); rewrite ?inE ⇒ //. rewrite -(@cards0 G) in gt0.
move: (below_smallest SS gt0). exact: vseparatorNE. }
rewrite !restrictE //; intro; rewrite !inE //.
Qed.
vseparators do not make precises what the separated comonents are,
i.e., a vseparator can disconnect the graph into more than two
components. Hence, we also define separations, which make the
separated sides explicit
Definition separation V1 V2 :=
((∀ x, x \in V1 :|: V2) × (∀ x1 x2, x1 \notin V2 → x2 \notin V1 → x1 -- x2 = false))%type.
Lemma sep_inR x V1 V2 : separation V1 V2 → x \notin V1 → x \in V2.
Proof. move ⇒ sepV. by case/setUP : (sepV.1 x) ⇒ →. Qed.
Lemma sep_inL x V1 V2 : separation V1 V2 → x \notin V2 → x \in V1.
Proof. move ⇒ sepV. by case/setUP : (sepV.1 x) ⇒ →. Qed.
Definition proper_separation V1 V2 := separation V1 V2 ∧ ∃ x y, x \notin V2 ∧ y \notin V1.
Lemma separate_nonadjacent x y : x != y → ~~ x -- y → proper_separation [set¬ x] [set¬ y].
Proof.
move ⇒ xDy xNy. split; last by ∃ y; ∃ x; rewrite !inE !eqxx.
split ⇒ [z | x1 x2].
- rewrite !inE -negb_and. by apply: contraNN xDy ⇒ /andP[/eqP->/eqP->].
- rewrite !inE !negbK sg_sym ⇒ /eqP→ /eqP→. by rewrite (negbTE xNy).
Qed.
Lemma separation_separates x y V1 V2:
separation V1 V2 → x \notin V2 → y \notin V1 → separates x y (V1 :&: V2).
Proof.
move ⇒ sepV Hx Hy. split; rewrite ?inE ?negb_and ?Hx ?Hy //.
move ⇒ p.
case: (@split_at_first G (mem V2) x y p y) ⇒ // ; rewrite ?(sep_inR sepV) //.
move ⇒ z [p1 [p2 [H1 H2 H3]]]. rewrite inE in H2.
∃ z; rewrite ?H1 !inE ?H2 // andbT.
case: (@splitR G x z p1) ⇒ [|z0 [p1' [z0z H4]]].
{ by apply: contraTneq H2 ⇒ <-. }
apply: contraTT (z0z) ⇒ Hz1. rewrite sepV ?inE //.
apply: contraTN (z0z) ⇒ H0. by rewrite [z0]H3 ?sgP // H4 !inE.
Qed.
Lemma proper_vseparator V1 V2 :
proper_separation V1 V2 → vseparator (V1 :&: V2).
Proof.
case ⇒ Hsep [x] [y] [Hx Hy]. ∃ x. ∃ y. exact: separation_separates.
Qed.
Lemma vseparator_separation S :
vseparator S → ∃ V1 V2, proper_separation V1 V2 ∧ S = V1 :&: V2.
Proof.
case ⇒ x1 [x2] [S1 S2 P12].
set U := locked [set x | connect (restrict [predC S] sedge) x1 x].
set V1 := U :|: S. set V2 := ~: U. ∃ V1; ∃ V2.
have D : x1 != x2.
{ apply/negP ⇒ /eqP A. subst x2. case: (P12 (idp x1)) ⇒ ?.
rewrite mem_idp ⇒ /eqP→ ?. contrab. }
have HU x : x \in U → x \notin S.
{ rewrite /U -lock inE srestrict_sym. case/connectP ⇒ [[/= _ <- //|/= y p]].
rewrite inE /=. by case: (x \in S). }
split; first split; first split.
- move ⇒ x. rewrite !inE. by case: (x \in U).
- move ⇒ u v. rewrite !inE !(negb_or,negb_and,negbK) ⇒ [Hu] /andP [Hv1 Hv2].
apply: contraNF Hv1 ⇒ uv. move: (Hu). rewrite /U -lock !inE ⇒ H.
apply: connect_trans H _. apply: connect1. by rewrite /= !inE HU.
- ∃ x1; ∃ x2; split.
+ suff H: (x1 \in U) by rewrite !inE H.
by rewrite /U -lock inE connect0.
+ rewrite !inE negb_or S2 (_ : x2 \notin U = true) //.
apply: contraTN isT. rewrite /U -lock inE ⇒ /connect_irredRP.
case ⇒ [//|p Ip /subsetP subS].
case: (P12 p) ⇒ z /subS. rewrite inE /= ⇒ ×. contrab.
- apply/setP ⇒ x. rewrite !inE. case E: (x \in U) ⇒ //=.
by rewrite (negbTE (HU _ _)).
Qed.
Definition vseparatorb U := [∃ x, ∃ y, separatesb x y U].
Lemma vseparatorP U : reflect (vseparator U) (vseparatorb U).
Proof. rewrite /vseparator /vseparatorb.
apply: (iffP existsP).
- move ⇒ [x /existsP [y /separatesP H]]. ∃ x; ∃ y; done.
- move ⇒ [x [y H]]. ∃ x. apply /existsP. ∃ y. by apply /separatesP.
Qed.
Lemma minimal_separation x y : x != y → ~~ x -- y →
∃ V1 V2, proper_separation V1 V2 ∧ smallest vseparator (V1 :&: V2).
Proof.
move ⇒ xDy xNy.
move/proper_vseparator/vseparatorP : (separate_nonadjacent xDy xNy) ⇒ sep.
case: (arg_minP (fun S ⇒ #|S|) sep) ⇒ U /vseparatorP sepU HU {sep xDy xNy}.
move: (vseparator_separation sepU) ⇒ [V1 [V2 [ps UV]]].
∃ V1; ∃ V2. repeat split ⇒ //; rewrite -UV // ⇒ V /vseparatorP. exact: HU.
Qed.
Lemma separation_sym V1 V2 : separation V1 V2 ↔ separation V2 V1.
Proof.
wlog suff W : V1 V2 / separation V1 V2 → separation V2 V1. { split; exact: W. }
move ⇒ sepV. split ⇒ [x|x1 x2 A B]; by rewrite 1?setUC 1?sgP sepV.
Qed.
Lemma proper_separation_symmetry V1 V2 :
proper_separation V1 V2 ↔ proper_separation V2 V1.
Proof. rewrite /proper_separation separation_sym. by firstorder. Qed.
Lemma svseparator_neighbours V1 V2 s :
proper_separation V1 V2 → smallest vseparator (V1 :&: V2) →
s \in V1 :&: V2 → ∃ x1 x2, [/\ x1 \notin V2, x2 \notin V1, s -- x1 & s -- x2].
Proof.
wlog: V1 V2 / [∀ x1, (x1 \notin V2) ==> ~~ s -- x1].
{ move ⇒ H ps ss sS.
case (boolP [∀ x1, (x1 \notin V2) ==> ~~ s -- x1]).
- move ⇒ HH. apply (H V1 V2) ⇒ //.
- move ⇒ /forall_inPn [x1 x1V /negPn sx1].
case (boolP [∀ x, (x \notin V1) ==> ~~ s -- x]).
+ move ⇒ HH. rewrite setIC in sS ss. case (H V2 V1) ⇒ //.
× by apply proper_separation_symmetry.
× move ⇒ y [z [? ? ? ?]]. ∃ z; ∃ y. split; done.
+ move ⇒ /forall_inPn [x2 x2V sx2].
∃ x1; ∃ x2. split ⇒ //; by apply negbNE. }
move ⇒ /forall_inP Hwlog [sepV [x1] [x2] [x1V12 x2V21]] smallS sS.
pose S' := V1 :&: V2:\ s.
suff: vseparator S'.
- move ⇒ sS'. case: (below_smallest (V := S') smallS) ⇒ //.
by rewrite /S' (cardsD1 s (V1 :&: V2)) sS.
-
∃ x1; ∃ x2. split; try by rewrite /S' notinD.
+ move ⇒ p.
case: (@split_at_first G (mem V2) x1 x2 p x2) ⇒ //.
{ by rewrite (sep_inR sepV x2V21). }
move ⇒ z [p1 [p2 [H1 H2 H3]]]. rewrite inE in H2.
∃ z; first by rewrite H1 !inE.
case: (@splitR G x1 z p1).
{ apply: contraTN isT ⇒ /eqP ?. subst x1; contrab. }
move ⇒ z0 [p' [z0z Hp']].
have z0V1: z0 \notin V2.
{ apply: contraTN (z0z) ⇒ ?. by rewrite [z0]H3 ?sgP // Hp' !inE. }
rewrite !inE H2 andbT. apply/andP; split.
× apply: contraTN (z0z) ⇒ /eqP→. by rewrite sgP Hwlog.
× apply: contraTT (z0z) ⇒ ?. by rewrite sepV.
Qed.
((∀ x, x \in V1 :|: V2) × (∀ x1 x2, x1 \notin V2 → x2 \notin V1 → x1 -- x2 = false))%type.
Lemma sep_inR x V1 V2 : separation V1 V2 → x \notin V1 → x \in V2.
Proof. move ⇒ sepV. by case/setUP : (sepV.1 x) ⇒ →. Qed.
Lemma sep_inL x V1 V2 : separation V1 V2 → x \notin V2 → x \in V1.
Proof. move ⇒ sepV. by case/setUP : (sepV.1 x) ⇒ →. Qed.
Definition proper_separation V1 V2 := separation V1 V2 ∧ ∃ x y, x \notin V2 ∧ y \notin V1.
Lemma separate_nonadjacent x y : x != y → ~~ x -- y → proper_separation [set¬ x] [set¬ y].
Proof.
move ⇒ xDy xNy. split; last by ∃ y; ∃ x; rewrite !inE !eqxx.
split ⇒ [z | x1 x2].
- rewrite !inE -negb_and. by apply: contraNN xDy ⇒ /andP[/eqP->/eqP->].
- rewrite !inE !negbK sg_sym ⇒ /eqP→ /eqP→. by rewrite (negbTE xNy).
Qed.
Lemma separation_separates x y V1 V2:
separation V1 V2 → x \notin V2 → y \notin V1 → separates x y (V1 :&: V2).
Proof.
move ⇒ sepV Hx Hy. split; rewrite ?inE ?negb_and ?Hx ?Hy //.
move ⇒ p.
case: (@split_at_first G (mem V2) x y p y) ⇒ // ; rewrite ?(sep_inR sepV) //.
move ⇒ z [p1 [p2 [H1 H2 H3]]]. rewrite inE in H2.
∃ z; rewrite ?H1 !inE ?H2 // andbT.
case: (@splitR G x z p1) ⇒ [|z0 [p1' [z0z H4]]].
{ by apply: contraTneq H2 ⇒ <-. }
apply: contraTT (z0z) ⇒ Hz1. rewrite sepV ?inE //.
apply: contraTN (z0z) ⇒ H0. by rewrite [z0]H3 ?sgP // H4 !inE.
Qed.
Lemma proper_vseparator V1 V2 :
proper_separation V1 V2 → vseparator (V1 :&: V2).
Proof.
case ⇒ Hsep [x] [y] [Hx Hy]. ∃ x. ∃ y. exact: separation_separates.
Qed.
Lemma vseparator_separation S :
vseparator S → ∃ V1 V2, proper_separation V1 V2 ∧ S = V1 :&: V2.
Proof.
case ⇒ x1 [x2] [S1 S2 P12].
set U := locked [set x | connect (restrict [predC S] sedge) x1 x].
set V1 := U :|: S. set V2 := ~: U. ∃ V1; ∃ V2.
have D : x1 != x2.
{ apply/negP ⇒ /eqP A. subst x2. case: (P12 (idp x1)) ⇒ ?.
rewrite mem_idp ⇒ /eqP→ ?. contrab. }
have HU x : x \in U → x \notin S.
{ rewrite /U -lock inE srestrict_sym. case/connectP ⇒ [[/= _ <- //|/= y p]].
rewrite inE /=. by case: (x \in S). }
split; first split; first split.
- move ⇒ x. rewrite !inE. by case: (x \in U).
- move ⇒ u v. rewrite !inE !(negb_or,negb_and,negbK) ⇒ [Hu] /andP [Hv1 Hv2].
apply: contraNF Hv1 ⇒ uv. move: (Hu). rewrite /U -lock !inE ⇒ H.
apply: connect_trans H _. apply: connect1. by rewrite /= !inE HU.
- ∃ x1; ∃ x2; split.
+ suff H: (x1 \in U) by rewrite !inE H.
by rewrite /U -lock inE connect0.
+ rewrite !inE negb_or S2 (_ : x2 \notin U = true) //.
apply: contraTN isT. rewrite /U -lock inE ⇒ /connect_irredRP.
case ⇒ [//|p Ip /subsetP subS].
case: (P12 p) ⇒ z /subS. rewrite inE /= ⇒ ×. contrab.
- apply/setP ⇒ x. rewrite !inE. case E: (x \in U) ⇒ //=.
by rewrite (negbTE (HU _ _)).
Qed.
Definition vseparatorb U := [∃ x, ∃ y, separatesb x y U].
Lemma vseparatorP U : reflect (vseparator U) (vseparatorb U).
Proof. rewrite /vseparator /vseparatorb.
apply: (iffP existsP).
- move ⇒ [x /existsP [y /separatesP H]]. ∃ x; ∃ y; done.
- move ⇒ [x [y H]]. ∃ x. apply /existsP. ∃ y. by apply /separatesP.
Qed.
Lemma minimal_separation x y : x != y → ~~ x -- y →
∃ V1 V2, proper_separation V1 V2 ∧ smallest vseparator (V1 :&: V2).
Proof.
move ⇒ xDy xNy.
move/proper_vseparator/vseparatorP : (separate_nonadjacent xDy xNy) ⇒ sep.
case: (arg_minP (fun S ⇒ #|S|) sep) ⇒ U /vseparatorP sepU HU {sep xDy xNy}.
move: (vseparator_separation sepU) ⇒ [V1 [V2 [ps UV]]].
∃ V1; ∃ V2. repeat split ⇒ //; rewrite -UV // ⇒ V /vseparatorP. exact: HU.
Qed.
Lemma separation_sym V1 V2 : separation V1 V2 ↔ separation V2 V1.
Proof.
wlog suff W : V1 V2 / separation V1 V2 → separation V2 V1. { split; exact: W. }
move ⇒ sepV. split ⇒ [x|x1 x2 A B]; by rewrite 1?setUC 1?sgP sepV.
Qed.
Lemma proper_separation_symmetry V1 V2 :
proper_separation V1 V2 ↔ proper_separation V2 V1.
Proof. rewrite /proper_separation separation_sym. by firstorder. Qed.
Lemma svseparator_neighbours V1 V2 s :
proper_separation V1 V2 → smallest vseparator (V1 :&: V2) →
s \in V1 :&: V2 → ∃ x1 x2, [/\ x1 \notin V2, x2 \notin V1, s -- x1 & s -- x2].
Proof.
wlog: V1 V2 / [∀ x1, (x1 \notin V2) ==> ~~ s -- x1].
{ move ⇒ H ps ss sS.
case (boolP [∀ x1, (x1 \notin V2) ==> ~~ s -- x1]).
- move ⇒ HH. apply (H V1 V2) ⇒ //.
- move ⇒ /forall_inPn [x1 x1V /negPn sx1].
case (boolP [∀ x, (x \notin V1) ==> ~~ s -- x]).
+ move ⇒ HH. rewrite setIC in sS ss. case (H V2 V1) ⇒ //.
× by apply proper_separation_symmetry.
× move ⇒ y [z [? ? ? ?]]. ∃ z; ∃ y. split; done.
+ move ⇒ /forall_inPn [x2 x2V sx2].
∃ x1; ∃ x2. split ⇒ //; by apply negbNE. }
move ⇒ /forall_inP Hwlog [sepV [x1] [x2] [x1V12 x2V21]] smallS sS.
pose S' := V1 :&: V2:\ s.
suff: vseparator S'.
- move ⇒ sS'. case: (below_smallest (V := S') smallS) ⇒ //.
by rewrite /S' (cardsD1 s (V1 :&: V2)) sS.
-
∃ x1; ∃ x2. split; try by rewrite /S' notinD.
+ move ⇒ p.
case: (@split_at_first G (mem V2) x1 x2 p x2) ⇒ //.
{ by rewrite (sep_inR sepV x2V21). }
move ⇒ z [p1 [p2 [H1 H2 H3]]]. rewrite inE in H2.
∃ z; first by rewrite H1 !inE.
case: (@splitR G x1 z p1).
{ apply: contraTN isT ⇒ /eqP ?. subst x1; contrab. }
move ⇒ z0 [p' [z0z Hp']].
have z0V1: z0 \notin V2.
{ apply: contraTN (z0z) ⇒ ?. by rewrite [z0]H3 ?sgP // Hp' !inE. }
rewrite !inE H2 andbT. apply/andP; split.
× apply: contraTN (z0z) ⇒ /eqP→. by rewrite sgP Hwlog.
× apply: contraTT (z0z) ⇒ ?. by rewrite sepV.
Qed.
Note: This generalizes the corresponding lemma on checkpoints
Lemma avoid_nonseperator U x y : ¬ vseparator U → x \notin U → y \notin U →
exists2 p : Path x y, irred p & [disjoint p & U].
Proof.
move ⇒ nsep_u xU yU.
case: (altP (x =P y)) ⇒ [?|A];first subst y.
- ∃ (idp x); first exact: irred_idp.
rewrite (@eq_disjoint1 _ x) // ⇒ y. by rewrite mem_idp.
- have/separatesNE/connect_irredRP : ¬ separates x y U by apply vseparatorNE.
case ⇒ // p irr_p. rewrite -disjoint_subset. by ∃ p.
Qed.
Lemma svseparator_uniq x y S:
smallest vseparator S → separates x y S → S != set0 →
exists2 p : Path x y, irred p & ∃! z, z \in p ∧ z \in S.
Proof.
Abort.
Lemma separation_connected_same_component V1 V2:
separation V1 V2 → ∀ x0 x, x0 \notin V2 →
connect (restrict [predC (V1:&:V2)] sedge) x0 x → x \notin V2.
Proof.
set S := V1 :&: V2.
move ⇒ sepV x0 x x0NV2.
case: (boolP (x0==x)) ⇒ [/eqP ? | x0x]; first by subst x0.
case/(connect_irredRP x0x) ⇒ p _ /subsetP Hp.
case: (boolP(x \in V2)) ⇒ // xV2.
case: (@split_at_first G (mem V2) x0 x p x) ⇒ //.
move ⇒ z [p1 [p2 [H1 H2 H3]]]. rewrite inE /= in H2.
case: (altP (x0 =P z)) ⇒ ?; first by subst x0; contrab.
case: (@splitR G x0 z p1) ⇒ [|z0 [p1' [z0z H4]]] //.
apply: contraTT (z0z) ⇒ _. rewrite sepV //.
+ apply: contraTN (z0z) ⇒ z0V2. by rewrite [z0]H3 ?sgP // H4 !inE.
+ have ? : (z \notin S) by apply: Hp; rewrite H1 !inE. by subst S; set_tac.
Qed.
End VSeparator.
Arguments separator : clear implicits.
Arguments separatorb : clear implicits.
Lemma connector_nodes (T : finType) (e1 e2 : rel T) (A B : {set T}) :
∀ s (p : 'I_s → pathS (DiGraph e1)) (q : 'I_s → pathS (DiGraph e2)),
(∀ i, nodes (tagged (p i)) = nodes (tagged (q i)) :> seq T) →
@connector (DiGraph e1) A B s p → @connector (DiGraph e2) A B s q.
Proof.
set G1 := DiGraph e1. set G2 := DiGraph e2.
move ⇒ s p q Epq [C1 C2 C3 C4].
have Spq : ∀ i, [set x in p i] = [set x in q i].
{ move ⇒ i. apply/setP ⇒ z. by rewrite !inE !mem_path Epq. }
split.
- move ⇒ i /=. rewrite irredE -Epq -(@irredE G1). exact: C1.
- move ⇒ i /=. rewrite -Spq C2. f_equal.
move: (Epq i). case: (p i) ⇒ [[x y] pi]. case: (q i) ⇒ [[x' y'] qi].
rewrite /fst /=. rewrite !nodesE. by case.
- move ⇒ i /=. rewrite -Spq C3. f_equal.
move: (Epq i). case: (p i) ⇒ [[x y] pi]. case: (q i) ⇒ [[x' y'] qi].
rewrite /lst /= in pi qi ×. rewrite !nodesE ⇒ [[E1 E2]].
by rewrite -(path_last pi) -(path_last qi) /= E2 E1.
- move ⇒ i j /C4. by rewrite -!Spq.
Qed.
Lemma del_edge_connector (G : diGraph) (a b : G) (A B : {set G}) s (p : 'I_s → pathS (del_edge a b)) :
@connector (del_edge a b) A B s p → connector A B (fun i : 'I_s ⇒ del_edge_liftS (p i)).
Proof.
destruct G. apply: connector_nodes ⇒ i.
case: (p i) ⇒ [[x y] pi] /=. by rewrite !nodesE.
Qed.
exists2 p : Path x y, irred p & [disjoint p & U].
Proof.
move ⇒ nsep_u xU yU.
case: (altP (x =P y)) ⇒ [?|A];first subst y.
- ∃ (idp x); first exact: irred_idp.
rewrite (@eq_disjoint1 _ x) // ⇒ y. by rewrite mem_idp.
- have/separatesNE/connect_irredRP : ¬ separates x y U by apply vseparatorNE.
case ⇒ // p irr_p. rewrite -disjoint_subset. by ∃ p.
Qed.
Lemma svseparator_uniq x y S:
smallest vseparator S → separates x y S → S != set0 →
exists2 p : Path x y, irred p & ∃! z, z \in p ∧ z \in S.
Proof.
Abort.
Lemma separation_connected_same_component V1 V2:
separation V1 V2 → ∀ x0 x, x0 \notin V2 →
connect (restrict [predC (V1:&:V2)] sedge) x0 x → x \notin V2.
Proof.
set S := V1 :&: V2.
move ⇒ sepV x0 x x0NV2.
case: (boolP (x0==x)) ⇒ [/eqP ? | x0x]; first by subst x0.
case/(connect_irredRP x0x) ⇒ p _ /subsetP Hp.
case: (boolP(x \in V2)) ⇒ // xV2.
case: (@split_at_first G (mem V2) x0 x p x) ⇒ //.
move ⇒ z [p1 [p2 [H1 H2 H3]]]. rewrite inE /= in H2.
case: (altP (x0 =P z)) ⇒ ?; first by subst x0; contrab.
case: (@splitR G x0 z p1) ⇒ [|z0 [p1' [z0z H4]]] //.
apply: contraTT (z0z) ⇒ _. rewrite sepV //.
+ apply: contraTN (z0z) ⇒ z0V2. by rewrite [z0]H3 ?sgP // H4 !inE.
+ have ? : (z \notin S) by apply: Hp; rewrite H1 !inE. by subst S; set_tac.
Qed.
End VSeparator.
Arguments separator : clear implicits.
Arguments separatorb : clear implicits.
Lemma connector_nodes (T : finType) (e1 e2 : rel T) (A B : {set T}) :
∀ s (p : 'I_s → pathS (DiGraph e1)) (q : 'I_s → pathS (DiGraph e2)),
(∀ i, nodes (tagged (p i)) = nodes (tagged (q i)) :> seq T) →
@connector (DiGraph e1) A B s p → @connector (DiGraph e2) A B s q.
Proof.
set G1 := DiGraph e1. set G2 := DiGraph e2.
move ⇒ s p q Epq [C1 C2 C3 C4].
have Spq : ∀ i, [set x in p i] = [set x in q i].
{ move ⇒ i. apply/setP ⇒ z. by rewrite !inE !mem_path Epq. }
split.
- move ⇒ i /=. rewrite irredE -Epq -(@irredE G1). exact: C1.
- move ⇒ i /=. rewrite -Spq C2. f_equal.
move: (Epq i). case: (p i) ⇒ [[x y] pi]. case: (q i) ⇒ [[x' y'] qi].
rewrite /fst /=. rewrite !nodesE. by case.
- move ⇒ i /=. rewrite -Spq C3. f_equal.
move: (Epq i). case: (p i) ⇒ [[x y] pi]. case: (q i) ⇒ [[x' y'] qi].
rewrite /lst /= in pi qi ×. rewrite !nodesE ⇒ [[E1 E2]].
by rewrite -(path_last pi) -(path_last qi) /= E2 E1.
- move ⇒ i j /C4. by rewrite -!Spq.
Qed.
Lemma del_edge_connector (G : diGraph) (a b : G) (A B : {set G}) s (p : 'I_s → pathS (del_edge a b)) :
@connector (del_edge a b) A B s p → connector A B (fun i : 'I_s ⇒ del_edge_liftS (p i)).
Proof.
destruct G. apply: connector_nodes ⇒ i.
case: (p i) ⇒ [[x y] pi] /=. by rewrite !nodesE.
Qed.
Theorem Menger (G : diGraph) (A B : {set G}) s :
(∀ S, separator G A B S → s ≤ #|S|) → ∃ (p : 'I_s → pathS G), connector A B p.
Proof.
move: G s A B. elim/(size_ind num_edges) ⇒ G IH s A B min_s.
case: (boolP [∃ x : G, ∃ 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. ∃ 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 [∃ 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.
- ∃ (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. ∃ 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 ∃ x | by ∃ y | ∃ 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.
∃ 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. ∃ 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.
∃ 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. ∃ 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] : ∃ j, lst (X j) = x.
{ suff : x \in codom (fun j ⇒ lst (X j)) by case/mapP ⇒ j _ ->; ∃ 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] : ∃ i : 'I_s, fst (Y i) = y :> G.
{ suff : y \in codom (fun j ⇒ fst (Y j)) by case/mapP ⇒ j _ ->; ∃ 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.
Corollary theta (G : diGraph) (x y : G) s :
~~ x -- y → x != y →
(∀ S, separates x y S → s ≤ #|S|) →
∃ p : 'I_s → IPath x y, ∀ i j : 'I_s, i != j → independent (p i) (p j).
Proof.
move ⇒ xNy xDy min_s.
pose G' := digraph.induced (~: [set x;y]).
pose A := [set z : G' | x -- val z].
pose B := [set z : G' | val z -- y].
have sepAB S : separator G' A B S → separates x y [set val x | x in S].
{ move ⇒ sepS. apply: separatesI; split.
- apply/negP. case/imsetP ⇒ x' _ E. move: (valP x'). by rewrite !inE -E eqxx.
- apply/negP. case/imsetP ⇒ y' _ E. move: (valP y'). by rewrite !inE -E eqxx orbT.
- move ⇒ p Ip. case: (splitL p xDy) ⇒ a [xA] [p'] [Ep _].
have aDy : (a != y) by apply: contraNneq xNy ⇒ <-.
case: (splitR p' aDy) ⇒ b [q] [By] Ep'.
have Hq : {subset q ≤ ~: [set x;y]}.
{ subst. rewrite irred_edgeL irred_edgeR mem_pcat_edgeR (negbTE xDy) /= in Ip.
case/and3P : Ip ⇒ I1 I2 _ u. rewrite inE.
apply: contraTN. case/setU1P ⇒ [->//|]. by move/set1P→. }
have [Ha Hb] : a \in ~: [set x;y] ∧ b \in ~: [set x;y] by split; apply: Hq.
case: (@digraph.Path_to_induced G (~: [set x;y]) (Sub a Ha) (Sub b Hb) q Hq) ⇒ q' Eq.
case: (sepS _ _ q'); rewrite ?inE // ⇒ s0 in_S in_q'.
∃ (val s0); last exact: mem_imset. subst.
by rewrite !inE [_ \in q]mem_path -Eq map_f. }
have min_s' S : separator G' A B S → s ≤ #|S|.
{ move ⇒ HS.
rewrite -[#|S|](_ : #|[set val x | x in S]| = _) ?min_s ?card_imset //.
+ exact: sepAB.
+ exact: val_inj. }
have [p conn_p] := Menger min_s'.
have xA (i : 'I_s) : x -- val (fst (p i)).
{ move: (connector_fst conn_p i). by rewrite inE. }
have By (i : 'I_s) : val (lst (p i)) -- y.
{ move: (connector_lst conn_p i). by rewrite inE. }
have X (i : 'I_s) : { pi : @IPath G x y | interior pi = [set val x | x in p i] }.
{ case def_pi : (p i) ⇒ [[a b] /= pi]. rewrite -/(PathS pi) in def_pi ×.
case: (digraph.Path_from_induced pi) ⇒ pi' P1 P2.
have [? ?] : a = fst (p i) ∧ b = lst (p i) by rewrite def_pi.
subst.
set q := (pcat (edgep (xA i)) (pcat pi' (edgep (By i)))).
have Iq : irred q.
{ rewrite /q irred_edgeL irred_edgeR mem_pcat_edgeR negb_or xDy /=. apply/and3P;split.
- apply/negP ⇒ /P1. by rewrite !inE eqxx.
- apply/negP ⇒ /P1. by rewrite !inE eqxx orbT.
- rewrite irredE P2 map_inj_uniq; last exact: val_inj.
move: (conn_irred conn_p i). by rewrite -(@irredE G') [in irred _]def_pi. }
∃ (Sub q Iq).
apply/setP ⇒ u. apply/setDP/imsetP ⇒ [[U1 U2]|].
- move: (U2) U1. rewrite 4!inE negb_or mem_pcat_edgeL mem_pcat_edgeR ⇒ /andP [/negbTE→ /negbTE->] /=.
by rewrite mem_path P2 ⇒ /mapP.
- case ⇒ u' ⇒ U1' U2'. rewrite -in_setC U2' (valP u') !inE [_ \in pi'](_ : _ = true) //.
rewrite mem_path P2 mem_map //. exact: val_inj. }
∃ (fun i ⇒ sval (X i)).
+ move ⇒ i j iDj. apply/disjointP ⇒ u. rewrite (svalP (X i)) (svalP (X j)).
case/imsetP ⇒ u1 UP1 UE1. case/imsetP ⇒ u2 UP2 UE2.
have ? : u1 = u2 by apply: val_inj; congruence.
subst u2. by rewrite [i](connector_eq conn_p UP1 UP2) eqxx in iDj.
Qed.
In addition to the independent paths, we also get a function providing a
default vertex on each path
Fact theta_vertices (G : diGraph) (x y : G) s (p : 'I_s → IPath x y) :
x != y → ~~ x -- y →
∃ (f : 'I_s → G), ∀ i, f i \in interior (p i).
Proof.
move ⇒ xDy xNy.
suff S i : { s | s \in interior (p i) }.
{ ∃ (fun i ⇒ val (S i)) ⇒ i. exact: (svalP (S i)). }
case: (set_0Vmem (interior (p i))) ⇒ [I0|//].
exfalso. case: (interior0E xDy (valP (p i)) I0) ⇒ xy.
by rewrite xy in xNy.
Qed.
x != y → ~~ x -- y →
∃ (f : 'I_s → G), ∀ i, f i \in interior (p i).
Proof.
move ⇒ xDy xNy.
suff S i : { s | s \in interior (p i) }.
{ ∃ (fun i ⇒ val (S i)) ⇒ i. exact: (svalP (S i)). }
case: (set_0Vmem (interior (p i))) ⇒ [I0|//].
exfalso. case: (interior0E xDy (valP (p i)) I0) ⇒ xy.
by rewrite xy in xNy.
Qed.
Corollary independent_walks Lv Le (G : graph Lv Le) (a b : G) n :
a != b → (∀ E, eseparates a b E → n ≤ #|E|) →
exists2 W : 'I_n → seq (edge G),
∀ i, walk a b (W i) & ∀ i j, i != j → [disjoint W i & W j].
Proof.
move ⇒ aDb min_sep.
pose A := [set e : line_graph G | source e == a].
pose B := [set e : line_graph G | target e == b].
have sep E : separator _ A B E → n ≤ #|E|.
{ move ⇒ sep_E. apply: min_sep ⇒ w walk_w.
have Nw : ~~ nilp w. { case: w walk_w ⇒ //=. by rewrite (negbTE aDb). }
case: (line_of_walk walk_w Nw) ⇒ e1 [e2] [p] [P1 P2 P3].
case: (sep_E _ _ p) ⇒ [||e in_E in_p]; rewrite ?inE ?P1 ?P2 //.
∃ e ⇒ //. by rewrite mem_path P3 in in_p. }
case: (Menger sep) ⇒ X con_X. pose W i := nodes (tagged (X i)). ∃ W.
- move ⇒ i. rewrite /W.
case: (X i) (connector_fst con_X i) (connector_lst con_X i) ⇒ [[e1 e2] /= p].
rewrite /fst/lst/= !inE ⇒ /eqP<- /eqP <-. exact: walk_of_line.
- move ⇒ i j iDj. apply/disjointP ⇒ e. rewrite /W -!(@mem_path (line_graph G)).
move ⇒ in_i in_j. move/(_ i j e in_i in_j) : (connector_eq con_X) ⇒ E.
by rewrite E eqxx in iDj.
Qed.
The (natural) notion of a matching on digraphs - a set of ordered
pairs - is not a resonable notion of matching on simple graphs, where
we should use unordered pairs. Hence, we have two separate definitions
Definition dimatching (G : diGraph) (M : {set G × G}) :=
(∀ e, e \in M → e.1 -- e.2)
∧ {in M &, ∀ e1 e2 x, x \in [set e1.1;e1.2] → x \in [set e2.1 ; e2.2] → e1 = e2}.
Definition matching (G : sgraph) (M : {set {set G}}) :=
{subset M ≤ E(G) } ∧
{in M&, ∀ (e1 e2 : {set G}) (x:G), x \in e1 → x \in e2 → e1 = e2}.
Lemma connectorC_edge (G : diGraph) (A : {set G}) n (p : 'I_n → pathS G) i :
connector A (~: A) p →
∃ fl : fst (p i) -- lst (p i), p i = PathS (edgep fl).
Proof.
move ⇒ conn_p.
case def_q : (p i) ⇒ [[a b] /= q]. rewrite -/(PathS q) in def_q ×.
case: (irred_is_edge q).
- move: (conn_irred conn_p i). by rewrite def_q.
- case: (altP (a =P b)) ⇒ // ?; subst.
move: (connector_fst conn_p i) (connector_lst conn_p i).
by rewrite def_q !inE ⇒ →.
- move ⇒ z zq. rewrite !inE. case: (boolP (z \in A)) ⇒ [zA|zNA].
+ by rewrite [z](connector_left conn_p (i := i)) ?def_q // eqxx.
+ by rewrite {2}[z](connector_right conn_p (i := i)) ?def_q ?inE // eqxx.
- move ⇒ ab →. by ∃ ab.
Qed.
Definition dimatching_of (G : diGraph) n (p : 'I_n → pathS G) :=
[set (fst (p i),lst (p i)) | i : 'I_n].
Lemma connector_dimatching (G : diGraph) (A : {set G} ) n (p : 'I_n → pathS G) :
connector A (~:A) p → dimatching (dimatching_of p).
Proof.
move ⇒ con_p. split.
+ move ⇒ e. case/imsetP ⇒ i _ → /=.
by case: (connectorC_edge i con_p).
+ move ⇒ [a b] [a' b'] /imsetP [i _ [-> ->]] /imsetP [j _ [-> ->]] /= x /set2P [->|->].
× case/set2P; by [move/(fst_inj con_p) → | move/(fst_lst_eq con_p) ->].
× case/set2P; by [move/(lst_inj con_p) → | move/esym/(fst_lst_eq con_p) ->].
Qed.
Lemma card_dimatching_of (G : diGraph) A B n (p : 'I_n → pathS G) :
connector A B p → #|dimatching_of p| = n.
Proof.
move ⇒ con_p. rewrite /dimatching_of card_imset ?card_ord // ⇒ i j.
case. by move/(fst_inj con_p).
Qed.
Definition matching_of (G : diGraph) (M' : {set G × G}) :=
[set [set e.1;e.2] | e in M'].
Lemma matching_of_dimatching (G : sgraph) (A : {set G}) M :
dimatching M → @matching G (matching_of M).
Proof.
move ⇒ [M1 M2]. split.
- move ⇒ e. case/imsetP ⇒ x /M1 ? ?. apply/edgesP. by ∃ x.1; ∃ x.2.
- move ⇒ e1 e2 /imsetP [x X1 X2] /imsetP [y Y1 Y2] z. subst e1 e2.
move ⇒ Z1 Z2. by rewrite (M2 x y X1 Y1 z Z1 Z2).
Qed.
Lemma card_matching_of (G : diGraph) (M : {set G × G}) :
dimatching M → #|matching_of M| = #|M|.
Proof.
move ⇒ [? dim_M]. rewrite /matching_of card_in_imset //.
move ⇒ e1 e2 /= inM1 inM2 E. apply dim_M with e1.1 ⇒ //.
all: by rewrite -?E !inE eqxx.
Qed.
Theorem diHall (G : diGraph) A :
bipartition A → (∀ S : {set G}, S \subset A → #|S| ≤ #|NS(S)|) →
∃ M, dimatching M ∧ A = [set x.1 | x in M].
Proof.
move ⇒ bip_A N_A.
have sep_A S : separator G A (~:A) S → #|A| ≤ #|S|.
{ move ⇒ sep_S. rewrite -[#|A|](cardsID S).
apply: (@leq_trans (#|A :&: S| + #|NS(A :\: S)|)).
- by rewrite leq_add2l N_A // subsetDl.
- rewrite -cardsUI [X in _ + X]eq_card0 ?addn0.
+ apply: subset_leq_card. rewrite subUset subsetIr /=.
apply/subsetP ⇒ z /bigcupP [x /setDP[xA xNS]]; rewrite in_opn ⇒ xz.
have [|s inS] := sep_S _ _ (edgep xz) xA; first by rewrite inE -(bip_A _ _ xz).
rewrite mem_edgep ⇒ /pred2P [?|<- //]; subst; contrab.
+ move ⇒ z;rewrite !inE -andbA;apply/negbTE/negP.
move ⇒ /and3P [zA zS /bigcupP [x /setDP [xA xS] xz]].
rewrite in_opn in xz. by rewrite (bip_A _ _ xz) zA in xA . }
case: (Menger sep_A) ⇒ p con_p. clear sep_A bip_A.
∃ (dimatching_of p). split; first exact: connector_dimatching con_p.
apply/setP ⇒ a. apply/idP/imsetP ⇒ [inA|[x]].
+ move: (inj_card_onto_pred (f := fun i ⇒ fst (p i)) (P := (mem A))) ⇒ /=.
case/(_ _ _ _ _ inA)/Wrap ⇒ //.
× apply: fst_inj con_p.
× apply: connector_fst con_p.
× by rewrite card_ord.
× case/mapP ⇒ i _ →. ∃ (fst (p i),lst (p i)) ⇒ //. by rewrite mem_imset.
+ case/imsetP ⇒ i _ → /= →. apply: connector_fst. exact: con_p.
Qed.
Theorem Hall (G : sgraph) A :
bipartition A → (∀ S : {set G}, S \subset A → #|S| ≤ #|NS(S)|) →
∃ M, matching M ∧ A \subset cover M.
Proof.
move ⇒ bip_A N_A. case: (@diHall G A) ⇒ [//|//|M' [M1 M2]].
- case: M1 ⇒ M1 M1'. ∃ (matching_of M').
split; first exact: matching_of_dimatching.
rewrite M2. apply/subsetP ⇒ a. case/imsetP ⇒ e E1 E2. apply/bigcupP.
∃ [set e.1; e.2]; last by rewrite E2 !inE eqxx. exact: mem_imset.
Qed.
Section vcover.
Variables (G : sgraph) (V :{set G}).
Definition vcover := [∀ x, ∀ (y | x -- y), (x \in V) || (y \in V)].
Lemma vcoverP : reflect (∀ x y, x -- y → (x \in V) ∨ (y \in V)) vcover.
Proof.
apply: (equivP idP).
rewrite /vcover -(rwP forallP).
setoid_rewrite <- (rwP forall_inP).
by setoid_rewrite <- (rwP orP).
Qed.
Lemma matching_cover_map (x0 : G) M :
matching M → vcover →
exists2 f : {set G} → G, (∀ e : {set G}, e \in M → f e \in V :&: e) & {in M&, injective f}.
Proof.
move ⇒ [M1 M2] cover_V.
pose f (A : {set G}) := if [pick x | x \in V :&: A] is Some x then x else x0.
have fP e : e \in M → f e \in V :&: e.
{ move/M1. case/edgesP ⇒ x [y] [E xy].
rewrite /f. case: pickP ⇒ [//|].
case/(vcoverP cover_V) : xy ⇒ xV;
[move/(_ x)|move/(_ y)]; by rewrite E !inE xV eqxx ?orbT. }
∃ f ⇒ // e1 e2 eM1 eM2.
move: (eM1) (eM2) ⇒ /fP /setIP [V1 E1] /fP /setIP [V2 E2] E.
apply M2 with (f e1) ⇒ //. by rewrite E.
Qed.
Lemma cover_matching (M :{set {set G}}) :
matching M → vcover → #|M| ≤ #|V|.
Proof.
move ⇒ [M1 M2] cover_V.
wlog [x0] : / inhabited G.
{ move ⇒ W. case: (set_0Vmem M) ⇒ [->|[e /M1]]; first by rewrite cards0.
case/edgesP ⇒ x _. exact: W. }
case: (matching_cover_map x0 (conj M1 M2) cover_V) ⇒ f F1 F2.
have f_V e : e \in M → f e \in V by move/F1 ⇒ /setIP[].
rewrite -(card_in_image F2). apply: subset_leq_card.
apply/subsetP ⇒ y /mapP [x Hx ->]. apply: f_V. by rewrite mem_enum in Hx.
Qed.
Proposition min_max_cover (M : {set {set G}}) :
vcover → matching M → #|M| = #|V| → V \subset cover M.
Proof.
move ⇒ cov_V match_V MV.
wlog [x0] : / inhabited G.
{ move ⇒ W. case: (set_0Vmem V) ⇒ [-> //|[x _]]; first by rewrite sub0set.
exact: W. }
case: (matching_cover_map x0 match_V cov_V) ⇒ f F1 F2.
pose f' (e : { e | e \in M}) := f (val e).
have inj_f' : injective f'.
{ case ⇒ e1 M1. case ⇒ e2 M2. rewrite /f' /= ⇒ E.
apply/eqP. change (e1 == e2). by rewrite (F2 _ _ M1 M2 E). }
move: (inj_card_onto_pred (P := (mem V)) inj_f') ⇒ /=. case/(_ _ _)/Wrap.
- case ⇒ e inM. by case/setIP : (F1 _ inM).
- by rewrite card_sig.
- move ⇒ X. apply/subsetP ⇒ v vV. case/mapP : (X _ vV) ⇒ /= [[e inM] _ E].
apply/bigcupP. ∃ e ⇒ //. rewrite E /f' /=. by case/setIP : (F1 _ inM).
Qed.
End vcover.
Prenex Implicits vcover.
Prenex Implicits matching.
Lemma bip_separation_vcover (G : sgraph) (A S : {set G}) :
bipartition A → separator G A (~: A) S → vcover S.
Proof.
move ⇒ bip_A sep_S. apply/vcoverP ⇒ x y xy.
wlog/andP [xA yNA] : x y xy / (x \in A) && (y \notin A).
{ move: (bip_A x y xy). case: (boolP (y \in A)) ⇒ /= yA xA; last by apply.
rewrite or_comm. apply; by rewrite 1?sgP ?xA ?yA. }
move: (sep_S _ _ (edgep xy)). rewrite xA inE yNA. case ⇒ // s sS.
rewrite mem_edgep ⇒ /orP [/eqP<-|/eqP<-]; by tauto.
Qed.
Lemma min_vcover_matching (G : sgraph) (A V : {set G}) :
bipartition A → smallest vcover V →
exists2 M, @matching G M & #|V| = #|M|.
Proof.
move ⇒ bip_A [cover_V min_V].
have sep_A S : separator G A (~:A) S → #|V| ≤ #|S|.
{ move/bip_separation_vcover ⇒ /(_ bip_A). exact: min_V. }
case: (Menger sep_A) ⇒ p conn_p.
move/connector_dimatching : (conn_p) ⇒ dim_M.
∃ (matching_of (dimatching_of p)). exact: matching_of_dimatching.
by rewrite card_matching_of // (card_dimatching_of conn_p).
Qed.
Theorem Konig (G : sgraph) (A V : {set G}) (M : {set {set G}}) :
bipartition A → smallest vcover V → largest matching M → #|V| = #|M|.
Proof.
move ⇒ bip_A [cov_V min_V] [match_M max_M]. apply/eqP.
rewrite eqn_leq cover_matching // andbT.
case: (min_vcover_matching (V := V) bip_A _) ⇒ // M' H →. exact: max_M.
Qed.
matching M → vcover →
exists2 f : {set G} → G, (∀ e : {set G}, e \in M → f e \in V :&: e) & {in M&, injective f}.
Proof.
move ⇒ [M1 M2] cover_V.
pose f (A : {set G}) := if [pick x | x \in V :&: A] is Some x then x else x0.
have fP e : e \in M → f e \in V :&: e.
{ move/M1. case/edgesP ⇒ x [y] [E xy].
rewrite /f. case: pickP ⇒ [//|].
case/(vcoverP cover_V) : xy ⇒ xV;
[move/(_ x)|move/(_ y)]; by rewrite E !inE xV eqxx ?orbT. }
∃ f ⇒ // e1 e2 eM1 eM2.
move: (eM1) (eM2) ⇒ /fP /setIP [V1 E1] /fP /setIP [V2 E2] E.
apply M2 with (f e1) ⇒ //. by rewrite E.
Qed.
Lemma cover_matching (M :{set {set G}}) :
matching M → vcover → #|M| ≤ #|V|.
Proof.
move ⇒ [M1 M2] cover_V.
wlog [x0] : / inhabited G.
{ move ⇒ W. case: (set_0Vmem M) ⇒ [->|[e /M1]]; first by rewrite cards0.
case/edgesP ⇒ x _. exact: W. }
case: (matching_cover_map x0 (conj M1 M2) cover_V) ⇒ f F1 F2.
have f_V e : e \in M → f e \in V by move/F1 ⇒ /setIP[].
rewrite -(card_in_image F2). apply: subset_leq_card.
apply/subsetP ⇒ y /mapP [x Hx ->]. apply: f_V. by rewrite mem_enum in Hx.
Qed.
Proposition min_max_cover (M : {set {set G}}) :
vcover → matching M → #|M| = #|V| → V \subset cover M.
Proof.
move ⇒ cov_V match_V MV.
wlog [x0] : / inhabited G.
{ move ⇒ W. case: (set_0Vmem V) ⇒ [-> //|[x _]]; first by rewrite sub0set.
exact: W. }
case: (matching_cover_map x0 match_V cov_V) ⇒ f F1 F2.
pose f' (e : { e | e \in M}) := f (val e).
have inj_f' : injective f'.
{ case ⇒ e1 M1. case ⇒ e2 M2. rewrite /f' /= ⇒ E.
apply/eqP. change (e1 == e2). by rewrite (F2 _ _ M1 M2 E). }
move: (inj_card_onto_pred (P := (mem V)) inj_f') ⇒ /=. case/(_ _ _)/Wrap.
- case ⇒ e inM. by case/setIP : (F1 _ inM).
- by rewrite card_sig.
- move ⇒ X. apply/subsetP ⇒ v vV. case/mapP : (X _ vV) ⇒ /= [[e inM] _ E].
apply/bigcupP. ∃ e ⇒ //. rewrite E /f' /=. by case/setIP : (F1 _ inM).
Qed.
End vcover.
Prenex Implicits vcover.
Prenex Implicits matching.
Lemma bip_separation_vcover (G : sgraph) (A S : {set G}) :
bipartition A → separator G A (~: A) S → vcover S.
Proof.
move ⇒ bip_A sep_S. apply/vcoverP ⇒ x y xy.
wlog/andP [xA yNA] : x y xy / (x \in A) && (y \notin A).
{ move: (bip_A x y xy). case: (boolP (y \in A)) ⇒ /= yA xA; last by apply.
rewrite or_comm. apply; by rewrite 1?sgP ?xA ?yA. }
move: (sep_S _ _ (edgep xy)). rewrite xA inE yNA. case ⇒ // s sS.
rewrite mem_edgep ⇒ /orP [/eqP<-|/eqP<-]; by tauto.
Qed.
Lemma min_vcover_matching (G : sgraph) (A V : {set G}) :
bipartition A → smallest vcover V →
exists2 M, @matching G M & #|V| = #|M|.
Proof.
move ⇒ bip_A [cover_V min_V].
have sep_A S : separator G A (~:A) S → #|V| ≤ #|S|.
{ move/bip_separation_vcover ⇒ /(_ bip_A). exact: min_V. }
case: (Menger sep_A) ⇒ p conn_p.
move/connector_dimatching : (conn_p) ⇒ dim_M.
∃ (matching_of (dimatching_of p)). exact: matching_of_dimatching.
by rewrite card_matching_of // (card_dimatching_of conn_p).
Qed.
Theorem Konig (G : sgraph) (A V : {set G}) (M : {set {set G}}) :
bipartition A → smallest vcover V → largest matching M → #|V| = #|M|.
Proof.
move ⇒ bip_A [cov_V min_V] [match_M max_M]. apply/eqP.
rewrite eqn_leq cover_matching // andbT.
case: (min_vcover_matching (V := V) bip_A _) ⇒ // M' H →. exact: max_M.
Qed.