proposition: Lemma add_edge_bridge_split1: forall (g: PGraph) e' u v p a b, connected g u a -> connected g v 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 u /\ connected_by_path g p2 v b).
proof: Proof. induction p; intros. destruct H4. destruct H5. inversion H6. destruct H3 as [l [? ?]]. destruct l. simpl in H5. contradiction. destruct p. simpl in H3. contradiction. assert (Hvvalid_g_u: vvalid g u). apply (connected_vvalid g u a0). auto. assert (Hvvalid_g_v: vvalid g v). apply (connected_vvalid g v b). auto. assert (a0 = a). destruct H4. destruct H6. simpl in 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. exists (u::nil); exists (v::p). split. auto. split. split; simpl; auto. assert (~ In e' l). unfold not; intros. assert (In (src (pregraph_add_edge g e' u v) e') (v :: p)). apply (fits_upath_vertex_src_In (pregraph_add_edge g e' u v) (v::p) l e'); auto. rewrite add_edge_src in H7. destruct H2. apply NoDup_cons_2 in H8. simpl in H8. contradiction. split. apply valid_upath_exists_list_edges'. exists l. apply add_edge_fits_upath_rev in H5; auto. split. simpl; auto. destruct H4. destruct H7. rewrite last_error_cons in H8. rewrite <- H8. auto. unfold not; intros. simpl in H9. inversion H9. subst a. contradiction. 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 (src (pregraph_add_edge g e' u v) e') (v :: p)). apply (fits_upath_vertex_src_In (pregraph_add_edge g e' u v) (v::p) l e'); auto. rewrite add_edge_src in H7. simpl in H7. destruct H2. apply NoDup_cons_2 in H8. simpl in H8. contradiction. assert (In (dst (pregraph_add_edge g e' u v) e') (u :: p)). apply (fits_upath_vertex_dst_In (pregraph_add_edge g e' u v) (u::p) l e'); auto. rewrite add_edge_dst in H7. simpl in H7. destruct H2. apply NoDup_cons_2 in H8. simpl 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 u /\ connected_by_path g p2 v b). apply (IHp v0 b); auto. apply (connected_trans g u 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. destruct H7. rewrite last_error_cons in H9. auto. unfold not; intros. inversion H10. destruct H7 as [p1 [p2 [? [? ?]]]]. 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