proposition: 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 exists phi : G -> G', [/\ total_minor_map phi, (forall u : G', val u \in T :\: U -> phi @^-1 u = [set val u]) & (forall u : G', val u \in U -> phi @^-1 u = bag U (val u))].
proof: 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. exists 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; exists 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. exists (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. exists (val x); exists (val y). by rewrite !preim_G'. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph sgraph minor) GraphTheory(checkpoint connectivity excluded set_tac)