proposition: Lemma exists_labeled_spanning_uforest_pre: forall (l: list E) (g: UAdjMatGG), Permutation l (EList g) -> exists (t: UAdjMatGG), labeled_spanning_uforest t g.
proof: Proof. induction l; intros. exists (@edgeless_graph (inf_representable g) (size_representable g)). split. split. apply edgeless_partial_lgraph. split. apply uforest'_edgeless_graph. unfold spanning; intros. destruct (V_EqDec u v). hnf in e. subst v. split; intros; apply connected_refl. apply connected_vvalid in H0. rewrite vert_bound in *. apply H0. apply connected_vvalid in H0. rewrite vert_bound in *. apply H0. unfold complement, equiv in c. split; intros. exfalso. destruct H0. unfold connected_by_path in H0. destruct H0. destruct H1. destruct x. inversion H1. destruct x. inversion H1. inversion H2. subst v0. contradiction. destruct H0. destruct H0. destruct H0. destruct H0. rewrite <- EList_evalid in H0. rewrite <- H in H0. contradiction. pose proof (@edgeless_graph_disconnected (inf_representable g) (size_representable g) u v c). contradiction. unfold preserve_vlabel, preserve_elabel; split; intros. destruct vlabel. destruct vlabel. auto. pose proof (@edgeless_graph_evalid (inf_representable g) (size_representable g) e). contradiction. set (u:=src g a). set (v:=dst g a). assert (connected g u v). apply adjacent_connected. exists a. unfold u; unfold v; apply strong_evalid_adj_edge. apply (evalid_strong_evalid g). rewrite <- EList_evalid, <- H. left; auto. set (remove_a:=(@UAdjMatGG_eremove g a)). assert (Ha_evalid: evalid g a). { rewrite <- EList_evalid. apply (Permutation_in (l:=(a::l))). apply H. left; auto. } specialize IHl with remove_a. destruct IHl as [t ?]. { unfold remove_a. pose proof (@eremove_EList g a Ha_evalid l H). apply NoDup_Permutation. assert (NoDup (a::l)). apply (Permutation_NoDup (l:=EList g)). apply Permutation_sym; auto. apply NoDup_EList. apply NoDup_cons_1 in H2; auto. apply NoDup_EList. intros. rewrite EList_evalid. split; intros. pose proof (Permutation_in (l:=l) (l':=_) x H1 H2). rewrite EList_evalid in H3; auto. apply Permutation_sym in H1. apply (Permutation_in (l:=_) (l':=l) x H1). rewrite EList_evalid; auto. } assert (Htg: is_partial_lgraph t g). { destruct H1. destruct H2. destruct H1. destruct H4. split. split. intros. apply H1 in H6. auto. split. intros. destruct H1. destruct H7. apply H7. auto. split. intros. apply H1 in H7. simpl in H7. auto. auto. intros. apply H1 in H7. simpl in H7. auto. auto. unfold preserve_vlabel, preserve_elabel; split; intros. destruct vlabel. destruct vlabel. auto. rewrite H3 by auto. simpl. destruct (E_EqDec e a). unfold equiv in e0. subst e. assert (evalid remove_a a). apply H1; auto. simpl in H7. unfold removeValidFunc in H7. destruct H7; contradiction. auto. } destruct (connected_dec remove_a u v). ++ exists t. destruct H1. destruct H3. destruct H1. destruct H5. split. split. apply Htg. split. auto. unfold spanning in *. intros. rewrite <- H6. split; intros. { destruct H7 as [p ?]. apply (connected_by_upath_exists_simple_upath) in H7. destruct H7 as [p' [? ?]]. clear p. assert (exists l, fits_upath g l p'). apply (connected_exists_list_edges g p' u0 v0); auto. destruct H9 as [l' ?]. destruct (in_dec E_EqDec a l'). ** assert (NoDup l'). apply (simple_upath_list_edges_NoDup g p' l'); auto. apply (fits_upath_split2 g p' l' a u0 v0) in H9; auto. destruct H9 as [p1 [p2 [l1 [l2 [? [? [? [? ?]]]]]]]]. subst l'. fold u in H11. fold v in H11. assert (~ In a l1). unfold not; intros. apply (NoDup_app_not_in E l1 ((a::nil)++l2) H10 a) in H14. apply H14. apply in_or_app. left; left; auto. assert (~ In a l2). unfold not; intros. apply NoDup_app_r in H10. apply (NoDup_app_not_in E (a::nil) l2 H10 a). left; auto. auto. destruct H11; destruct H11. **** apply (connected_trans _ u0 u). exists p1. split. apply (remove_edge_valid_upath _ a p1 l1); auto. apply H11. apply H11. apply (connected_trans _ u v). auto. exists p2. split. apply (remove_edge_valid_upath _ a p2 l2); auto. apply H16. apply H16. **** apply (connected_trans _ u0 v). exists p1. split. apply (remove_edge_valid_upath _ a p1 l1); auto. apply H11. apply H11. apply (connected_trans _ v u). apply connected_symm; auto. exists p2. split. apply (remove_edge_valid_upath _ a p2 l2); auto. apply H16. apply H16. ** exists p'. split. apply (remove_edge_valid_upath _ a p' l'); auto. apply H7. apply H7. } { destruct H7 as [p [? ?]]. exists p. split. apply remove_edge_unaffected in H7; auto. auto. } apply Htg. ++ assert (vvalid g u /\ vvalid g v). apply connected_vvalid in H0; auto. destruct H3. assert (u <= v). apply (undirected_edge_rep g). auto. set (w:= elabel g a). assert (Int.min_signed <= w < inf). unfold w. split. pose proof (weight_representable g a). apply H6. apply (evalid_meaning g). auto. rewrite vert_bound in H3, H4. rewrite <- (vert_bound t) in H3, H4. assert (Ha: a = (u,v)). unfold u, v; apply evalid_form; auto. rewrite Ha in *. set (adde_a:=@UAdjMatGG_adde t u v H3 H4 H5 w H6). exists adde_a. split. split. apply adde_partial_lgraph; auto. unfold w. rewrite Ha; auto. split. apply add_edge_uforest'; auto. apply H1. unfold not; intros. apply (is_partial_lgraph_connected t remove_a) in H7. contradiction. split. apply H1. apply H1. unfold spanning; intros. assert (Ht_uv: ~ evalid t (u,v)). unfold not; intros. assert (evalid remove_a (u,v)). apply H1; auto. simpl in H8. rewrite Ha in H8. unfold removeValidFunc in H8. destruct H8; contradiction. split; intros. { destruct H7 as [p ?]. apply connected_by_upath_exists_simple_upath in H7. destruct H7 as [p' [? ?]]. clear p. assert (exists l', fits_upath g l' p'). apply connected_exists_list_edges in H7; auto. destruct H9 as [l' ?]. assert (NoDup l'). apply simple_upath_list_edges_NoDup in H9; auto. destruct (in_dec E_EqDec a l'). ** apply (fits_upath_split2 g p' l' a u0 v0) in H9; auto. destruct H9 as [p1 [p2 [l1 [l2 [? [? [? [? ?]]]]]]]]. fold u in H11. fold v in H11. subst l'. assert (~ In a l1). unfold not; intros. apply (NoDup_app_not_in E l1 ((a::nil)++l2) H10 a) in H14. apply H14. apply in_or_app. left; left; auto. assert (~ In a l2). unfold not; intros. apply NoDup_app_r in H10. apply (NoDup_app_not_in E (a::nil) l2 H10 a). left; auto. auto. destruct H11; destruct H11. **** apply (connected_trans _ u0 u). apply add_edge_connected; auto. apply H1. exists p1. split. apply (remove_edge_valid_upath _ a p1 l1); auto. apply H11. apply H11. apply (connected_trans _ u v). apply adjacent_connected. exists a. rewrite Ha. apply add_edge_adj_edge1. auto. auto. apply add_edge_connected; auto. apply H1. exists p2. split. apply (remove_edge_valid_upath _ a p2 l2); auto. apply H16. apply H16. **** apply (connected_trans _ u0 v). apply add_edge_connected; auto. apply H1. exists p1. split. apply (remove_edge_valid_upath _ a p1 l1); auto. apply H11. apply H11. apply (connected_trans _ v u). apply adjacent_connected. apply adjacent_symm. exists a. rewrite Ha. apply add_edge_adj_edge1. auto. auto. apply add_edge_connected; auto. apply H1. exists p2. split. apply (remove_edge_valid_upath _ a p2 l2); auto. apply H16. apply H16. ** apply add_edge_connected; auto. apply H1. exists p'. split. 2: apply H7. apply (remove_edge_valid_upath g a p' l'); auto. apply H7. } { apply (is_partial_lgraph_connected adde_a g). apply adde_partial_lgraph; auto. unfold w. rewrite Ha; auto. auto. } unfold preserve_vlabel, preserve_elabel; split; intros. destruct vlabel; destruct vlabel; auto. simpl. unfold update_elabel, equiv_dec. destruct (E_EqDec (u,v) e). hnf in e0. subst e. unfold w; rewrite Ha; auto. apply Htg. simpl in H7. unfold addValidFunc in H7. destruct H7. apply H7. unfold complement, equiv in c. symmetry in H7; contradiction. Qed.
imports: VST.floyd.proofauto CertiGraph.lib.EquivDec_ext CertiGraph.lib.List_ext CertiGraph.lib.find_lemmas CertiGraph.graph.graph_model CertiGraph.graph.graph_gen CertiGraph.graph.graph_relation CertiGraph.graph.undirected_graph CertiGraph.graph.MathAdjMatGraph