proposition: Lemma minor_with (H G': sgraph) (S : {set H}) (i : H) (N : {set G'}) (phi : (sgraph.induced S) -> option G') : i \notin S -> (forall y, y \in N -> exists2 x , x \in phi @^-1 (Some y) & val x -- i) -> @minor_map (sgraph.induced S) G' phi -> minor H (add_node G' N).
proof: Proof. move => Hi Hphi mm_phi. pose psi (u:H) : option (add_node G' N) := match @idP (u \in S) with | ReflectT p => obind (fun x => Some (Some x)) (phi (Sub u p)) | ReflectF _ => if u == i then Some None else None end. have psi_G' (a : G') : psi @^-1 (Some (Some a)) = val @: (phi @^-1 (Some a)). { apply/setP => x. rewrite !inE. apply/eqP/imsetP. + rewrite /psi. case: {-}_ / idP => p; last by case: ifP. case E : (phi _) => [b|//] /= [<-]. exists (Sub x p) => //. by rewrite !inE E. + move => [[/= b Hb] Pb] ->. rewrite /psi. case: {-}_ / idP => //= Hb'. rewrite !inE (bool_irrelevance Hb Hb') in Pb. by rewrite (eqP Pb). } have psi_None : psi @^-1 (Some None) = [set i]. { apply/setP => z. rewrite !inE /psi. case: {-}_ / idP => [p|_]; last by case: ifP. have Hz : z != i. { apply: contraNN Hi. by move/eqP <-. } case: (phi _) => [b|]; by rewrite (negbTE Hz). } case: mm_phi => M1 M2 M3. exists psi;split. - case. + move => a. case: (M1 a) => x E. exists (val x). apply/eqP. rewrite mem_preim psi_G' imset_f //. by rewrite !inE E. + exists i. rewrite /psi. move: Hi. case: {-}_ / idP => [? ?|_ _]; by [contrab|rewrite eqxx]. - case. + move => y. move: (M2 y). rewrite psi_G'. exact: connected_in_subgraph. + rewrite psi_None. exact: connected1. - move => [a|] [b|]; last by rewrite sg_irrefl. + move => /= /M3 [x0] [y0] [? ? ?]. exists (val x0). exists (val y0). by rewrite !psi_G' !imset_f. + move => /= /Hphi [x0] ? ?. exists (val x0); exists i. by rewrite psi_None set11 !psi_G' !imset_f. + move => /= /Hphi [x0] ? ?. exists i;exists (val x0). by rewrite sg_sym psi_None set11 !psi_G' !imset_f. Qed.
imports: Coq(RelationClasses) mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph) GraphTheory(sgraph treewidth set_tac)