proposition: Lemma add_edge_bridge_split2: forall (g: PGraph) e' u v p a b , connected g v a -> connected g u b -> ~ connected g u v -> simple_upath (pregraph_add_edge g e' u v) p -> (exists l, fits_upath (pregraph_add_edge g e' u v) l p /\ In e' l) -> connected_by_path (pregraph_add_edge g e' u v) p a b -> (exists p1 p2, p = p1++p2 /\ connected_by_path g p1 a v /\ connected_by_path g p2 u b).
proof: Proof. induction p; intros. destruct H4. destruct H5. inversion H6. destruct H3 as [l ?]. destruct H3. destruct l. simpl in *. contradiction. destruct p. simpl in H3. contradiction. assert (Hvvalid_g_v: vvalid g v). apply (connected_vvalid g v a0). auto. assert (Hvvalid_g_u: vvalid g u). apply (connected_vvalid g u b). auto. assert (a0 = a). destruct H4. destruct H6. inversion H6. auto. subst a0. destruct H5. subst e. destruct H3. destruct H3. rewrite add_edge_src in H6. rewrite add_edge_dst in H6. destruct H6; destruct H6; subst a; subst v0. apply connected_symm in H. contradiction. exists (v::nil); exists (u::p). split. auto. split. split; simpl; auto. assert (~ In e' l). unfold not; intros. assert (In v (u::p)). replace v with (dst (pregraph_add_edge g e' u v) e'). apply (fits_upath_vertex_dst_In (pregraph_add_edge g e' u v) (u::p) l e'). auto. auto. rewrite add_edge_dst. auto. destruct H2. apply NoDup_cons_2 in H8. contradiction. split. apply valid_upath_exists_list_edges'. exists l. apply (add_edge_fits_upath_rev g e' u v); auto. split. simpl; auto. destruct H4. destruct H7. rewrite last_error_cons in H8. auto. unfold not; intros. inversion H9. assert (e <> e'). unfold not; intros. subst e. destruct H3. destruct H3. rewrite add_edge_src in H7; rewrite add_edge_dst in H7. destruct H7; destruct H7; subst a; subst v0. assert (In u (v::p)). replace u with (src (pregraph_add_edge g e' u v) e'). apply (fits_upath_vertex_src_In (pregraph_add_edge g e' u v) (v::p) l e'). auto. auto. rewrite add_edge_src. auto. destruct H2. apply NoDup_cons_2 in H8. contradiction. assert (In v (u::p)). replace v with (dst (pregraph_add_edge g e' u v) e'). apply (fits_upath_vertex_dst_In (pregraph_add_edge g e' u v) (u::p) l e'). auto. auto. rewrite add_edge_dst. auto. destruct H2. apply NoDup_cons_2 in H8. contradiction. assert (Hav0: adjacent g a v0). exists e. destruct H3. destruct H3. split. apply (add_edge_preserves_strong_evalid g e' u v e). auto. auto. rewrite add_edge_preserves_src in H8; auto. rewrite add_edge_preserves_dst in H8; auto. assert (exists p1 p2, v0 :: p = p1++ p2 /\ connected_by_path g p1 v0 v /\ connected_by_path g p2 u b). apply (IHp v0 b); auto. apply (connected_trans g v a v0). auto. apply adjacent_connected. auto. destruct H2. split. apply H2. apply NoDup_cons_1 in H7. auto. exists l. split. destruct H3. apply H7. apply H5. destruct H4. destruct H4. split. apply H8. split. auto. destruct H7. rewrite last_error_cons in H9. auto. unfold not; intros. inversion H10. destruct H7 as [p1 [p2 ?]]. destruct H7. destruct H8. exists (a::p1). exists p2. split. rewrite H7. simpl. auto. split. destruct H8. split. apply valid_upath_cons. apply H8. destruct H10. rewrite H10. simpl. auto. split. simpl; auto. rewrite last_error_cons. apply H10. destruct H10. unfold not; intros. subst p1. inversion H10. auto. Qed.
imports: Coq.Logic.Classical CertiGraph.lib.List_ext CertiGraph.lib.EquivDec_ext CertiGraph.graph.graph_model CertiGraph.graph.graph_relation CertiGraph.graph.path_lemmas CertiGraph.graph.graph_gen CertiGraph.graph.FiniteGraph