# Library GraphTheory.treewidth

Require Import RelationClasses.

From mathcomp Require Import all_ssreflect.
Require Import edone preliminaries digraph sgraph connectivity.
Require Import set_tac.

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Local Open Scope quotient_scope.
Set Bullet Behavior "Strict Subproofs".

# Tree Decompositions and treewidth

Covering is not really required, but makes the renaming theorem easier to state

Record sdecomp (T : forest) (G : sgraph) (B : T {set G}) := SDecomp
{ sbag_cover x : t, x \in B t;
sbag_edge x y : x -- y t, (x \in B t) && (y \in B t);
sbag_conn x t1 t2 : x \in B t1 x \in B t2
connect (restrict [pred t | x \in B t] sedge) t1 t2}.

Arguments sdecomp T G B : clear implicits.

Lemma sdecomp_subrel (V : finType) (e1 e2 : rel V) (T:forest) (D : T {set V})
(e1_sym : symmetric e1) (e1_irrefl : irreflexive e1)
(e2_sym : symmetric e2) (e2_irrefl : irreflexive e2):
subrel e2 e1
sdecomp T (SGraph e1_sym e1_irrefl) D
sdecomp T (SGraph e2_sym e2_irrefl) D.
Proof.
moveE [D1 D2 D3]. split ⇒ //=.
movex y /= xy. apply: D2 ⇒ /=. exact: E xy.
Qed.

Lemma sdecomp_tree_subrel
(G:sgraph) (V : finType) (D : V {set G}) (e1 e2 : rel V)
(e1_sym : symmetric e1) (e1_irrefl : irreflexive e1)
(e2_sym : symmetric e2) (e2_irrefl : irreflexive e2)
(e1_forest : is_forest [set: SGraph e1_sym e1_irrefl])
(e2_forest : is_forest [set: SGraph e2_sym e2_irrefl]):
subrel e1 e2
sdecomp (Forest e1_forest) G D sdecomp (Forest e2_forest) G D.
Proof.
movesub12 [D1 D2 D3]. split ⇒ // x t1 t2 X1 X2.
move: (D3 x _ _ X1 X2). apply: connect_mono.
moveu v /=. rewrite -!andbA ⇒ /and3P [-> → /=]. exact: sub12.
Qed.

Definition triv_sdecomp (G : sgraph) :
sdecomp tunit G (fun _[set: G]).
Proof.
split ⇒ [x|e|x [] [] _ _]; try by tt; rewrite !inE.
exact: connect0.
Qed.

Lemma decomp_iso (G1 G2 : sgraph) (T : forest) B1 :
sdecomp T G1 B1 diso G1 G2
exists2 B2, sdecomp T G2 B2 & width B2 = width B1.
Proof.
caseD1 D2 D3 [[g f can_g can_f] /= hom_g hom_f].
(fun t[set g x | x in B1 t]).
- split.
+ movex. case: (D1 (f x)) ⇒ t Ht. t.
apply/imsetP. by (f x).
+ movex y /hom_f /D2 [t] /andP [t1 t2].
t. by rewrite -[x]can_f -[y]can_f !mem_imset.
+ movex t1 t2 /imsetP [x1] X1 ? /imsetP [x2] X2 P. subst.
have ?: x1 = x2 by rewrite -[x1]can_g P can_g. subst ⇒ {P}.
have := D3 _ _ _ X1 X2.
apply: connect_monot t' /=.
rewrite !inE -andbA ⇒ /and3P [A B ->]. by rewrite !mem_imset.
- rewrite /width. apply: eq_bigri _. rewrite card_imset //.
apply: can_inj can_g.
Qed.

Definition triv_decomp (G : sgraph) :
sdecomp tunit G (fun _[set: G]).
Proof.
split ⇒ [x|e|x [] [] _ _]; try by tt; rewrite !inE.
exact: connect0.
Qed.

Lemma decomp_small (G : sgraph) k : #|G| k
T D, [/\ sdecomp T G D & width D k].
Proof.
tunit; (fun setT). split.
- exact: triv_decomp.
- by rewrite /width (big_pred1 tt _) // cardsT.
Qed.

## Renaming

Lemma rename_decomp (T : forest) (G H : sgraph) D (dec_D : sdecomp T G D) (h : G H) :
hom_s h
surjective h
( x y : H, x -- y x0 y0, [/\ h x0 = x, h y0 = y & x0 -- y0])
( x y, h x = h y
( t, (x \in D t) && (y \in D t)) ( t1 t2, [/\ t1 -- t2, x \in D t1 & y \in D t2]))
@sdecomp T _ (rename D h).
Proof.
movehom_h sur_h sur_e comp_h.
split.
- movex. pose x0 := iinv (sur_h x). case: (sbag_cover dec_D x0) ⇒ t Ht.
t. apply/imsetP. by x0; rewrite // f_iinv.
- movex y xy. case: (sur_e _ _ xy) ⇒ x0 [y0] [hx0 hy0 e0].
case: (sbag_edge dec_D e0) ⇒ t /andP [t1 t2].
t. apply/andP;split;apply/imsetP;by [ x0| y0].
- movex t0 t1 bg1 bg2.
case/imsetP : bg1 bg2x0 A B /imsetP [x1 C E]. subst.
have connT x t t' : x \in D t x \in D t'
connect (restrict [pred t | h x \in (rename D h) t] sedge) t t'.
{ moveHt Ht'.
apply: connect_mono (sbag_conn dec_D Ht Ht') ⇒ u v /= /andP [/andP [X Y] Z].
rewrite Z andbT. apply/andP;split; by apply/imsetP; x. }
case: (comp_h _ _ E).
+ caset /andP [F I].
apply: (connect_trans (y := t)); [exact: connT|rewrite E;exact:connT].
+ move ⇒ [t0'] [t1'] [t0t1 H0 H1].
apply: connect_trans (connT _ _ _ A H0) _.
rewrite E. apply: connect_trans (connect1 _) (connT _ _ _ H1 C).
by rewrite /= t0t1 !inE -{1}E !mem_imset.
Qed.

Lemma rename_width (T : forest) (G : sgraph) (D : T {set G}) (G' : finType) (h : G G') :
width (rename D h) width D.
Proof. apply: bigmax_leq_pointwiset _. exact: leq_imset_card. Qed.

## Disjoint Union

Section JoinT.
Variables (T1 T2 : forest).

Lemma sub_inl (a b : T1) (p : @Path (sjoin T1 T2) (inl a) (inl b)) :
{subset p codom inl}.
Proof.
apply: path_closed; first by rewrite codom_f.
do 2 case ⇒ ? //; rewrite ?codom_f //. by case/codomP ⇒ ?.
Qed.

Lemma sub_inr (a b : T2) (p : @Path (sjoin T1 T2) (inr a) (inr b)) :
{subset p codom inr}.
Proof.
apply: path_closed; first by rewrite codom_f.
do 2 case ⇒ ? //; rewrite ?codom_f //. by case/codomP ⇒ ?.
Qed.

Arguments inl_inj [A B].
Prenex Implicits inl_inj.

Lemma join_is_forest : is_forest [set: sjoin T1 T2].
Proof with try solve [exact: inl_inj|exact: inr_inj
|exact: sub_inl|exact: sub_inr].
move ⇒ [a|a] [b|b] p q [Ip _] [Iq _].
- case: (lift_Path (p' := p)) ⇒ //...
case: (lift_Path (p' := q)) ⇒ //...
movep' Np I q' Nq I'.
have E : p' = q'. { apply: forestP; by rewrite ?I ?I'. }
apply/eqP. by rewrite -nodes_eqE -Nq -E Np.
- move: (Path_connect p). by rewrite join_disc.
- move: (Path_connect p). by rewrite sconnect_sym join_disc.
- case: (lift_Path (p' := p)) ⇒ //...
case: (lift_Path (p' := q)) ⇒ //...
movep' Np I q' Nq I'.
have E : p' = q'. { apply: forestP; by rewrite ?I ?I'. }
apply/eqP. by rewrite -nodes_eqE -Nq -E Np.
Qed.

Definition tjoin := @Forest (sjoin T1 T2) join_is_forest.

Definition decompU (G1 G2 : sgraph) (D1 : T1 {set G1}) (D2 : T2 {set G2}) :
tjoin {set sjoin G1 G2} :=
[fun a match a with
| inl a[set inl x | x in D1 a]
| inr a[set inr x | x in D2 a]
end].

Lemma join_decomp (G1 G2 : sgraph) (D1 : T1 {set G1}) (D2 : T2 {set G2}) :
sdecomp T1 G1 D1 sdecomp T2 G2 D2 sdecomp tjoin (sjoin G1 G2) (decompU D1 D2).
Proof using.
movedec1 dec2. split.
- move ⇒ [x|x].
+ case: (sbag_cover dec1 x) ⇒ t Ht. (inl t) ⇒ /=. by rewrite mem_imset.
+ case: (sbag_cover dec2 x) ⇒ t Ht. (inr t) ⇒ /=. by rewrite mem_imset.
- move ⇒ [x|x] [y|y] // xy.
+ case: (sbag_edge dec1 xy) ⇒ t /andP [H1 H2]. (inl t) ⇒ /=. by rewrite !mem_imset.
+ case: (sbag_edge dec2 xy) ⇒ t /andP [H1 H2]. (inr t) ⇒ /=. by rewrite !mem_imset.
- have inl_inr x t : inl x \in decompU D1 D2 (inr t) = false.
{ rewrite /decompU /=. apply/negbTE/negP. by case/imsetP. }
have inr_inl x t : inr x \in decompU D1 D2 (inl t) = false.
{ rewrite /decompU /=. apply/negbTE/negP. by case/imsetP. }
move ⇒ [x|x] [t1|t1] [t2|t2] /= ; rewrite ?inl_inr ?inr_inl // ⇒ A B.
+ pose e := restrict [pred t | x \in D1 t] sedge.
apply: (homo_connect (e:= e) (f := inl)).
× movea b. rewrite /e /= !in_simpl -andbA ⇒ /and3P[? ? ?].
by rewrite !mem_imset.
× apply: sbag_conn ⇒ //.
move: A. by case/imsetP ⇒ ? ? [->].
move: B. by case/imsetP ⇒ ? ? [->].
+ pose e := restrict [pred t | x \in D2 t] sedge.
apply: (homo_connect (e:= e) (f := inr)).
× movea b. rewrite /e /= !in_simpl -andbA ⇒ /and3P[? ? ?].
by rewrite !mem_imset.
× apply: sbag_conn ⇒ //.
move: A. by case/imsetP ⇒ ? ? [->].
move: B. by case/imsetP ⇒ ? ? [->].
Qed.

Lemma join_width (G1 G2 : sgraph) (D1 : T1 {set G1}) (D2 : T2 {set G2}) :
width (decompU D1 D2) maxn (width D1) (width D2).
Proof.
apply/bigmax_leqP ⇒ [[x|x] _].
all: rewrite /decompU /= card_imset; try solve [exact: inl_inj|exact: inr_inj].
- apply: leq_trans (leq_maxl _ _). exact: leq_bigmax.
- apply: leq_trans (leq_maxr _ _). exact: leq_bigmax.
Qed.

End JoinT.

## Link Construction (without intermediate node)

Lemma add_edge_break (G : sgraph) (s1 s2 x y : G) (p : @Path (add_edge s1 s2) x y) :
s1 != s2
let U := [set s1;s2] in
irred p ~~ @connect G sedge x y
u v : G, q1 : Path x u, q2 : Path v y,
[/\ u \in U, v \in U, u != v & nodes p = nodes q1 ++ nodes q2].
Proof.
moveD U Ip NCxy.
have/andP [H1 H2] : (s1 \in p) && (s2 \in p).
{ rewrite -[_ && _]negbK negb_and. apply: contraNN NCxyH.
case: (add_edge_avoid p H) ⇒ p' Ep. exact: Path_connect. }
case: (@split_at_first (add_edge s1 s2) (mem U) _ _ p s1) ⇒ //.
{ by rewrite !inE eqxx. }
movez [p1] [p2] [P1 P2 P3]. subst U.
wlog ? : s1 s2 p D Ip NCxy H1 H2 z p1 p2 P1 P3 {P2 H1} / z = s1.
{ moveW. case/setUP : P2 ⇒ /set1P P2; subst z.
- by apply W with s1 p1 p2.
- case: (add_edge_pathC p) ⇒ p' Ep.
case: (add_edge_pathC p1) ⇒ p1' Ep1.
case: (add_edge_pathC p2) ⇒ p2' Ep2.
case: (W s2 s1 p' _ _ _ _ _ s2 p1' p2') ⇒ //.
+ by rewrite eq_sym.
+ by rewrite irredE Ep.
+ by rewrite (@mem_path G'') Ep -(@mem_path G').
+ by rewrite (@mem_path G'') Ep -(@mem_path G').
+ apply/eqP. by rewrite -nodes_eqE Ep P1 !nodes_pcat Ep1 Ep2.
+ movez. rewrite setUC. rewrite (@mem_path G'') Ep1 -(@mem_path G').
exact: P3.
+ moveu [v] [q1] [q2]. rewrite setUC ⇒ [[? ? ? E]].
u. v. q1. q2. split ⇒ //. congruence. }
subst. move: H2. rewrite (@mem_pcat (add_edge s1 s2)).
have {P3} s2p1 : s2 \notin p1. apply: contraNN DC. by rewrite [s2]P3 ?inE ?eqxx.
rewrite (negbTE s2p1) /= ⇒ s2p2. case/irred_catE : IpIp1 Ip2 Ip12.
case: (splitL p2) ⇒ [|z [s1z] [pR [def_p2 _]]].
{ apply: contraNneq D ⇒ ?;subst y.
move: s2p2. by rewrite [p2]irredxx // mem_idp eq_sym. }
move: Ip2. rewrite def_p2 irred_edgeL ⇒ /andP [s1pR IpR].
case: (add_edge_avoid p1) ⇒ [|p1' Ep]; first by rewrite s2p1.
case: (add_edge_avoid pR) ⇒ [|pR' ER]; first by rewrite s1pR.
have ? : z = s2.
{ apply: contraNeq NCxyzNs2. move: (s1z) ⇒ /=.
rewrite /edge_rel/= (negbTE zNs2) [z == s1]eq_sym (sg_edgeNeq s1z) ?eqxx.
case/or3P ⇒ //= s1z'.
exact: (Path_connect (pcat p1' (pcat (edgep s1z') pR'))). }
subst z. s1; s2; p1'; pR'. rewrite !inE ?eqxx. split ⇒ //.
rewrite Ep ER. by rewrite !nodesE.
Qed.

Lemma path_return (G : sgraph) z (A : {set G}) (x y : G) (p : Path x y) :
x \in A y \in A irred p
( u v, u -- v u \in A v \notin A u = z) p \subset A.
Abort.

Variables (T : forest) (t0 t1 : T).
Hypothesis discT : ~~ connect sedge t0 t1.

Let T' := add_edge t0 t1.
Notation Path G x y := (@Path G x y).

Lemma add_edge_is_forest : is_forest [set: T'].
Proof using discT.
apply: unique_forestTx y p q Ip Iq.
have D : t0 != t1 by apply: contraNneq discT ⇒ →.
case: (boolP (@connect T sedge x y)) ⇒ [|NC].
- case/connect_irredPr Ir. apply/eqP. rewrite -nodes_eqE.
wlog suff {q Iq} S : p Ip / nodes p = nodes r.
{ by rewrite (S p) ?(S q). }
suff S : (t0 \notin p) || (t1 \notin p).
{ case: (add_edge_avoid p S) ⇒ p' Ep.
by rewrite -Ep (@forestP _ _ _ p' r) // irredE Ep. }
rewrite -negb_and. apply:contraNN discT ⇒ /andP [T1 T2].
wlog before : x y p Ip D r Ir T1 T2 / t0 <[p] t1.
{ moveW. case: (ltngtP (idx p t0) (idx p t1)).
- by apply W with r.
- rewrite idx_swap //.
apply W with (prev r); rewrite ?prev_irred //.
all: by rewrite (@mem_prev (add_edge t0 t1)).
- move/idx_inj. rewrite -mem_path. by move/(_ T1)->. }
case:(three_way_split Ip T1 T2 before) ⇒ p1 [p2] [p3] [_ P2 P3].
case:(add_edge_avoid p1 _) ⇒ [|p1' _] ; first by rewrite P3.
case:(add_edge_avoid p3 _) ⇒ [|p3' _] ; first by rewrite P2.
exact: (Path_connect (pcat (prev p1') (pcat r (prev p3')))).
- case:(add_edge_break D Ip NC) ⇒ u [u'] [p1] [p2] [U1 U2 U3 E1].
wlog [? ?]: x y p q Ip Iq NC u u' p1 p2 E1 {U1 U2 U3} / u = t0 u' = t1.
{ moveW.
case/setUP : U1 ⇒ /set1P U1; case/setUP : U2 ⇒ /set1P U2; subst.
- by rewrite eqxx in U3.
- exact: (W x y p q _ _ _ t0 t1 p1 p2).
- have H := (W y x (prev p) (prev q) _ _ _ t0 t1 (prev p2) (prev p1)).
rewrite -[p]prevK H ?prevK ?prev_irred // 1?sconnect_sym //.
by rewrite !nodes_prev E1 rev_cat.
- by rewrite eqxx in U3. }
subst.
case:(add_edge_break D Iq NC) ⇒ v [v'] [q1] [q2] [V1 V2 V3 E2].
have {V1} V1 : v = t0.
{ apply: contraTeq V1H. rewrite !inE (negbTE H) /=.
apply: contraNneq discT ⇒ <-. exact: (Path_connect (pcat (prev p1) q1)). }
have {V2 V3} V2 : v' = t1.
{ subst. rewrite !inE eq_sym (negbTE V3) in V2. exact/eqP. }
subst. apply/eqP. rewrite -nodes_eqE E1 E2.
rewrite !irredE E1 E2 !cat_uniq in Ip Iq.
case/and3P : Ip ⇒ [? _ ?]. case/and3P : Iq ⇒ [? _ ?].
rewrite (@forestP _ _ _ p1 q1) 1?(@forestP _ _ _ p2 q2) //.
Qed.

## Link Construction (with intermediate node)

Variables (T : forest) (U : {set T}).
Hypothesis U_disc : {in U &, x y, x != y ~~ connect sedge x y}.

unique (fun p : Path x yirred p None \notin p).
Proof.
move: x y ⇒ [x|] [y|] p q [Ip Np] [Iq Nq];
gen have H,Hp : p Ip Np / {subset p codom Some}.
{ move ⇒ [u|]; by rewrite ?codom_f // (negbTE Np). }
case: (lift_Path (p' := p)) ⇒ //.
case: (lift_Path (p' := q)) ⇒ //; first exact: H.
movep0 Ep Ip0 q0 Eq Iq0.
have E : p0 = q0. apply: forestP; by rewrite ?Ip0 ?Iq0.
apply/eqP. rewrite -nodes_eqE. by apply/eqP;congruence.
Qed.

Lemma link_bypass (x y : T) (p : @Path link (Some x) (Some y)) :
x \in U y \in U None \notin p x = y.
Proof.
movexU yU Np. case: (lift_Path (p' := p)) ⇒ // ⇒ [|p' _ _].
{ move ⇒ [u|]; by rewrite ?codom_f // (negbTE Np). }
apply: contraTeq isT ⇒ /U_disc ⇒ /(_ xU yU).
by rewrite (Path_connect p').
Qed.

unique (fun p : @Path link None xirred p).
Proof.
move: x ⇒ [x|] p q Ip Iq; last by rewrite (irredxx Ip) (irredxx Iq).
case: (splitL p) ⇒ // [] [y|] [/= xy] [p'] [P1 _] //.
case: (splitL q) ⇒ // [] [z|] [/= xz] [q'] [Q1 _] //. subst.
move: Ip Iq. rewrite !irred_edgeL ⇒ /andP[Np Ip] /andP[Nq Iq].
have ? : y = z. {
apply: (link_bypass (p := pcat p' (prev q'))) ⇒ //.
by rewrite (@mem_pcat link) mem_prev negb_or Np Nq. }
subst. congr pcat; first exact: val_inj. exact: link_unique_lift.
Qed.

Lemma link_has_None (x y : link) (p q : Path x y) :
irred p irred q None \in p None \in q.
Proof using U_disc.
move: x y p q ⇒ [x|] [y|] p q;
moveIp Iq Np. apply: contraTT isTNq.
case/(isplitP Ip) def_p : _ / Np ⇒ [p1 p2 Ip1 Ip2 I12]. subst.
case: (splitL p2) ⇒ // [] [a|] [/= na] [p2'] [D _] //.
case: (splitL (prev p1)) ⇒ // [] [b|] [/= nb] [p1'] [D' _] //.
have ? : b = a; last subst.
{ suff [p Hp] : p : @Path link (Some b) (Some a), None \notin p.
(pcat p1' (pcat q (prev p2'))).
rewrite !(@mem_pcat link) mem_prev (negbTE Nq) /= negb_or.
move: Ip1 Ip2. rewrite -irred_rev D' D !irred_edgeL. by do 2 case: (_ \notin _). }
move: (I12 (Some a)). case/(_ _ _)/Wrap ⇒ //; rewrite ?mem_pcat ?path_end //.
by rewrite -mem_prev D' mem_pcat path_begin.
Qed.

Proof.
apply: unique_forestTx y p q Ip Iq.
case: (boolP (None \in p)) ⇒ Np.
- have Nq := link_has_None Ip Iq Np.
case/(isplitP Ip) def_p : _ / Np ⇒ [p1 p2 Ip1 Ip2 _].
case/(isplitP Iq) def_q : _ / Nq ⇒ [q1 q2 Iq1 Iq2 _].
congr pcat.
+ apply: prev_inj. apply: link_unique_None; by rewrite irred_rev.
- suff Nq : None \notin q by apply: link_unique_lift.
Qed.

Definition decompL (G:sgraph) (D : T {set G}) A a :=
match a with Some xD x | NoneA end.

Lemma decomp_link (G : sgraph) (D : T {set G}) (A : {set G}) :
A \subset \bigcup_(t in U) D t
sdecomp T G D @sdecomp tlink G (decompL D A).
Proof.
moveHA decD. split ⇒ //.
- movex. case: (sbag_cover decD x) ⇒ t Ht. by (Some t).
- movex y xy. case: (sbag_edge decD xy) ⇒ t Ht. by (Some t).
- have X x a : x \in D a x \in A
connect (restrict [pred t | x \in decompL D A t] (add_node_rel U))
(Some a) None.
{ moveH1 H2. move/(subsetP HA) : (H2) ⇒ /bigcupP [t Ht1 Ht2].
apply: (connect_trans (y := Some t)).
- move: (sbag_conn decD H1 Ht2). exact: homo_connect.
- apply: connect1 ⇒ /=; by rewrite !in_simpl H2 Ht1. }
movex [a|] [b|] /= H1 H2; last exact: connect0.
+ move: (sbag_conn decD H1 H2). exact: homo_connect.
+ exact: X.
+ rewrite (@srestrict_sym link). exact: X.
Qed.

Lemma width_link (G : sgraph) (D : T {set G}) (A : {set G}) :
width (decompL D A) maxn (width D) #|A|.
Proof.
apply/bigmax_leqP ⇒ [] [t|] _ /=; last by rewrite ?leq_maxr.
apply: leq_trans (leq_maxl _ _). exact: leq_bigmax.
Qed.

## Every clique is contained in some bag

Section DecompTheory.
Variables (G : sgraph) (T : forest) (B : T {set G}).
Implicit Types (t u v : T) (x y z : G).

Hypothesis decD : sdecomp T G B.

Arguments sbag_conn [T G B] dec x t1 t2 : rename.

This proof is based on a stackexchange post to be found here: https://math.stackexchange.com/questions/1227867/ a-clique-in-a-tree-decomposition-is-contained-in-a-bag
The assumption 0 < #|S| ensures that T is nonempty.
Lemma decomp_clique (S : {set G}):
0 < #|S| clique S t : T, S \subset B t.
Proof.
elim/card_ind : SS IH inh_S clique_S.
case: (leqP #|S| 1) ⇒ [card_S | card_S {inh_S}].
- have/cards1P [x ->] : #|S| == 1 by rewrite eqn_leq card_S.
case: (sbag_cover decD x) ⇒ t A. t. by rewrite sub1set.
- have [v [v0] [Hv Hv0 X]] := card_gt1P (card_S).
pose S0 := S :\ v.
pose T0 := [set t | S0 \subset B t].
wlog /forall_inP HT0 : / [ t in T0, v \notin B t].
{ case: (boolP [ _ in _,_]) ⇒ [H|/forall_inPn [t H1 /negPn H2] _]; first by apply.
t. rewrite inE in H1. by rewrite -(setD1K Hv) subUset sub1set H2 H1. }
have HT0' t : v \in B t ~~ (S0 \subset B t).
{ apply: contraTNC. apply: HT0. by rewrite inE. }
have pairs x y : x \in S y \in S t, x \in B t y \in B t.
{ movexS yS. case: (altP (x =P y)) ⇒ [?|xDy].
- subst y. case: (sbag_cover decD x) ⇒ t A. by t.
- move/clique_S : xDy. case/(_ _ _)/Wrap ⇒ // xy.
case: (sbag_edge decD xy) ⇒ t A. t. exact/andP. }

have [c [Hc1 Hc2]] : t, v \in B t v0 \in B t by apply: pairs.
pose C := [set t in [predC T0] | connect (restrict [predC T0] sedge) c t].
have inC: c \in C. { by rewrite !inE connect0 andbT HT0'. }
have con_C : connected C.
{ apply: connected_restrict_in. move: inC. rewrite inE. by case/andP. }
have dis_C : [disjoint C & T0].
{ rewrite disjoints_subset /C. apply/subsetPt. rewrite !inE. by case/andP. }
have [t0 [c0 [Ht0 Hc0 tc0]]] : t0 c0, [/\ t0 \in T0, c0 \in C & t0 -- c0].
{ have [t Ht] : t, S0 \subset B t.
{ case: (IH S0 _ _) ⇒ [|||t Ht]; last by t.
- by rewrite [#|S|](cardsD1 v) Hv.
- apply/card_gt0P. v0. by rewrite !inE eq_sym X.
- apply: sub_in2W clique_S; apply/subsetP; by rewrite subD1set. }
have A : v0 \in B t. { apply (subsetP Ht). by rewrite !inE eq_sym X. }
have/connect_irredRP [|p Ip _] := (sbag_conn decD v0 c t Hc2 A).
{ apply: contraTneq inC ⇒ →. by rewrite !inE Ht. }
move: (c) p Ip (inC). apply: irred_ind; first by rewrite !inE Ht.
movex z p xz Ip xp IHp xC.
case: (boolP (z \in C)) ⇒ [|zNC {IHp}] ; first exact: IHp.
z; x. rewrite sgP. split ⇒ //. apply: contraNT zNCH.
rewrite 2!inE /= in xC. case/andP : xCH1 H2.
rewrite 2!inE /= (negbTE H) /=. apply: connect_trans H2 _.
apply: connect1 ⇒ /=. by rewrite 2!inE H1 2!inE xz H. }

have t0P c' (p : Path t0 c') : irred p c' \in C c0 \in p.
{ moveIp inC'.
case: (altP (c0 =P c')) ⇒ [-> |?]. by rewrite path_end.
have/connect_irredRP [//|q Iq /subsetP subC] := con_C _ _ Hc0 inC'.
suff → : p = pcat (edgep tc0) q by rewrite mem_pcat path_end.
apply: forest_is_forest; (repeat split) ⇒ //.
rewrite irred_edgeL Iq andbT.
apply: contraTN Ht0 ⇒ /subCH. by rewrite (disjointFr dis_C H). }

suff A : c0 \in T0 by case: (disjointE dis_C Hc0 A).
rewrite inE. apply/subsetPu u_in_S0.
have Hu: u \in B t0. { rewrite inE in Ht0. exact: (subsetP Ht0). }
have [cu [Hcu1 Hcu2]] : t, u \in B t v \in B t.
{ apply: (pairs u v) ⇒ //. move: u_in_S0. rewrite inE. by case: (_ \notin _). }
case/connect_irredRP:(sbag_conn decD u t0 cu Hu Hcu1) ⇒ [|q irr_p /subsetP has_u].
{ apply: contraTneq Hcu2 ⇒ <-. exact: HT0. }
suff Hq : c0 \in q. { move/has_u : Hq. by rewrite inE. }
apply: t0P irr_p _. rewrite !inE /= HT0' //=.
move: (sbag_conn decD v c cu Hc1 Hcu2).
apply: connect_monot t' /=.
rewrite !inE -andbA ⇒ /and3P [*]. by rewrite !HT0'.
Qed.

End DecompTheory.
Arguments rename_decomp [T G H D].

decompositsions of 'K_m have width at least m

Lemma Km_bag m (T : forest) (D : T {set 'K_m.+1}) :
sdecomp T 'K_m.+1 D t, m.+1 #|D t|.
Proof.
movedecD.
case: (@decomp_clique _ _ _ decD setT _ _) ⇒ //.
- by rewrite cardsT card_ord.
- movet A. t. rewrite -{1}[m](card_ord m) -cardsT.
apply: leq_trans (subset_leq_card A). by rewrite !cardsT !card_ord.
Qed.

Lemma Km_width m (T : forest) (D : T {set 'K_m.+1}) :
sdecomp T 'K_m.+1 D m.+1 width D.
Proof. case/Km_bagt Ht. apply: leq_trans Ht _. exact: leq_bigmax. Qed.

Obtaining a tree decomposition from tree decompositions of (induced) subgraphs
Lemma separation_decomp (G:sgraph) (V1 V2 : {set G}) T1 T2 B1 B2 :
@sdecomp T1 (induced V1) B1 @sdecomp T2 (induced V2) B2
separation V1 V2 clique (V1 :&: V2)
T B, @sdecomp T G B width B maxn (width B1) (width B2).
Proof.
movedec1 dec2 sepV clV.
have dec12 := join_decomp dec1 dec2.
set G' := sjoin _ _ in dec12.
set T := tjoin T1 T2 in dec12.
set B : tjoin T1 T2 {set G'}:= decompU B1 B2 in dec12.
pose h (x : G') : G := match x with inl xval x | inr xval x end.
case: (boolP (0 < #|V1 :&: V2|)) ⇒ [cliquen0|clique0].
-
case/card_gt0P : cliquen0v0 /setIP [v01 v02].
have HVx (V : {set G}) : (V = V1) V = V2 v0 \in V
let V' := val @^-1: (V1 :&: V2) : {set induced V} in 0 < #|V'| clique V'.
{ moveHV xV /=. split.
- apply/card_gt0P; (Sub v0 xV). rewrite inE /=. case: HV ⇒ ?; by set_tac.
- moveu v. rewrite [_:&:_]lock !inE -lock -val_eqE. exact: clV. }
set S := V1 :&: V2 in HVx.
pose S1 := val @^-1: S : {set induced V1}.
pose S2 := val @^-1: S : {set induced V2}.
have [cln01 clS1] : 0 < #|S1| clique S1 by apply: HVx; auto.
have [cln02 clS2] : 0 < #|S2| clique S2 by apply: HVx; auto.
case: (decomp_clique dec1 cln01 clS1) ⇒ t1 Ht1.
case: (decomp_clique dec2 cln02 clS2) ⇒ t2 Ht2.
have dis_t1_t2 : ~~ connect (@sedge T)(inl t1) (inr t2) by rewrite join_disc.
set T' := Forest (add_edge_is_forest dis_t1_t2).
have dec12' : sdecomp T' G' B.
{ apply: sdecomp_tree_subrel dec12. exact: subrelUl. }
case/Wrap: (rename_decomp dec12' h). case/(_ _ _ _ _)/Wrap.
+ by move ⇒ [u|u] [v|v].
+ movev.
case/setUP : (sepV.1 v) ⇒ Hv; apply/codomP; by [ (inl (Sub v Hv))| (inr (Sub v Hv))].
+ movex y xy.
suff: x \in V1 y \in V1 x \in V2 y \in V2.
{ case ⇒ [[Hx Hy]|[Hx Hy]].
- by (inl (Sub x Hx)); (inl (Sub y Hy)).
- by (inr (Sub x Hx)); (inr (Sub y Hy)). }
case: (boolP (x \in V1));case: (boolP (y \in V1)) ⇒ Hy Hx;
first [by left|right; apply/andP].
× rewrite [y \in _](sep_inR sepV) // andbT.
apply: contraTT xyH. by rewrite sepV.
× rewrite [x \in _](sep_inR sepV) //=.
apply: contraTT xyH. by rewrite sgP sepV.
× by rewrite !(sep_inR sepV).
+ case: dec1dec1A dec1B dec1C. case: dec2dec2A dec2B dec2C.
have X (x : induced V1) (y : induced V2) : val x = val y
((inl x \in B (inl t1) = true) × (inr y \in B (inr t2) = true))%type.
{ moveExy. rewrite /B /decompU /= !mem_imset //.
- apply: (subsetP Ht2). rewrite !inE -{1}Exy.
apply/andP; split; exact: valP.
- apply: (subsetP Ht1). rewrite !inE {2}Exy.
apply/andP; split; exact: valP. }
move ⇒ [x|x] [y|y]; simpl h.
× move/val_inj ⇒ ?;subst y.
case: (dec1A x) ⇒ t Ht. left. (inl t).
by rewrite /B /decompU /= mem_imset.
× moveExy. right. (inl t1). (inr t2).
by rewrite /edge_rel/= !(X _ _ Exy) /= !eqxx.
× move/esymEyx. right. (inr t2). (inl t1).
by rewrite /edge_rel/= !(X _ _ Eyx) /= !eqxx.
× move/val_inj ⇒ ?;subst y.
case: (dec2A x) ⇒ t Ht. left. (inr t).
by rewrite /B /decompU /= mem_imset.
+ movedecRB. do 2 eexists. split. eapply decRB.
apply: leq_trans (rename_width _ _) _. exact: join_width.
-
suff iso: diso G' G.
+ case: (decomp_iso dec12 iso) ⇒ B' sdecB' wB'B.
T; B'. split ⇒ //. by rewrite wB'B join_width.
+ suff HH: V2 = ~:V1.
{ rewrite /G' HH. apply ssplit_disconnected. movex y xV1 yNV1.
rewrite (sepV.2 x y) ⇒ //. by rewrite HH inE xV1. }
apply/setPz. rewrite inE. case: (boolP (z \in V1)) ⇒ Hz.
× apply: contraNF clique0H. apply/card_gt0P. z. by set_tac.
× apply: contraTT (sepV.1 z). by set_tac.
Qed.

## Forests have treewidth 1

Lemma forest_vseparator (G : sgraph) :
is_forest [set: G] 3 #|G| exists2 S : {set G}, vseparator S & #|S| 1.
Proof.
moveforest_G card_G.
have {card_G} [x [y [xDy xy]]] := forest3 forest_G card_G.
have [/connect_irredP [p Ip]|nCxy]:= (boolP (connect sedge x y)).
move/forestT_unique in forest_G.
- have/set0Pn [z z_p] : interior p != set0.
{ apply: contraNneq xyIp0. by case: (interior0E xDy Ip Ip0). }
[set z]; last by rewrite cards1.
x; y; apply: separatesI.
move: (interiorN z_p); rewrite !inE negb_or ![z == _]eq_sym ⇒ /andP[-> ->].
split ⇒ // q Iq. z; rewrite ?inE ?eqxx //.
apply: interiorW. by rewrite (forest_G _ _ _ _ Iq Ip).
- set0; last by rewrite cards0. x; y. split; rewrite ?inE // ⇒ p.
case: notF. apply: contraNT nCxy_. exact: Path_connect p.
Qed.

Lemma forest_TW1 (G : sgraph) :
is_forest [set: G] T B, sdecomp T G B width B 2.
Proof.
elim/(size_ind (fun G : sgraph#|G|)) : GG Hind forest_G.
have:= forest_vseparator forest_G.
case: leqP ⇒ [Glt2 _|Ggt2 /(_ isT) [S sepS Slt2]]; first exact: decomp_small.
have [V1 [V2 [[sep [x0 [y0 [Hx0 Hy0]]]] SV12]]] := vseparator_separation sepS.
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. }
have C: clique (V1 :&: V2) by rewrite -SV12; exact: small_clique.
case: (Hind (induced V1)) ⇒ // [|T1 [B1 [sd1 w1]]].
{ apply: induced_forest. exact: sub_forest forest_G. }
case: (Hind (induced V2)) ⇒ // [|T2 [B2 [sd2 w2]]].
{ apply: induced_forest. exact: sub_forest forest_G. }
case separation_decomp with G V1 V2 T1 T2 B1 B2 ⇒ // T [B [sd w]].
T. B. split ⇒ //.
apply leq_trans with (maxn (width B1) (width B2)) ⇒ //.
by rewrite geq_max w1 w2.
Qed.