proposition: Lemma cross_bridge_implies_endpoints: forall (g: PGraph) e u v p l a b, ~ connected g u v -> simple_upath (pregraph_add_edge g e u v) p -> connected_by_path (pregraph_add_edge g e u v) p a b -> fits_upath (pregraph_add_edge g e u v) l p -> In e l -> ((connected g a u /\ connected g v b) \/ (connected g a v /\ connected g u b)).
proof: Proof. induction p; intros. destruct H1. destruct H4. inversion H4. assert (a = a0). destruct H1. destruct H4. inversion H4. auto. subst a0. destruct l. contradiction. destruct p. contradiction. destruct H3. subst e0. destruct H2. destruct H2. destruct H2. rewrite add_edge_src in H5, H4. rewrite add_edge_dst in H5, H4. destruct H5. simpl in H5, H6. assert (~ In e l). unfold not; intros. destruct H4; destruct H4; subst a; subst v0; destruct H0. assert (In u (v::p)). replace u with (src (pregraph_add_edge g e u v) e). apply (fits_upath_vertex_src_In _ (v::p) l e); auto. rewrite add_edge_src. auto. apply NoDup_cons_2 in H4. contradiction. assert (In v (u::p)). replace v with (dst (pregraph_add_edge g e u v) e). apply (fits_upath_vertex_dst_In _ (u::p) l e); auto. rewrite add_edge_dst. auto. apply NoDup_cons_2 in H4. contradiction. destruct H4; destruct H4; subst a; subst v0. left. split. apply connected_refl. auto. exists (v::p). split. apply valid_upath_exists_list_edges'. exists l. apply (add_edge_fits_upath_rev g e u v). auto. auto. split. simpl; auto. destruct H1. destruct H4. rewrite last_error_cons in H8; auto. unfold not; intros; inversion H9. right. split. apply connected_refl. auto. exists (u::p). split. apply valid_upath_exists_list_edges'. exists l. apply (add_edge_fits_upath_rev g e u v). auto. auto. split. simpl; auto. destruct H1. destruct H4. rewrite last_error_cons in H8; auto. unfold not; intros; inversion H9. assert (Hav0: connected g a v0). { apply adjacent_connected. destruct H2. destruct H2. assert (e <> e0). unfold not; intros. subst e0. rewrite add_edge_src in H5; rewrite add_edge_dst in H5. destruct H5; destruct H5; 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 _ (v::p) l e); auto. rewrite add_edge_src. auto. destruct H0. apply NoDup_cons_2 in H6. contradiction. assert (In v (u::p)). replace v with (dst (pregraph_add_edge g e u v) e). apply (fits_upath_vertex_dst_In _ (u::p) l e); auto. rewrite add_edge_dst. auto. destruct H0. apply NoDup_cons_2 in H6. contradiction. exists e0. destruct H2. repeat rewrite <- adde_vvalid in H7. rewrite add_edge_preserves_src in H5, H7; auto. rewrite add_edge_preserves_dst in H5, H7; auto. apply add_edge_evalid_rev in H2; auto. split; auto. split; auto. } assert (connected g v0 u /\ connected g v b \/ connected g v0 v /\ connected g u b). apply (IHp l v0 b). auto. split. apply H0. destruct H0. apply NoDup_cons_1 in H4. auto. destruct H1. destruct H4. split. apply H0. split. simpl; auto. rewrite last_error_cons in H5; auto. unfold not; intros; inversion H6. apply H2. apply H3. destruct H4; destruct H4. left. split. apply (connected_trans g a v0 u); auto. auto. right. split. apply (connected_trans g a v0 v); auto. 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