proposition: Lemma spanning_list_spanning_tree2: forall (g g1 g2: Graph) root (e1 e2 : E), (e1 <> e2) -> (forall e, In e (e1 :: e2 :: nil) <-> out_edges g root e) -> ReachDecidable g1 (dst g1 e1) (unmarked g1) -> vvalid g root -> unmarked g root -> mark1 root g g1 -> spanning_list g1 (e1 :: e2 :: nil) g2 -> spanning_tree g root g2.
proof: Proof. intros. rewrite spanning_tree_inj. apply (spanning_list_inj _ _ _ root) in H4. 2: { destruct H3 as [_ [? _]]; auto. } 2: { constructor. + intro. apply H. simpl in H5. destruct H5; [|exfalso]; auto. + constructor. intro. inversion H5. constructor. } 2: { rewrite Forall_forall. intros. rewrite H0 in H5. destruct H3. apply (out_edges_si _ _ root x) in H3. intuition. } destruct H4. split. + assert (step_list g root (map (dst g1) (e1 :: e2 :: nil))). { hnf. destruct H3. intros. assert (HD: forall e, evalid g e -> dst g e = dst g1 e). { intros. destruct H3 as [_ [? [_ ?]]]. specialize (H3 e). specialize (H8 e). intuition. } split; intro. + simpl in H7. destruct H7 as [? | [? | ?]]; [| |exfalso; auto]; subst n'; rewrite step_spec. - assert (out_edges g root e1) by (rewrite <- H0; apply in_eq). exists e1. destruct H7. auto. - assert (out_edges g root e2) by (rewrite <- H0; apply in_cons, in_eq). exists e2. destruct H7. auto. + rewrite step_spec in H7. destruct H7 as [e [? [? ?]]]. assert (out_edges g root e) by (split; auto). rewrite <- H0 in H10. simpl in H10. destruct H10 as [? | [? | ?]]; [| |exfalso; auto]; subst e; subst n'; simpl; [|right]; left; rewrite HD; intuition. } assert (relation_list (nothing root :: mark1 root :: nothing root :: componded_mark_list root (map (dst g1) (e1 :: e2 :: nil)) :: nothing root :: nil) g g2). { split_relation_list ((lg_gg g) :: nil). apply eq_do_nothing; auto. split_relation_list ((lg_gg g1) :: nil); auto. split_relation_list ((lg_gg g1) :: nil). apply eq_do_nothing; auto. split_relation_list ((lg_gg g2) :: nil); auto. apply eq_do_nothing; auto. } apply mark1_componded_mark_list_mark in H7; auto. - destruct H7. exact H8. + assert (forall x, unmarked g1 x <-> unmarked g x /\ x <> root). { intros. destruct H3 as [? [? ?]]. unfold unmarked. rewrite !negateP_spec. split; intros. + specialize (H7 x). destruct_eq_dec root x. - subst. exfalso; auto. - rewrite H7; intuition. + destruct H8. rewrite <- H7; intuition. } destruct H3. rewrite H3. apply (SIMPLE_SPANNING_TREE.spanning_list_spanning_tree2_s _ _ _ _ e1 e2); auto. - intros. rewrite H0. apply out_edges_si; auto. - destruct H3. rewrite <- H3; auto. - apply (ReachDecidable_si g1 g1 (unmarked g1)); auto. * reflexivity. * hnf. intros. rewrite H6; intuition. - apply (SIMPLE_SPANNING_TREE.spanning_list_derive (unmarked g1)); 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