Library GraphTheory.cp_minor
From mathcomp Require Import all_ssreflect.
Require Import edone preliminaries digraph sgraph minor checkpoint.
Require Import connectivity excluded set_tac.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Set Bullet Behavior "Strict Subproofs".
Require Import edone preliminaries digraph sgraph minor checkpoint.
Require Import connectivity excluded set_tac.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Set Bullet Behavior "Strict Subproofs".
Combined Minor and Checkpoint Properties
Lemma collapse_bags (U : {set G}) u0' (inU : u0' \in U) :
let T := U :|: ~: \bigcup_(x in U) bag U x in
let G' := sgraph.induced T in
∃ phi : G → G',
[/\ total_minor_map phi,
(∀ u : G', val u \in T :\: U → phi @^-1 u = [set val u]) &
(∀ u : G', val u \in U → phi @^-1 u = bag U (val u))].
Proof.
move ⇒ T G'.
have inT0 : u0' \in T by rewrite !inE inU.
pose u0 : G' := Sub u0' inT0.
pose phi u := if [pick x in U | u \in bag U x] is Some x
then insubd u0 x else insubd u0 u.
∃ phi.
have phiU (u : G') : val u \in U → phi @^-1 u = bag U (val u).
{ move ⇒ uU. apply/setP ⇒ z. rewrite !inE /phi.
case: pickP ⇒ [x /andP [X1 X2]|H].
- rewrite -val_eqE insubdK ?inE ?X1 //. apply/eqP/idP ⇒ [<-//|].
apply: contraTeq ⇒ C.
suff S: [disjoint bag U x & bag U (val u)] by rewrite (disjointFr S).
apply: bag_disj ⇒ //; exact: CP_extensive.
- move: (H (val u)). rewrite uU /= ⇒ →.
have zU : z \notin U. { move: (H z). by rewrite bag_id andbT ⇒ →. }
have zT : z \in T.
{ rewrite !inE (negbTE zU) /=. apply/negP ⇒ /bigcupP [x xU xP].
move: (H x). by rewrite xU xP. }
rewrite -val_eqE insubdK //. by apply: contraNF zU ⇒ /eqP→. }
have phiT (u : G') : val u \in T :\: U → phi @^-1 u = [set val u].
{ move/setDP ⇒ [uT uU]. apply/setP ⇒ z. rewrite !inE /phi.
case: pickP ⇒ [x /andP [xU xP]|H].
- rewrite -val_eqE insubdK ?inE ?xU // (_ : z == val u = false).
+ by apply: contraNF uU ⇒ /eqP <-.
+ apply: contraTF uT ⇒ /eqP ?. subst.
rewrite inE (negbTE uU) /= inE negbK. by apply/bigcupP; ∃ x.
- have zU : z \notin U. { move: (H z). by rewrite bag_id andbT ⇒ →. }
have zT : z \in T.
{ rewrite !inE (negbTE zU) /=. apply/negP ⇒ /bigcupP [x xU xP].
move: (H x). by rewrite xU xP. }
by rewrite -val_eqE insubdK. }
have preim_G' (u : G') : val u \in phi @^-1 u.
{ case: (boolP (val u \in U)) ⇒ H; first by rewrite phiU // bag_id.
rewrite phiT ?set11 // inE H. exact: valP. }
split ⇒ //.
- split.
+ move ⇒ y. ∃ (val y). apply/eqP. case: (boolP (val y \in U)) ⇒ x_inU.
× by rewrite mem_preim phiU // bag_id.
× rewrite mem_preim phiT inE // x_inU. exact: valP.
+ move ⇒ y. case: (boolP (val y \in U)) ⇒ xU.
× rewrite phiU //. apply: connected_bag ⇒ //. exact: CP_extensive.
× rewrite phiT; first exact: connected1. rewrite inE xU. exact: valP.
+ move ⇒ x y xy. ∃ (val x); ∃ (val y). by rewrite !preim_G'.
Qed.
End CheckpointsAndMinors.
Arguments collapse_bags [G] conn_G U u0' _.
Neighbor Tree Lemma
Proposition 21(ii)
Definition igraph (G : sgraph) (x y : G) : sgraph := induced (interval x y).
Definition istart (G : sgraph) (x y : G) : igraph x y := Sub x (intervalL x y).
Definition iend (G : sgraph) (x y : G) : igraph x y := Sub y (intervalR x y).
Arguments add_edge : clear implicits.
Arguments igraph : clear implicits.
Arguments istart {G x y}.
Arguments iend {G x y}.
Lemma add_edge_induced_iso (G : sgraph) (S T : {set G})
(u v : induced S) (x y : induced T) :
S = T → val u = val x → val v = val y →
diso (add_edge (induced S) u v) (add_edge (induced T) x y).
Proof.
move⇒ eq_ST eq_ux eq_vy.
have SofT z : z \in T → z \in S by rewrite eq_ST.
have TofS z : z \in S → z \in T by rewrite eq_ST.
set g : induced T → induced S := fun z ⇒ Sub (val z) (SofT (val z) (valP z)).
set f : induced S → induced T := fun z ⇒ Sub (val z) (TofS (val z) (valP z)).
apply (@Diso'' (add_edge (induced S) _ _) (add_edge (induced T) _ _) f g); rewrite {}/f {}/g.
- move ⇒ ?. exact: val_inj.
- move ⇒ ?. exact: val_inj.
- move ⇒ a b; rewrite /edge_rel /= /edge_rel /=.
rewrite -!(inj_eq val_inj) /=. by rewrite eq_ux eq_vy.
- move ⇒ a b. rewrite /edge_rel /= /edge_rel /=.
rewrite -!(inj_eq val_inj) /=. by rewrite eq_ux eq_vy.
Qed.
Definition istart (G : sgraph) (x y : G) : igraph x y := Sub x (intervalL x y).
Definition iend (G : sgraph) (x y : G) : igraph x y := Sub y (intervalR x y).
Arguments add_edge : clear implicits.
Arguments igraph : clear implicits.
Arguments istart {G x y}.
Arguments iend {G x y}.
Lemma add_edge_induced_iso (G : sgraph) (S T : {set G})
(u v : induced S) (x y : induced T) :
S = T → val u = val x → val v = val y →
diso (add_edge (induced S) u v) (add_edge (induced T) x y).
Proof.
move⇒ eq_ST eq_ux eq_vy.
have SofT z : z \in T → z \in S by rewrite eq_ST.
have TofS z : z \in S → z \in T by rewrite eq_ST.
set g : induced T → induced S := fun z ⇒ Sub (val z) (SofT (val z) (valP z)).
set f : induced S → induced T := fun z ⇒ Sub (val z) (TofS (val z) (valP z)).
apply (@Diso'' (add_edge (induced S) _ _) (add_edge (induced T) _ _) f g); rewrite {}/f {}/g.
- move ⇒ ?. exact: val_inj.
- move ⇒ ?. exact: val_inj.
- move ⇒ a b; rewrite /edge_rel /= /edge_rel /=.
rewrite -!(inj_eq val_inj) /=. by rewrite eq_ux eq_vy.
- move ⇒ a b. rewrite /edge_rel /= /edge_rel /=.
rewrite -!(inj_eq val_inj) /=. by rewrite eq_ux eq_vy.
Qed.
Lemma igraph_K4F (G : sgraph) (i o x y : G) :
connected [set: G] →
x \in cp i o → y \in cp i o → x != y →
K4_free (add_edge G i o) →
K4_free (add_edge (igraph G x y) istart iend).
Proof.
set H := add_edge G i o.
set I := add_edge _ _ _.
move⇒ G_conn x_cpio y_cpio xNy; apply: minor_K4_free.
have iNo : i != o.
{ apply: contra_neq xNy ⇒ x_y. move: x_cpio y_cpio.
by rewrite -{}x_y cpxx !inE =>/eqP->/eqP→. }
have conn_io : connect sedge i o := connectedTE G_conn i o.
wlog x_le_y : x y @I x_cpio y_cpio xNy / cpo conn_io x y.
{ move⇒ Hyp. case/orP: (cpo_total conn_io x y); first exact: Hyp.
move⇒ ?; suff : minor (add_edge (igraph G y x) istart iend) I.
{ by apply: minor_trans; apply: Hyp; rewrite // 1?sg_sym 1?eq_sym. }
apply: strict_is_minor; apply: iso_strict_minor.
setoid_rewrite add_edge_sym.
by apply: add_edge_induced_iso; first exact: interval_sym. }
pose U2 := [set x; y].
have [i_Px o_Py] : i \in bag U2 x ∧ o \in bag U2 y.
{ split; apply/bagP⇒ z; rewrite CP_set2 (cpo_cp x_cpio y_cpio x_le_y);
move⇒ /andP[z_cpio] /andP[x_le_z z_le_y].
+ rewrite (cpo_cp (mem_cpl i o) z_cpio);
repeat (apply/andP; split) ⇒ //; exact: cpo_min.
+ have o_cpio : o \in cp i o by rewrite cp_sym mem_cpl.
rewrite cp_sym (cpo_cp z_cpio o_cpio);
repeat (apply/andP; split) ⇒ //; exact: cpo_max. }
case: (collapse_bags G_conn U2 x _); first by rewrite !inE eqxx.
set T := U2 :|: _. have {T}-> : T = interval x y.
{ rewrite {}/T {-3}/U2 /interval bigcup_setU !bigcup_set1.
congr ([set x; y] :|: _).
rewrite -setTD (sinterval_bag_cover G_conn xNy).
rewrite setUAC setDUl setDv set0U; apply/setDidPl.
rewrite disjoint_sym disjoints_subset subUset -!disjoints_subset.
by rewrite {2}sinterval_sym !interval_bag_disj //;
apply: CP_extensive; rewrite !inE eqxx. }
rewrite -[induced _]/(igraph G x y). set Gxy := igraph G x y in I ×.
move⇒ phi [[phi_surj preim_phi_conn phi_edge] preim_phi preim_phixy].
apply: strict_is_minor. ∃ phi; split; first exact: phi_surj.
+ move⇒ u; have u_I : val u \in interval x y := valP u.
case: (boolP (val u \in U2)) ⇒ u_xy.
- rewrite preim_phixy //. apply: add_edge_connected.
apply: (@connected_bag G G_conn (val u) U2).
exact: CP_extensive.
- rewrite preim_phi; first exact: connected1.
by rewrite inE u_xy u_I.
+ move⇒ u v /orP[].
- move/phi_edge ⇒ [u'] [v'] [? ? uv'].
by ∃ u'; ∃ v'; split; rewrite /edge_rel //= uv'.
- wlog [-> → _] : u v / u = istart ∧ v = iend.
{ case/(_ istart iend); [ by split | by rewrite /= !eqxx xNy | ].
move⇒ u' [v'] [? ? ?]. have ? : v' -- u' by rewrite sg_sym.
case/orP⇒ /andP[_]/andP[/eqP->/eqP->];
[ by ∃ u'; ∃ v' | by ∃ v'; ∃ u' ]. }
rewrite 2?preim_phixy ?inE ?eqxx // ![val _]/=.
by ∃ i; ∃ o; split; rewrite /edge_rel //= iNo !eqxx.
Qed.
Lemma igraph_K4F_add_node (G : sgraph) (U : {set G}) :
connected [set: G] → ∀ x y, x \in CP U → y \in CP U → x != y →
K4_free (add_node G U) → K4_free (add_edge (igraph G x y) istart iend).
Proof.
set H := add_node G U ⇒ G_conn x y x_cp y_cp xy H_K4F.
set I := add_edge _ _ _.
case: (CP_base x_cp y_cp) ⇒ [i] [o] [i_U o_U].
rewrite subUset !sub1set =>/andP[x_cpio y_cpio].
suff : K4_free (add_edge G i o) by exact: igraph_K4F ⇒ //.
set K := add_edge G i o.
apply: minor_K4_free H_K4F. apply: strict_is_minor.
set phi : H → K := odflt i.
have preim_phi u :
phi @^-1 u = Some u |: if u == i then [set None] else set0.
{ by apply/setP⇒ v; case: ifP ⇒ u_i; rewrite -mem_preim !inE ?orbF;
case: v ⇒ [v|] //=; rewrite eq_sym. }
have preim_phixx u : Some u \in phi @^-1 u by rewrite -mem_preim.
∃ phi; split.
+ by move⇒ /= u; ∃ (Some u).
+ move⇒ /= u; rewrite preim_phi.
case: ifP ⇒ [/eqP{u}->|_]; first exact: connected2.
by rewrite setU0; exact: connected1.
+ move⇒ u v /orP[]; first by [ ∃ (Some u); ∃ (Some v); split ].
move⇒ /orP[]/andP[_]/andP[/eqP->/eqP->];
[ ∃ None; ∃ (Some o) | ∃ (Some o); ∃ None ];
by split; rewrite // -mem_preim.
Qed.
Lemma sepatates_cp (G : sgraph) (x y z : G) : separates x y [set z] → z \in cp x y :\: [set x; y].
Proof.
case. rewrite !inE ![z == _]eq_sym ⇒ /negbTE→ /negbTE→ /= H.
apply/cpP ⇒ p. by case: (H p) ⇒ z' Hz /set1P <-.
Qed.
TOTHINK: Make this the definition of the link relation? Is the
link relation realiy needed in the first place ?
Lemma link_rel_sep2 (G : sgraph) (x y : G) :
connected [set: G] → ~~ x -- y → link_rel x y →
x != y ∧ ∀ S, separates x y S → 2 ≤ #|S|.
Proof.
move ⇒ con_G xNy /andP [xDy cp_sub]. split ⇒ // S sep_xy.
case E : #|S| ⇒ [|[|//]].
- move/cards0_eq : E ⇒ E. subst S. move/connectedTE : con_G ⇒ /(_ x y).
apply: contraTT ⇒ _. exact/separates0P.
- move/eqP/cards1P : E ⇒ [z Hz]. subst. move/sepatates_cp in sep_xy. by set_tac.
Qed.
Lemma set_pred0 (T : finType) : @set0 T =i pred0.
Proof. move ⇒ z. by rewrite !inE. Qed.
Hint Resolve set_pred0 : core.
Lemma irred_in_sinterval (G : sgraph) (i o : G) (p : Path i o) :
irred p → {subset interior p ≤ sinterval i o}.
Proof.
move ⇒ Ip u. rewrite 5!inE negb_or -andbA ⇒ /and3P [U1 U2 U3].
case/(isplitP Ip) : U3 ⇒ {p Ip} p1 p2 Ip1 Ip2 I. apply/sintervalP2. split.
- ∃ (prev p1); rewrite ?irred_rev // inE. apply: contraNN U2 ⇒ in_p. by rewrite [o]I.
- ∃ p2 ⇒ //. apply: contraNN U1 ⇒ in_p. by rewrite [i]I.
Qed.
Open Scope implicit_scope.
Lemma ssplit_K4_nontrivial (G : sgraph) (i o : G) :
~~ i -- o → link_rel i o → K4_free (add_edge G i o) →
connected [set: G] → disconnected (sinterval i o).
Proof.
move ⇒ io1 L K4F conn_G. case: (link_rel_sep2 conn_G io1 L) ⇒ io2 io3 {L}.
case: (theta io1 io2 io3) ⇒ p indep_p.
case: (theta_vertices p io2 io1) ⇒ x in_p.
apply/disconnectedE ⇒ conn_io.
have in_io j : x j \in sinterval i o.
{ apply: irred_in_sinterval (in_p _). exact: valP. }
case: (path_in_connected conn_io (in_io ord0) (in_io ord1)) ⇒ q' Iq /subsetP sub_io.
case: (split_at_first (A := mem (interior (p ord1))) (p := q') (k := x ord1)).
all: try by [exact: in_p|].
move ⇒ x2 [q1'] [q2] [E Q1 Q2].
have Iq1 : irred q1'. move: Iq. rewrite E. by case/irred_catE.
apply: K4F.
case: (add_edge_Path i o (p ord0)) ⇒ p0 N0.
case: (add_edge_Path i o (p ord1)) ⇒ p1 N1.
case: (add_edge_Path i o q1') ⇒ q Nq.
have io : i -- o :> add_edge G i o by rewrite /edge_rel/= io2 !eqxx.
pose p2 := edgep io.
apply (@K4_of_paths (add_edge G i o)) with i o (x ord0) x2 p0 p1 p2 q ⇒ //.
- rewrite (independent_nodes N0 N1). exact: indep_p.
- by rewrite /independent interior_edgep disjoint_sym eq_disjoint0.
- by rewrite /independent interior_edgep disjoint_sym eq_disjoint0.
- by rewrite (interior_eq_nodes N0).
- by rewrite (interior_eq_nodes N1).
- rewrite (irred_eq_nodes N0). exact: valP.
- rewrite (irred_eq_nodes N1). exact: valP.
- exact: irred_edge.
- by rewrite (irred_eq_nodes Nq).
- apply/disjointP ⇒ z. rewrite (mem_eq_nodes Nq) ⇒ z_q1'. case/set2P ⇒ [?|?]; subst.
+ move: (sub_io i). by rewrite sinterval_bounds !inE z_q1' ⇒ /(_ isT).
+ move: (sub_io o). by rewrite sinterval_bounds !inE z_q1' ⇒ /(_ isT).
- move ⇒ z. rewrite (interior_edgep) inE /= in_set0 orbF (mem_eq_nodes Nq).
rewrite (interior_eq_nodes N1). exact: Q2.
Qed.
Close Scope implicit_scope.
connected [set: G] → ~~ x -- y → link_rel x y →
x != y ∧ ∀ S, separates x y S → 2 ≤ #|S|.
Proof.
move ⇒ con_G xNy /andP [xDy cp_sub]. split ⇒ // S sep_xy.
case E : #|S| ⇒ [|[|//]].
- move/cards0_eq : E ⇒ E. subst S. move/connectedTE : con_G ⇒ /(_ x y).
apply: contraTT ⇒ _. exact/separates0P.
- move/eqP/cards1P : E ⇒ [z Hz]. subst. move/sepatates_cp in sep_xy. by set_tac.
Qed.
Lemma set_pred0 (T : finType) : @set0 T =i pred0.
Proof. move ⇒ z. by rewrite !inE. Qed.
Hint Resolve set_pred0 : core.
Lemma irred_in_sinterval (G : sgraph) (i o : G) (p : Path i o) :
irred p → {subset interior p ≤ sinterval i o}.
Proof.
move ⇒ Ip u. rewrite 5!inE negb_or -andbA ⇒ /and3P [U1 U2 U3].
case/(isplitP Ip) : U3 ⇒ {p Ip} p1 p2 Ip1 Ip2 I. apply/sintervalP2. split.
- ∃ (prev p1); rewrite ?irred_rev // inE. apply: contraNN U2 ⇒ in_p. by rewrite [o]I.
- ∃ p2 ⇒ //. apply: contraNN U1 ⇒ in_p. by rewrite [i]I.
Qed.
Open Scope implicit_scope.
Lemma ssplit_K4_nontrivial (G : sgraph) (i o : G) :
~~ i -- o → link_rel i o → K4_free (add_edge G i o) →
connected [set: G] → disconnected (sinterval i o).
Proof.
move ⇒ io1 L K4F conn_G. case: (link_rel_sep2 conn_G io1 L) ⇒ io2 io3 {L}.
case: (theta io1 io2 io3) ⇒ p indep_p.
case: (theta_vertices p io2 io1) ⇒ x in_p.
apply/disconnectedE ⇒ conn_io.
have in_io j : x j \in sinterval i o.
{ apply: irred_in_sinterval (in_p _). exact: valP. }
case: (path_in_connected conn_io (in_io ord0) (in_io ord1)) ⇒ q' Iq /subsetP sub_io.
case: (split_at_first (A := mem (interior (p ord1))) (p := q') (k := x ord1)).
all: try by [exact: in_p|].
move ⇒ x2 [q1'] [q2] [E Q1 Q2].
have Iq1 : irred q1'. move: Iq. rewrite E. by case/irred_catE.
apply: K4F.
case: (add_edge_Path i o (p ord0)) ⇒ p0 N0.
case: (add_edge_Path i o (p ord1)) ⇒ p1 N1.
case: (add_edge_Path i o q1') ⇒ q Nq.
have io : i -- o :> add_edge G i o by rewrite /edge_rel/= io2 !eqxx.
pose p2 := edgep io.
apply (@K4_of_paths (add_edge G i o)) with i o (x ord0) x2 p0 p1 p2 q ⇒ //.
- rewrite (independent_nodes N0 N1). exact: indep_p.
- by rewrite /independent interior_edgep disjoint_sym eq_disjoint0.
- by rewrite /independent interior_edgep disjoint_sym eq_disjoint0.
- by rewrite (interior_eq_nodes N0).
- by rewrite (interior_eq_nodes N1).
- rewrite (irred_eq_nodes N0). exact: valP.
- rewrite (irred_eq_nodes N1). exact: valP.
- exact: irred_edge.
- by rewrite (irred_eq_nodes Nq).
- apply/disjointP ⇒ z. rewrite (mem_eq_nodes Nq) ⇒ z_q1'. case/set2P ⇒ [?|?]; subst.
+ move: (sub_io i). by rewrite sinterval_bounds !inE z_q1' ⇒ /(_ isT).
+ move: (sub_io o). by rewrite sinterval_bounds !inE z_q1' ⇒ /(_ isT).
- move ⇒ z. rewrite (interior_edgep) inE /= in_set0 orbF (mem_eq_nodes Nq).
rewrite (interior_eq_nodes N1). exact: Q2.
Qed.
Close Scope implicit_scope.