proposition: Lemma spanning_list_inj: forall (g1 g2 : Graph) (es : list E) (root: V), marked g1 root -> NoDup es -> Forall (out_edges g1 root) es -> spanning_list g1 es g2 -> componded_mark_list root (map (dst g1) es) g1 g2 /\ SIMPLE_SPANNING_TREE.spanning_list (unmarked g1) g1 es g2.
proof: Proof. intros. induction H2; simpl. + subst. split; constructor. reflexivity. + pose proof H2. rewrite edge_spanning_tree_inj in H2. destruct H2 as [? ?]. assert (marked g2 root) by (rewrite (H2 root); auto). assert (NoDup rest) by (apply NoDup_cons_1 in H0; auto). assert (Forall (out_edges g2 root) rest). { pose proof (Forall_tl _ _ _ H1). rewrite Forall_forall in H8 |-* . intros. specialize (H8 _ H9). apply (SIMPLE_SPANNING_TREE.EST_out_edges (unmarked g1) g1 root g2 e); auto. apply NoDup_cons_2 in H0. intro. apply H0. subst; auto. } specialize (IHspanning_list H6 H7 H8). destruct IHspanning_list. split. - unfold componded_mark_list. simpl. split_relation_list ((lg_gg g2) :: nil); auto. * hnf in H4. destruct (node_pred_dec (marked g1) (dst g1 e)). 1: { destruct H4. apply gremove_is_componded_mark; auto. apply Forall_inv in H1. auto. } 1: { apply spanning_tree_is_componded_mark; auto. } * unfold componded_mark_list in H9. assert (map (dst g1) rest = map (dst g2) rest). { apply NoDup_cons_2 in H0. apply Forall_tl in H1. clear -H0 H H0 H5 H1. induction rest; simpl; auto. f_equal. + apply Forall_inv in H1. apply (SIMPLE_SPANNING_TREE.EST_the_same_dst (unmarked g1) _ root _ e); auto. intro. apply H0. subst. apply in_eq. + apply IHrest. - intro; apply H0, in_cons; auto. - apply Forall_tl in H1. auto. } rewrite H11; auto. - apply SIMPLE_SPANNING_TREE.spanning_list_cons with g2; auto. apply (SIMPLE_SPANNING_TREE.spanning_list_derive (unmarked g2)); auto. intro. symmetry. apply edge_spanning_tree_unmarked_equiv; auto. Qed.
imports: Coq.Classes.Morphisms CertiGraph.lib.Coqlib CertiGraph.lib.EquivDec_ext CertiGraph.lib.EnumEnsembles CertiGraph.lib.List_ext CertiGraph.lib.relation_list CertiGraph.graph.graph_model CertiGraph.graph.path_lemmas CertiGraph.graph.graph_gen CertiGraph.graph.graph_relation CertiGraph.graph.subgraph2 CertiGraph.graph.reachable_ind Coq.Logic.Classical