proposition: Lemma partial_lgraph_spanning_equiv: forall (t1 t2 g: UAdjMatGG), is_partial_lgraph t1 t2 -> labeled_spanning_uforest t1 g -> labeled_spanning_uforest t2 g -> Permutation (EList t1) (EList t2).
proof: Proof. intros. apply NoDup_Permutation. apply NoDup_EList. apply NoDup_EList. intros. repeat rewrite EList_evalid. split; intros. apply H. auto. destruct (evalid_dec t1 x). auto. exfalso. pose proof (trivial_path1 t2 x (evalid_strong_evalid t2 x H2)). destruct H3. assert (connected t1 (src t2 x) (dst t2 x)). apply H0. apply H1. exists (src t2 x :: dst t2 x :: nil); auto. destruct H5 as [p ?]. apply connected_by_upath_exists_simple_upath in H5. clear p. destruct H5 as [p [? ?]]. assert (exists l, fits_upath t1 l p). apply connected_exists_list_edges in H5; auto. destruct H7 as [l ?]. assert (~ In x l). unfold not; intros. apply (fits_upath_evalid t1 p l) in H8; auto. assert (fits_upath t2 l p). apply (fits_upath_transfer' p l t1 t2) in H7; auto. intros; split; intros. apply H. auto. rewrite vert_bound in *; auto. intros. apply H. apply (fits_upath_evalid t1 p l); auto. intros. apply H. auto. apply (evalid_strong_evalid t1); auto. intros. apply H. auto. apply (evalid_strong_evalid t1); auto. assert (p = (src t2 x :: dst t2 x :: nil)). assert (unique_simple_upath t2). apply H1. unfold unique_simple_upath in H10. apply (H10 (src t2 x) (dst t2 x)). split. apply valid_upath_exists_list_edges'. exists l; auto. apply H6. apply connected_exists_list_edges'. intros. rewrite vert_bound. apply (valid_upath_vvalid t1) in H11. rewrite vert_bound in H11; auto. apply H6. exists l. auto. apply H5. apply H5. split. apply H3. apply NoDup_cons. unfold not; intros. destruct H11. 2: contradiction. symmetry in H11. assert (src t2 x <> dst t2 x). apply H1. auto. contradiction. apply NoDup_cons. unfold not; intros; contradiction. apply NoDup_nil. apply H3. assert (x :: nil = l). apply (uforest'_unique_lpath p (x::nil) l t2). apply H1. split. apply valid_upath_exists_list_edges'. exists l; auto. apply H6. rewrite H10; auto. auto. rewrite <- H11 in H8. apply H8. left; auto. 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