proposition: Lemma exists_msf: forall {E_EqDec : EqDec E eq} (g: UAdjMatGG), exists (t: UAdjMatGG), minimum_spanning_forest t g.
proof: Proof. intros. pose proof (NoDup_incl_ordered_powerlist (EList g) (NoDup_EList g)). destruct H as [L ?]. destruct (list_decidable_prop_reduced_list (fun l' => NoDup l' /\ incl l' (EList g) /\ (forall x y, In x l' -> In y l' -> (find l' x 0 <= find l' y 0 <-> find (EList g) x 0 <= find (EList g) y 0))) (fun l => (exists (t: UAdjMatGG), labeled_spanning_uforest t g /\ Permutation l (EList t))) L ). apply exists_dec. intros; split; intros. rewrite <- H in H0. destruct H0 as [? [? ?]]. split. apply H0. split. apply H1. apply H2. rewrite <- H. auto. rename x into Lspan. assert (Lspan <> nil). unfold not; intros. { destruct (exists_labeled_spanning_uforest g) as [t ?]. destruct (test2 (EList t) (EList g)) as [lt ?]. apply NoDup_EList. apply NoDup_EList. apply partial_graph_incl. apply H2. destruct H3. assert (In lt Lspan). apply H0. split. split. apply (Permutation_NoDup (l:=EList t)). apply Permutation_sym; auto. apply NoDup_EList. split. unfold incl; intros. apply (Permutation_in (l':=EList t)) in H5; auto. apply (partial_graph_incl t g) in H5; auto. apply H2. apply H4. exists t. split; auto. rewrite H1 in H5; contradiction. } pose proof (exists_Zmin Lspan (fun l => fold_left Z.add (map (elabel g) l) 0) H1). destruct H2 as [lmin [? ?]]. apply H0 in H2. destruct H2. destruct H2 as [? [? ?]]. destruct H4 as [msf [? ?]]. exists msf. unfold minimum_spanning_forest. split. apply H4. intros. destruct (test2 (EList t') (EList g)) as [lt' ?]. apply NoDup_EList. apply NoDup_EList. apply partial_graph_incl. apply H8. destruct H9. rewrite (sum_DE_equiv msf lmin). 2: apply Permutation_sym; auto. rewrite (sum_DE_equiv t' lt'). 2: apply Permutation_sym; auto. replace (map (elabel msf) lmin) with (map (elabel g) lmin). replace (map (elabel t') lt') with (map (elabel g) lt'). apply H3. apply H0. split. split. apply (Permutation_NoDup (l:=EList t')). apply Permutation_sym; auto. apply NoDup_EList. split. unfold incl; intros. apply (Permutation_in (l':=EList t')) in H11; auto. apply (partial_graph_incl t' g) in H11. auto. apply H8. apply H10. exists t'. split; auto. symmetry; apply partial_lgraph_elabel_map. split. apply H8. apply H8. apply Permutation_incl; auto. symmetry; apply partial_lgraph_elabel_map. split. apply H4. apply H4. apply Permutation_incl; 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