proposition: Lemma K4_of_paths (G : sgraph) x y s0 s1' (p0 p1 p2 : Path x y) (q1 : Path s0 s1') : x!=y -> independent p0 p1 -> independent p0 p2 -> independent p1 p2 -> s0 \in interior p0 -> s1' \in interior p1 -> irred p0 -> irred p1 -> irred p2 -> irred q1 -> [disjoint q1 & [set x; y]] -> (forall z' : G, z' \in [predU interior p1 & interior p2] -> z' \in q1 -> z' = s1') -> minor G K4.
proof: Proof. move => xDy ind01 ind02 ind12 sp0 in_p1 Ip0 Ip1 Ip2 Iq av_xy s1'firstp12. pose phi (i : K4) := match i with | Ordinal 0 _ => [set x] | Ordinal 1 _ => interior p0 :|: interior q1 | Ordinal 2 _ => interior p1 | Ordinal 3 _ => y |: interior p2 | Ordinal p n => set0 end. suff: minor_rmap phi by apply minor_of_rmap. split. - move => [m i]. case m as [|[|[|[|m]]]] => //=; apply /set0Pn. + exists x. by set_tac. + exists (s0). by rewrite inE sp0. + by exists s1'. + exists y. by set_tac. - move => [m i]. case m as [|[|[|[|m]]]] => //=. + exact: connected1. + case: (altP (interior q1 =P set0)) => [->|H]. * rewrite setU0. exact: connected_interior. * apply: neighbor_connected; try exact: connected_interior. exact: path_neighborL. + exact: connected_interior. + exact: connected_interiorR. - move => i j iNj. wlog iltj: i j {iNj} / i < j. { move => H. rewrite /= neq_ltn in iNj. move: iNj => /orP [iltj|jlti]; [|rewrite disjoint_sym]; exact: H. } destruct i as [m i]. destruct j as [n j]. case m as [|[|[|[|m]]]] => //=; case n as [|[|[|[|m']]]] => //=. + rewrite disjoints1. rewrite inE negb_or /interior notinD /=. have: (x \in [set x; y]); by set_tac. + rewrite disjoints1. by rewrite /interior; set_tac. + rewrite disjoints1. by rewrite /interior; set_tac. + apply: disjointsU => //. apply/disjointP => z Z1 Z2. suff: z = s1' by move: Z1 Z2; rewrite /interior; set_tac. apply: s1'firstp12. by rewrite inE /= Z2. exact: interiorW. + apply: disjointsU => //. * rewrite disjoint_sym. apply: disjointsU. -- rewrite /interior. apply/disjointP; by set_tac. -- by rewrite disjoint_sym. * rewrite disjoint_sym. apply: disjointsU. -- apply/disjointP. rewrite /interior. have: (y \in [set x; y]); by set_tac. -- apply/disjointP => z Z1 Z2. suff: z = s1' by move: Z1 Z2; rewrite /interior; set_tac. apply: s1'firstp12. by rewrite inE /= Z1. exact: interiorW. + rewrite disjoint_sym. apply: disjointsU. * rewrite disjoints1 /interior. by set_tac. * by rewrite disjoint_sym. - move => i j iNj. wlog iltj: i j {iNj} / i < j. { move => H. rewrite /edge_rel /= neq_ltn in iNj. move: iNj => /orP [iltj|jlti]; [|rewrite neighborC]; exact: H. } destruct i as [m i]. destruct j as [n j]. have [[? ?] ?] := (valP (p0),valP p1, valP p2). case m as [|[|[|[|m]]]] => //=; case n as [|[|[|[|m']]]] => //=. + apply: neighborUl. apply: path_neighborL => //; by set_tac. + apply: path_neighborL => //; by set_tac. + exact: neighbor_interiorL. + case: (altP (interior q1 =P set0)) => [E|H]. * rewrite E setU0. apply/neighborP; exists (s0); exists s1'. split => //. case/interior0E : E => //. apply: contraTneq ind01. rewrite /independent; set_tac. * rewrite neighborC. apply: neighborUr. exact: path_neighborR. + apply: neighborUl. rewrite neighborC. apply: neighborUl. apply: path_neighborR => //; by set_tac. + apply: neighborUl. rewrite neighborC. apply: path_neighborR => //; by set_tac. Qed.
imports: Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries set_tac digraph) GraphTheory(sgraph treewidth minor connectivity)