proposition: Lemma remove_edge_uforest': forall (g: PGraph) e, uforest' g -> evalid g e -> uforest' (pregraph_remove_edge g e) /\ ~ connected (pregraph_remove_edge g e) (src g e) (dst g e).
proof: Proof. intros. pose proof (remove_edge_evalid g e). assert (Hvvalid: forall v1, vvalid (pregraph_remove_edge g e) v1 <-> vvalid g v1). intros. simpl. split; auto. split. { split. intros. simpl. apply H. rewrite remove_edge_evalid in H2; apply H2. split. intros. unfold adj_edge, strong_evalid in H2; simpl in H2. unfold removeValidFunc in H2. destruct H2. destruct H2. destruct H3. destruct H. destruct H6. apply (H6 u v e1 e2). split; split. split. apply H2. apply H2. apply H4. split. apply H3. apply H3. apply H5. split. intros. rewrite remove_edge_evalid in H2; destruct H2. destruct H. destruct H4. destruct H5. apply remove_edge_preserves_strong_evalid; auto. unfold unique_simple_upath; intros. assert (exists l, fits_upath (pregraph_remove_edge g e) l p1). apply valid_upath_exists_list_edges. apply H2. destruct H6 as [l1 ?]. assert (exists l, fits_upath (pregraph_remove_edge g e) l p2). apply valid_upath_exists_list_edges. apply H4. destruct H7 as [l2 ?]. destruct (in_dec EE e l1). apply (fits_upath_evalid (pregraph_remove_edge g e) p1) in i; auto. rewrite remove_edge_evalid in i. destruct i. contradiction. destruct (in_dec EE e l2). apply (fits_upath_evalid (pregraph_remove_edge g e) p2) in i; auto. rewrite remove_edge_evalid in i. destruct i. contradiction. apply (fits_upath_transfer' p1 l1 _ g) in H6; auto. apply (fits_upath_transfer' p2 l2 _ g) in H7; auto. assert (valid_upath g p1). apply valid_upath_exists_list_edges'. exists l1. auto. assert (valid_upath g p2). apply valid_upath_exists_list_edges'. exists l2. auto. assert (unique_simple_upath g). apply H. unfold unique_simple_upath in H10. destruct H2. destruct H4. destruct H3. destruct H5. apply (H10 u v p1 p2). split; auto. split; auto. split; auto. split; auto. intros. apply (fits_upath_evalid _ _ _ _ H7) in H8. apply H8. intros. apply (fits_upath_evalid _ _ _ _ H6) in H8. apply H8. } { unfold not, connected; intros. destruct H2 as [p ?]. assert (exists l, fits_upath (pregraph_remove_edge g e) l p). apply valid_upath_exists_list_edges. apply H2. destruct H3 as [l ?]. assert (fits_upath g l p). apply (fits_upath_transfer' p l (pregraph_remove_edge g e) g); auto. intros. apply (fits_upath_evalid _ _ _ _ H3) in H4. apply H4. assert (connected_by_path g p (src g e) (dst g e)). split. apply valid_upath_exists_list_edges'. exists l; auto. destruct H2. auto. assert (bridge g e (src g e) (dst g e)). apply (forest_adj_bridge g e (src g e) (dst g e) H). apply strong_evalid_adj_edge. apply H. auto. assert (In e l). unfold bridge in H6. apply (H6 p l); auto. apply (fits_upath_evalid _ _ _ _ H3) in H7. rewrite remove_edge_evalid in H7. destruct H7. contradiction. } 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