proposition: Lemma rename_sdecomp (T : forest) (G H : sgraph) D (dec_D : sdecomp T G D) (h :G -> H) : hom_s h -> surjective h -> edge_surjective h -> (forall x y, h x = h y -> exists t, (x \in D t) && (y \in D t)) -> @sdecomp T _ (rename D h).
proof: Proof. Abort. Lemma width_minor (G H : sgraph) (T : forest) (B : T -> {set G}) : sdecomp T G B -> minor G H -> exists B', @sdecomp T H B' /\ width B' <= width B. Proof. move => decT [phi [p1 p2 p3]]. pose B' t := [set x : H | [exists (x0 | x0 \in B t), phi x0 == Some x]]. exists B'. split. - split. + move => y. case: (p1 y) => x /eqP Hx. case: (sbag_cover decT x) => t Ht. exists t. apply/pimsetP. by exists x. + move => x y xy. move/p3: xy => [x0] [y0]. rewrite !inE => [[H1 H2 H3]]. case: (sbag_edge decT H3) => t /andP [T1 T2]. exists t. apply/andP; split; apply/pimsetP; by [exists x0|exists y0]. + have conn_pre1 t1 t2 x x0 : phi x0 == Some x -> x0 \in B t1 -> x0 \in B t2 -> connect (restrict [pred t | x \in B' t] sedge) t1 t2. { move => H1 H2 H3. move: (sbag_conn decT H2 H3). apply: connect_mono => u v /=. rewrite !in_simpl -!andbA => /and3P [? ? ?]. apply/and3P; split => //; apply/pimsetP; eexists; eauto. } move => x t1 t2 /pimsetP [x0 X1 X2] /pimsetP [y0 Y1 Y2]. move: (p2 x x0 y0). rewrite !inE. case/(_ _ _)/Wrap => // /connectP [p]. elim: p t1 x0 X1 X2 => /= [|z0 p IH] t1 x0 X1 X2. * move => _ E. subst x0. exact: conn_pre1 X1 Y1. * rewrite -!andbA => /and3P [H1 H2 /andP [H3 H4] H5]. case: (sbag_edge decT H3) => t /andP [T1 T2]. apply: (connect_trans (y := t)). -- move => {p IH H4 H5 y0 Y1 Y2 X2}. rewrite !inE in H1 H2. exact: conn_pre1 X1 T1. -- apply: IH H4 H5 => //. by rewrite inE in H2. - apply: bigmax_leq_pointwise => t _. exact: pimset_card. Qed.
imports: Coq(RelationClasses) mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph) GraphTheory(sgraph treewidth set_tac)