proposition: Lemma add_edge_unique_simple_upath: forall (g: PGraph) e' u v, unique_simple_upath g -> ~ connected g u v -> unique_simple_upath (pregraph_add_edge g e' u v).
proof: Proof. unfold unique_simple_upath; intros. rename u0 into a; rename v0 into b. assert (exists l : list E, fits_upath (pregraph_add_edge g e' u v) l p1). apply connected_exists_list_edges in H2; auto. assert (exists l : list E, fits_upath (pregraph_add_edge g e' u v) l p2). apply connected_exists_list_edges in H4; auto. destruct H5 as [l1 ?]. destruct H6 as [l2 ?]. destruct (in_dec EE e' l1); destruct (in_dec EE e' l2). + assert ((connected g a u /\ connected g v b) \/ (connected g a v /\ connected g u b)). apply (cross_bridge_implies_endpoints g e' u v p1 l1 a b); auto. destruct H7; destruct H7. apply connected_symm in H7. assert (exists p1_a p1_b, (p1 = p1_a++p1_b /\ connected_by_path g p1_a a u /\ connected_by_path g p1_b v b)). apply (add_edge_bridge_split1 g e' u v p1 a b); auto. exists l1; split; auto. destruct H9 as [p1_a [p1_b ?]]. destruct H9. destruct H10. assert (exists p2_a p2_b, (p2 = p2_a++p2_b /\ connected_by_path g p2_a a u /\ connected_by_path g p2_b v b)). apply (add_edge_bridge_split1 g e' u v p2 a b); auto. exists l2; split; auto. destruct H12 as [p2_a [p2_b ?]]. destruct H12. destruct H13. rewrite H9 in H1; rewrite H12 in H3. destruct H1. destruct H3. assert (p1_a = p2_a). apply (H a u p1_a p2_a). split. apply H10. apply (NoDup_app_l _ _ _ H15). auto. split. apply H13. apply (NoDup_app_l _ _ _ H16). auto. assert (p1_b = p2_b). apply (H v b p1_b p2_b). split. apply H11. apply (NoDup_app_r _ _ _ H15). auto. split. apply H14. apply (NoDup_app_r _ _ _ H16). auto. rewrite H9; rewrite H12; rewrite H17; rewrite H18. auto. apply connected_symm in H7. assert (exists p1_a p1_b, (p1 = p1_a++p1_b /\ connected_by_path g p1_a a v /\ connected_by_path g p1_b u b)). apply (add_edge_bridge_split2 g e' u v p1 a b); auto. exists l1; split; auto. destruct H9 as [p1_a [p1_b ?]]. destruct H9. destruct H10. assert (exists p2_a p2_b, (p2 = p2_a++p2_b /\ connected_by_path g p2_a a v /\ connected_by_path g p2_b u b)). apply (add_edge_bridge_split2 g e' u v p2 a b); auto. exists l2; split; auto. destruct H12 as [p2_a [p2_b ?]]. destruct H12. destruct H13. rewrite H9 in H1; rewrite H12 in H3. destruct H1. destruct H3. assert (p1_a = p2_a). apply (H a v p1_a p2_a). split. apply H10. apply (NoDup_app_l _ _ _ H15). auto. split. apply H13. apply (NoDup_app_l _ _ _ H16). auto. assert (p1_b = p2_b). apply (H u b p1_b p2_b). split. apply H11. apply (NoDup_app_r _ _ _ H15). auto. split. apply H14. apply (NoDup_app_r _ _ _ H16). auto. rewrite H9; rewrite H12; rewrite H17; rewrite H18. auto. + destruct H4. apply (add_edge_unaffected g e' u v p2 l2) in H4; auto. assert (connected g a b). exists p2. split; auto. assert ((connected g a u /\ connected g v b) \/ (connected g a v /\ connected g u b)). apply (cross_bridge_implies_endpoints g e' u v p1 l1 a b); auto. assert (connected g u v). destruct H9; destruct H9. apply (connected_trans g u a v). apply connected_symm; auto. apply (connected_trans g a b v). auto. apply connected_symm; auto. apply (connected_trans g u b v). auto. apply (connected_trans g b a v). apply connected_symm; auto. auto. contradiction. + destruct H2. apply (add_edge_unaffected g e' u v p1 l1) in H2; auto. assert (connected g a b). exists p1. split; auto. assert ((connected g a u /\ connected g v b) \/ (connected g a v /\ connected g u b)). apply (cross_bridge_implies_endpoints g e' u v p2 l2); auto. assert (connected g u v). destruct H9; destruct H9. apply (connected_trans g u a v). apply connected_symm; auto. apply (connected_trans g a b v). auto. apply connected_symm; auto. apply (connected_trans g u b v). auto. apply (connected_trans g b a v). apply connected_symm; auto. auto. contradiction. + destruct H2. apply (add_edge_unaffected g e' u v p1 l1) in H2; auto. destruct H4. apply (add_edge_unaffected g e' u v p2 l2) in H4; auto. apply (H a b). split. apply H2. apply H1. split; auto. split. apply H4. apply H3. split; 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