proposition: Theorem TW2_of_K4F (G : sgraph) : K4_free G -> exists (T : forest) (B : T -> {set G}), sdecomp T G B /\ width B <= 3.
proof: Proof. elim/card_ind : G => G Hind K4free. case (no_K4_smallest_vseparator K4free) =>[|[S [ssepS Ssmall2]]]. { exact: decomp_small. } move: (vseparator_separation ssepS.1) => [V1 [V2 [[sep prop] SV12]]]. move: (prop) => [x0 [y0 [Hx0 Hy0]]]. case: (ltngtP #|S| 2) Ssmall2 => // [Sless2|/eqP Ssize2] _. - have V1properG: #|induced V1| < #|G|. { rewrite card_sig. eapply card_ltnT. simpl. eauto. } have {x0 Hx0 y0 Hy0} V2properG: #|induced V2| < #|G|. { rewrite card_sig. eapply card_ltnT. simpl. eauto. } case: (Hind (induced V1)) => // [|T1 [B1 [sd1 w1]]]. apply: subgraph_K4_free K4free; exact: induced_sub. case: (Hind (induced V2)) => // [|T2 [B2 [sd2 w2]]]. apply: subgraph_K4_free K4free; exact: induced_sub. have [|T[B [sdB wB]]] := separation_decomp sd1 sd2 sep _. by rewrite -SV12; exact: small_clique. by exists T,B; split => //; apply: leq_trans wB _; rewrite geq_max w1 w2. - case/cards2P : Ssize2 => s1 [s2] [s1Ns2 S12]; pose G' := add_edge s1 s2. suff [T[B [dcB wB]]] : exists (T : forest) (B : T -> {set G'}), sdecomp T G' B /\ width B <= 3. { exists T,B; split => //; move: dcB. destruct G; apply sdecomp_subrel. exact: subrelUl. } have V1properG: #|@induced G' V1| < #|G|. { rewrite card_sig. eapply card_ltnT. simpl. eauto. } have {x0 Hx0 y0 Hy0} V2properG: #|@induced G' V2| < #|G|. { rewrite card_sig. eapply card_ltnT. simpl. eauto. } case: (Hind (@induced G' V1)) => // [|T1 [B1 [sd1 w1]]]. { apply: (@add_edge_separation_excluded G s1 s2 V1 V2) => //. by rewrite -SV12 S12. by rewrite -SV12. } case: (Hind (@induced G' V2)) => // [|T2 [B2 [sd2 w2]]]. { apply: (@add_edge_separation_excluded G s1 s2 V2 V1) => //. - rewrite proper_separation_symmetry //. - by rewrite setIC -SV12 S12. - by rewrite setIC -SV12. } have [||T [B [sdB wB]]] := @separation_decomp G' _ _ _ _ _ _ sd1 sd2 _ _. by apply: add_edge_separation => //; rewrite -SV12 S12 !inE eqxx. by rewrite -SV12 S12; apply: clique2; rewrite /edge_rel/= !eqxx s1Ns2. by exists T,B; split => //; apply: leq_trans wB _; rewrite geq_max w1 w2. Qed.
imports: Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries set_tac digraph) GraphTheory(sgraph treewidth minor connectivity)