proposition: Lemma path_return (G : sgraph) z (A : {set G}) (x y : G) (p : Path x y) : x \in A -> y \in A -> irred p -> (forall u v, u -- v -> u \in A -> v \notin A -> u = z) -> p \subset A.
proof: Proof. Abort. Section AddEdge. 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_forestT => x y p q Ip Iq. have D : t0 != t1 by apply: contraNneq discT => ->. case: (boolP (@connect T sedge x y)) => [|NC]. - case/connect_irredP => r 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. { move => W. 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. { move => W. 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 V1 => H. 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.
imports: Coq(RelationClasses) mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph sgraph) GraphTheory(connectivity set_tac)