proposition: Lemma uforest_uforest': forall g, uforest g -> uforest' g.
proof: Proof. unfold uforest, uforest'; intros. split. intros. apply uforest_no_self_loops; auto. split. intros. apply (uforest_no_multigraph g u v e1 e2); auto. split. apply H. destruct H. unfold unique_simple_upath; intros. destruct (EV u v). hnf in e. subst v. apply (simple_upath_self g u p1) in H1; auto. apply (simple_upath_self g u p2) in H3; auto. rewrite H1, H3. auto. unfold complement, equiv in c. destruct (list_eqdec EV p1 p2). hnf in e; auto. unfold complement, equiv in c0. exfalso. assert (exists (la : list V) (x : V) (l1b l2b : list V) (y : V) (l1c l2c : list V), p1 = la ++ x :: l1b ++ y :: l1c /\ p2 = la ++ x :: l2b ++ y :: l2c /\ (forall u : V, In u l1b -> ~ In u l2b) /\ (forall u : V, In u l2b -> ~ In u l1b) /\ l1b <> l2b). apply (first_divergence_bubble_ugly p1 p2 u v). auto. apply H2. apply H4. apply H2. apply H4. auto. apply H1. apply H3. destruct H5 as [pa [x [p1' [p2' [y [p1c [p2c ?]]]]]]]. destruct H5 as [? [? [? [? Hnot]]]]. subst p1. subst p2. assert (connected_by_path g (x::p1'+::y) x y). { split. replace (pa ++ x :: p1' ++ y :: p1c) with (pa++(x::p1'+::y)++p1c) in H2. destruct H2. apply valid_upath_app_split in H2. destruct H2. apply valid_upath_app_split in H6. apply H6. simpl. rewrite <- app_assoc. simpl. auto. split. auto. rewrite app_comm_cons. apply last_err_appcons. } assert (simple_upath g (x::p1'+::y)). split. apply H5. destruct H1. apply NoDup_app_r in H6. replace (x :: p1' ++ y :: p1c) with ((x::p1'+::y)++p1c) in H6. apply NoDup_app_l in H6. auto. simpl. rewrite <- app_assoc. simpl; auto. assert (connected_by_path g (x::p2'+::y) x y). { split. replace (pa ++ x :: p2' ++ y :: p2c) with (pa++(x::p2'+::y)++p2c) in H4. destruct H4. apply valid_upath_app_split in H4. destruct H4. apply valid_upath_app_split in H10. apply H10. simpl. rewrite <- app_assoc. simpl. auto. split. auto. rewrite app_comm_cons. apply last_err_appcons. } assert (simple_upath g (x::p2'+::y)). split. apply H9. destruct H3. apply NoDup_app_r in H10. replace (x :: p2' ++ y :: p2c) with ((x::p2'+::y)++p2c) in H10. apply NoDup_app_l in H10. auto. simpl. rewrite <- app_assoc. simpl; auto. clear c0. clear H2 H1 H4 H3. clear p1c p2c pa. clear c u v. replace (x :: p2' +:: y) with (rev ((y::(rev p2')+::x))) in *. 2: { simpl. rewrite rev_unit, rev_involutive. simpl; auto. } apply connected_by_path_rev in H9. rewrite rev_involutive in H9. apply simple_upath_rev in H10. rewrite rev_involutive in H10. set (p:=(x::p1'+::y)++ tl (y::rev p2'+::x)). assert (connected_by_path g p x x). unfold p. apply (connected_by_path_join g _ _ x y x); auto. assert (exists l, fits_upath g l p). apply connected_exists_list_edges in H1; auto. destruct H2 as [l ?]. assert (simple_upath g (tl p)). { split. apply valid_upath_tail. apply H1. unfold p. simpl. apply NoDup_app_inv. destruct H6. apply NoDup_cons_1 in H4. auto. destruct H10. apply NoDup_cons_1 in H4. auto. unfold not; intros. apply in_app_or in H3; apply in_app_or in H4. destruct H3; destruct H4. rewrite <- in_rev in H4. apply H8 in H4. auto. destruct H4. subst x0. destruct H6. apply NoDup_cons_2 in H6. apply H6. apply in_or_app; left; auto. contradiction. destruct H3. subst x0. destruct H10. apply NoDup_cons_2 in H10. apply H10. apply in_or_app; left; auto. contradiction. destruct H3; destruct H4; try contradiction. subst x0. destruct H6. apply NoDup_cons_2 in H6. apply H6. subst y. apply in_or_app. right; left; auto. } apply (H0 p l). unfold p, simple_ucycle, ucycle. split. apply H3. simpl. destruct (p1' +:: y ++ rev p2' +:: x) eqn:Htmp. assert (In x (p1' +:: y ++ rev p2' +:: x)). apply in_or_app; right; apply in_or_app; right; left; auto. rewrite Htmp in H4; contradiction. unfold p in H2. simpl in H2. rewrite Htmp in H2. destruct l. contradiction. split. rewrite <- Htmp. apply H1. split. auto. apply NoDup_cons. -- assert (Htl: connected_by_path g (tl p) v x). split. apply H3. split. unfold p; simpl; rewrite Htmp; auto. simpl. rewrite app_assoc. apply last_err_appcons. simpl in Htl. rewrite Htmp in Htl. unfold not; intros. destruct H2. unfold p in H3. simpl in H3. rewrite Htmp in H3. destruct H3. assert (Hv: ~ In v l0). apply NoDup_cons_2 in H12; auto. destruct l. contradiction. destruct l0. simpl in H11; contradiction. destruct H4. subst e0. destruct H11. assert (v0 = x). { destruct H2. destruct H4. destruct H13; destruct H13; destruct H14; destruct H14; rewrite H13 in H14; rewrite H15 in H16. apply NoDup_cons_2 in H12. exfalso; apply H12. left. auto. auto. auto. exfalso; apply NoDup_cons_2 in H12; apply H12; left; auto. } subst v0. clear H4. destruct l0. ++ destruct p1'. destruct p2'. contradiction. simpl in Htmp. inversion Htmp. destruct (rev p2'). simpl in H14. inversion H14. simpl in H14. inversion H14. pose proof (app_not_nil (l0+::v0) x). contradiction. inversion Htmp. destruct p1'. inversion H14. pose proof (app_not_nil (rev p2') x). contradiction. simpl in H14. inversion H14. rewrite app_assoc in H16. pose proof (app_not_nil (p1' +:: y ++ rev p2') x). contradiction. ++ assert (In x (v0::l0)). apply last_error_In. apply Htl. apply NoDup_cons_1 in H12. apply NoDup_cons_2 in H12. contradiction. ++ destruct H11. apply NoDup_cons_2 in H12. exfalso; apply H12. destruct H2. destruct H14; destruct H14. apply (fits_upath_vertex_dst_In g (v0::l0)) in H4. rewrite H15 in H4; auto. auto. apply (fits_upath_vertex_src_In g (v0::l0)) in H4. rewrite H14 in H4; auto. auto. -- apply fits_upath_cons in H2. rewrite <- Htmp in H2. apply (simple_upath_list_edges_NoDup g (tl p) l). auto. unfold p; simpl; 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