proposition: Lemma spanning_bi_tree: forall (P: V -> Prop) g1 root g2 g3 (e1 e2 : E), (e1 <> e2) -> (forall e, In e (e1 :: e2 :: nil) <-> out_edges g1 root e) -> vvalid g1 root -> P root -> ReachDecidable g1 (dst g1 e1) (fun x => P x /\ x <> root) -> edge_spanning_tree g1 e1 (fun x : V => P x /\ x <> root) g2 -> edge_spanning_tree g2 e2 (fun x : V => (P x /\ x <> root) /\ ~ g1 |= dst g1 e1 ~o~> x satisfying (fun x0 : V => P x0 /\ x0 <> root)) g3 -> spanning_tree g1 root P g3.
proof: Proof. intros. rename H3 into H5. rename H4 into H6. assert (out_edges g1 root e1) by (rewrite <- H0; apply in_eq). assert (out_edges g1 root e2) by (rewrite <- H0; apply in_cons, in_eq). assert (vvalid g2 root) by (rewrite <- (edge_spanning_tree_vvalid_s g1 e1 (fun x : V => P x /\ x <> root)); auto). assert (out_edges g2 root e2) by (apply (EST_out_edges (fun x : V => P x /\ x <> root) g1 _ _ e1);intuition). split; [|split; [|split]]; intros. + pose proof H5. apply (EST_predicate_partial_si g1 g2 e1 root P) in H9; auto. 2: intro; unfold Ensembles.In ; intuition. rewrite H9. clear H9. apply (EST_predicate_partial_si g2 g3 e2 root P) in H6; auto. 2: intro; unfold Ensembles.In ; intuition. apply si_stronger_partialgraph_simple with (fun n : V => ~ g2 |= root ~o~> n satisfying P); auto. cut (Included (reachable_by g2 root P) (reachable_by g1 root P)). - unfold Included. unfold Ensembles.In . intros. intuition. - apply EST_root_reachable_by with e1; auto. + rewrite is_tree_ppg_spec. intros. pose proof H10. destruct H11 as [p ?]. exists p. unfold unique. split; auto. intros. destruct x' as [v x']. assert (v = root) by (destruct H12 as [[? _] _]; simpl in H12; inversion H12; auto). subst v. destruct p as [v p]. assert (v = root) by (destruct H11 as [[? _] _]; simpl in H11; inversion H11; auto). subst v. assert (forall e path, ~ g3 |= (root, e :: path) is root ~o~> root satisfying (reachable_by g1 root P)). { intros. intro. pose proof H13. destruct H14 as [_ [[? ?] _]]. assert (strong_evalid g3 e) by (simpl in H15; destruct path; intuition). destruct H16 as [? [? ?]]. assert (out_edges g1 root e). { apply (EST_reverse_out_edges (fun x : V => P x /\ x <> root) g1 g2 e1); auto. intro. destruct H19; auto. apply (EST_reverse_out_edges (fun x : V => (P x /\ x <> root) /\ ~ g1 |= dst g1 e1 ~o~> x satisfying (fun x0 : V => P x0 /\ x0 <> root)) g2 g3 e2); auto. intro. destruct H19 as [[_ ?] _]; auto. split; auto. } rewrite <- H0 in H19. simpl in H19. destruct H19 as [? | [? | ?]]; auto; subst e. + assert (~ reachable g3 (dst g3 e1) root \/ ~ out_edges g3 root e1). { apply (ST2_not_reachable (fun x : V => P x /\ x <> root) P g1 _ g2 _ _ e2); auto. + intro. destruct H19; auto. + compute. tauto. + intro. apply reachable_by_foot_prop in H19. destruct H19; auto. + intro. apply reachable_by_foot_prop in H19. destruct H19 as [[_ ?] _]; auto. } destruct H19. - apply H19. exists (dst g3 e1, path). destruct H13 as [[_ ?] [? _]]. split; split; auto. * rewrite pfoot_cons in H13; auto. * clear -H15. simpl in *. destruct path. 1: hnf in H15; intuition. destruct H15; auto. * hnf. destruct path; simpl; auto. hnf. rewrite Forall_forall. intros; auto. - apply H19. split; auto. + assert (~ reachable g3 (dst g3 e2) root \/ ~ out_edges g3 root e2). { apply (EST_not_reachable (fun x : V => (P x /\ x <> root) /\ ~ g1 |= dst g1 e1 ~o~> x satisfying (fun x0 : V => P x0 /\ x0 <> root)) P g2); auto. + intro. destruct H19 as [[_ ?] _]; auto. + hnf. unfold Ensembles.In . intuition. + intro. apply reachable_by_foot_prop in H19. destruct H19 as [[_ ?] _]; auto. } destruct H19. - apply H19. exists (dst g3 e2, path). clear -H13. destruct H13 as [[? ?] [? ?]]. split; split; auto. * rewrite pfoot_cons in H0; auto. * apply valid_path_cons in H1; auto. * hnf. rewrite Forall_forall. split; intros; auto. - apply H19. split; auto. } destruct x'; destruct p; auto. - destruct H12 as [[_ ?] _]. simpl in H12. inversion H12. subst y. exfalso. specialize (H13 e p). auto. - destruct H11 as [[_ ?] _]. simpl in H11. inversion H11. subst y. exfalso. specialize (H13 e x'). auto. - clear H13. assert (forall m ms, g3 |= (root, m :: ms) is root ~o~> y satisfying (reachable_by g1 root P) -> g3 |= (dst g3 m, ms) is dst g3 m ~o~> y satisfying (reachable_by g1 root P)). { intros. clear -H13. destruct H13 as [[_ ?] [? ?]]. assert (valid_path g3 (dst g3 m, ms)) by (apply valid_path_cons in H0; auto). split; split; auto. + rewrite pfoot_cons in H; auto. + rewrite path_prop_equiv in H1 |-* ; auto. intros. apply H1. rewrite in_path_or_cons. 2: destruct H0; auto. right; auto. } assert (forall e, evalid g3 e -> src g3 e = root -> out_edges g2 root e). { intros. apply (EST_reverse_out_edges (fun x : V => (P x /\ x <> root) /\ ~ g1 |= dst g1 e1 ~o~> x satisfying (fun x0 : V => P x0 /\ x0 <> root)) g2 g3 e2); auto. intro. destruct H16 as [[_ ?] _]; auto. split; auto. } assert (forall e, evalid g3 e -> src g3 e = root -> out_edges g1 root e). { intros. apply (EST_reverse_out_edges (fun x : V => P x /\ x <> root) g1 g2 e1); auto. intro. destruct H17; auto. } assert (evalid g3 e1 -> src g3 e1 = root -> vvalid g3 (dst g3 e1) -> (P (dst g1 e1) /\ dst g1 e1 <> root) /\ dst g1 e1 = dst g2 e1 /\ dst g2 e1 = dst g3 e1). { intros. clear H11 H12 H13. destruct H5 as [[? ?] | [? ?]]. + split; auto. destruct H11 as [? [? [? ?]]]. assert (dst g1 e1 = dst g2 e1). { apply (ppg_the_same_dst _ _ root _ _ e1) in H11; auto. intro. destruct H20. auto. } rewrite H20 in *. assert (out_edges g2 root e1). { rewrite <- (ppg_out_edges (fun x : V => P x /\ x <> root) g1); eauto. intro. destruct H21. auto. } assert (dst g2 e1 = dst g3 e1). { apply (EST_the_same_dst _ _ root _ _ e1) in H6; auto. intro. destruct H22 as [[_ ?] _]. auto. } rewrite H22 in *. auto. + exfalso. specialize (H14 _ H16 H17). destruct H14. destruct H11 as [? [? [? [? ?]]]]. destruct H21; auto. destruct H21 as [? [? ?]]. pose proof H6. apply (EST_the_same_dst _ _ root _ _ e1) in H24; auto. - rewrite H24 in *. apply (edge_spanning_tree_vvalid_s _ _ _ _ (dst g3 e1)) in H6. rewrite <- H6 in H18. auto. - intro. destruct H25 as [[_ ?] _]; auto. - split; auto. } assert (evalid g3 e2 -> src g3 e2 = root -> vvalid g3 (dst g3 e2) -> ((P (dst g2 e2) /\ dst g2 e2 <> root) /\ ~ g1 |= dst g1 e1 ~o~> dst g2 e2 satisfying (fun x0 : V => P x0 /\ x0 <> root)) /\ dst g2 e2 = dst g3 e2). { intros. clear H11 H12 H13. destruct H6 as [[? ?] | [? ?]]. + split; auto. destruct H11 as [? _]. apply (ppg_the_same_dst _ _ root _ _ e2) in H11; auto. intro. destruct H12 as [[_ ?] _]. auto. + exfalso. specialize (H14 _ H17 H18). destruct H14. destruct H11 as [? [? [? [? ?]]]]. destruct H22 as [? | [? _]]; auto. } assert (forall ms, evalid g3 e1 -> src g3 e1 = root -> vvalid g3 (dst g3 e1) -> g3 |= (dst g3 e1, ms) is dst g3 e1 ~o~> y satisfying (reachable_by g1 root P) -> g2 |= (dst g3 e1, ms) is dst g3 e1 ~o~> y satisfying (reachable_by g1 (dst g3 e1) (fun x : V => P x /\ x <> root))). { clear H11 H12 H13 H17. intros. specialize (H16 H11 H12 H13). pose proof H5. destruct H16 as [? [? ?]]. destruct H5 as [[_ ?] | [? ?]]. 2: exfalso; auto. destruct H5 as [? [? [? ?]]]. rewrite H19 in *. rewrite H20 in *. assert (g1 |= dst g3 e1 ~o~> dst g3 e1 satisfying (fun x : V => P x /\ x <> root)). { apply reachable_by_refl; auto. rewrite <- (edge_spanning_tree_vvalid_s _ _ _ _ _ H6) in H13. rewrite <- (edge_spanning_tree_vvalid_s _ _ _ _ _ H18) in H13. auto. } assert (forall v, In_path g3 v (dst g3 e1, ms) -> g1 |= dst g3 e1 ~o~> v satisfying (fun x : V => P x /\ x <> root)). { intros. destruct (X v); auto. destruct H17 as [? [? ?]]. pose proof (not_sat_edge _ _ _ _ (reachable_by g1 (dst g3 e1) (fun x : V => P x /\ x <> root)) H26 H25 H24 n). destruct H28 as [e3 [? [? ?]]]. specialize (H23 _ _ H29 H30). assert (strong_evalid g3 e3) by (apply (valid_path_strong_evalid _ (dst g3 e1) ms); auto). assert (g3 |= src g3 e3 ~> (dst g3 e3)) by (destruct H31 as [? [? ?]]; hnf; do 2 (split; auto); rewrite step_spec; exists e3; split; auto). apply (EST_not_edge_derive _ _ _ _ _ _ H6) in H32. 2: intro; apply reachable_by_foot_prop in H33; destruct H33; auto. clear -H32 H23. exfalso. apply H23. apply edge_reachable_by with (dst g3 e3); auto. apply reachable_by_refl; auto. destruct H32 as [? [? ?]]. auto. } assert (g3 |= (dst g3 e1, ms) is dst g3 e1 ~o~> y satisfying (reachable_by g1 (dst g3 e1) (fun x : V => P x /\ x <> root))). { destruct H17 as [[? ?] [? ?]]. split; split; auto. rewrite path_prop_equiv; auto. } destruct H6 as [[? ?] | [? ?]]. + destruct H27. apply (ppg_reachable_by_path_to g3 g2 (fun n : V => ~ g2 |= dst g2 e2 ~o~> n satisfying (fun x : V => (P x /\ x <> root) /\ ~ g1 |= dst g3 e1 ~o~> x satisfying (fun x0 : V => P x0 /\ x0 <> root)))) in H26; [|symmetry|]; auto. intros. specialize (H25 _ H29). intro. apply reachable_by_foot_prop in H30. destruct H30; auto. + apply (gremove_not_reachable_by_derive _ e2 g3); auto. } assert (forall ms, evalid g3 e2 -> src g3 e2 = root -> vvalid g3 (dst g3 e2) -> g3 |= (dst g3 e2, ms) is dst g3 e2 ~o~> y satisfying (reachable_by g1 root P) -> g3 |= (dst g3 e2, ms) is dst g2 e2 ~o~> y satisfying ( reachable_by g2 (dst g2 e2) (fun x : V => (P x /\ x <> root) /\ ~ g1 |= dst g1 e1 ~o~> x satisfying (fun x0 : V => P x0 /\ x0 <> root)))). { clear H11 H12 H13 H16 H18. intros. specialize (H17 H11 H12 H13). destruct H17. destruct H6 as [[_ ?] | [? _]]. 2: exfalso; auto. pose proof H6. destruct H6 as [? [? [? ?]]]. rewrite H18 in *. assert (g2 |= dst g3 e2 ~o~> dst g3 e2 satisfying (fun x : V => (P x /\ x <> root) /\ ~ g1 |= dst g1 e1 ~o~> x satisfying (fun x0 : V => P x0 /\ x0 <> root))). { apply reachable_by_refl; auto. rewrite <- (spanning_tree_vvalid_s _ _ _ _ _ H19) in H13. auto. } assert (forall v, In_path g3 v (dst g3 e2, ms) -> (g2 |= dst g3 e2 ~o~> v satisfying (fun x : V => (P x /\ x <> root) /\ ~ g1 |= dst g1 e1 ~o~> x satisfying (fun x0 : V => P x0 /\ x0 <> root)))). { intros. destruct (classic (g2 |= dst g3 e2 ~o~> v satisfying (fun x : V => (P x /\ x <> root) /\ ~ g1 |= dst g1 e1 ~o~> x satisfying (fun x0 : V => P x0 /\ x0 <> root)))); auto. destruct H16 as [? [? ?]]. pose proof (not_sat_edge _ _ _ _ (reachable_by g2 (dst g3 e2) (fun x : V => (P x /\ x <> root) /\ ~ g1 |= dst g1 e1 ~o~> x satisfying (fun x0 : V => P x0 /\ x0 <> root))) H26 H24 H23 H25). destruct H28 as [e3 [? [? ?]]]. specialize (H22 _ _ H29 H30). assert (strong_evalid g3 e3) by (apply (valid_path_strong_evalid _ (dst g3 e2) ms); auto). assert (g3 |= src g3 e3 ~> (dst g3 e3)) by (destruct H31 as [? [? ?]]; hnf; do 2 (split; auto); rewrite step_spec; exists e3; split; auto). clear -H32 H22. exfalso. apply H22. apply edge_reachable_by with (dst g3 e3); auto. apply reachable_by_refl; auto. destruct H32 as [? [? ?]]. auto. } destruct H16 as [[? ?] [? ?]]. split; split; auto. rewrite path_prop_equiv; auto. } pose proof (H13 _ _ H11). pose proof (H13 _ _ H12). clear H13. destruct H11 as [_ [? _]]. rewrite valid_path_cons_iff in H11. destruct H11 as [? [[? [? ?]] ?]]. destruct H12 as [_ [? _]]. rewrite valid_path_cons_iff in H12. destruct H12 as [? [[? [? ?]] ?]]. symmetry in H12, H11. pose proof (H15 _ H13 H11). pose proof (H15 _ H25 H12). clear H15. rewrite <- H0 in H29. rewrite <- H0 in H30. simpl in H29. simpl in H30. destruct H29 as [? | [? | ?]]; [subst e0..| exfalso; tauto]; destruct H30 as [? | [? | ?]]; try (exfalso; tauto); subst e. * specialize (H16 H25 H12 H27). destruct H16 as [? [? ?]]. destruct H5 as [[_ ?] | [? ?]]. 2: exfalso; auto. pose proof (H18 _ H13 H12 H27 H20). pose proof (H18 _ H13 H12 H27 H21). destruct H5 as [_ [? _]]. specialize (H5 H15). rewrite is_tree_ppg_spec in H5. rewrite <- H29 in *. rewrite <- H16 in *. pose proof (reachable_by_path_is_reachable_by _ _ _ _ _ H30). specialize (H5 _ H32). destruct H5 as [path' ?]. destruct H5. pose proof (H33 _ H30). pose proof (H33 _ H31). rewrite H34 in H35. inversion H35. auto. * specialize (H16 H13 H11 H23). destruct H16 as [? [? ?]]. destruct H5 as [[_ ?] | [? _]]. 2: exfalso; auto. specialize (H17 H25 H12 H27). destruct H17 as [? ?]. destruct H6 as [[_ ?] | [? _]]. 2: exfalso; auto. specialize (H18 _ H13 H11 H23 H20). apply reachable_by_path_is_reachable_by in H18. apply reachable_by_foot_prop in H18. pose proof H6. destruct H6 as [_ [_ [_ ?]]]. rewrite <- H29 in *. assert (~ g2 |= dst g3 e2 ~o~> y satisfying (fun x : V => (P x /\ x <> root) /\ ~ g1 |= dst g1 e1 ~o~> x satisfying (fun x0 : V => P x0 /\ x0 <> root))). { intro. apply reachable_by_foot_prop in H32. destruct H32. rewrite <- H16 in *. auto. } assert (g2 |= dst g3 e2 ~o~> dst g3 e2 satisfying (fun x : V => (P x /\ x <> root) /\ ~ g1 |= dst g1 e1 ~o~> x satisfying (fun x0 : V => P x0 /\ x0 <> root))). { rewrite H30 in *. apply reachable_by_refl; auto. rewrite <- (spanning_tree_vvalid_s _ _ _ _ _ H31) in H27; auto. } rewrite H30 in *. specialize (H6 _ _ H33 H32). exfalso; apply H6. apply reachable_by_path_is_reachable in H21; auto. * specialize (H16 H25 H12 H27). destruct H16 as [? [? ?]]. destruct H5 as [[_ ?] | [? _]]. 2: exfalso; auto. specialize (H17 H13 H11 H23). destruct H17 as [? ?]. destruct H6 as [[_ ?] | [? _]]. 2: exfalso; auto. specialize (H18 _ H25 H12 H27 H21). apply reachable_by_path_is_reachable_by in H18. apply reachable_by_foot_prop in H18. pose proof H6. destruct H6 as [_ [_ [_ ?]]]. rewrite <- H29 in *. assert (~ g2 |= dst g3 e2 ~o~> y satisfying (fun x : V => (P x /\ x <> root) /\ ~ g1 |= dst g1 e1 ~o~> x satisfying (fun x0 : V => P x0 /\ x0 <> root))). { intro. apply reachable_by_foot_prop in H32. destruct H32. rewrite <- H16 in *. auto. } assert (g2 |= dst g3 e2 ~o~> dst g3 e2 satisfying (fun x : V => (P x /\ x <> root) /\ ~ g1 |= dst g1 e1 ~o~> x satisfying (fun x0 : V => P x0 /\ x0 <> root))). { rewrite <- H30 in *. apply reachable_by_refl; auto. rewrite <- (spanning_tree_vvalid_s _ _ _ _ _ H31) in H23; auto. } rewrite <- H30 in *. specialize (H6 _ _ H33 H32). exfalso; apply H6. apply reachable_by_path_is_reachable in H20; auto. * specialize (H17 H13 H11 H23). destruct H17 as [? ?]. destruct H6 as [[_ ?] | [? _]]. 2: exfalso; auto. destruct H6 as [_ [? _]]. specialize (H6 H15). pose proof (H19 _ H13 H11 H23 H20). pose proof (H19 _ H13 H11 H23 H21). pose proof (reachable_by_path_is_reachable_by _ _ _ _ _ H29). rewrite is_tree_ppg_spec in H6. rewrite H17 in *. specialize (H6 _ H31). destruct H6 as [path' ?]. destruct H6. pose proof (H32 _ H29). pose proof (H32 _ H30). rewrite H33 in H34. inversion H34. auto. + apply (spanning_list_spanning_tree2_reachable P g1 g2 g3 root e1 e2 n); auto. + apply (spanning_list_spanning_tree2_reachable _ _ g2 g3 _ e1 e2) in H9; auto. intro. assert (reachable g3 root b) by (apply reachable_by_trans with a; auto). cut (~ reachable g3 root b). 1: intro. apply H13; auto. clear H9 H11. destruct_eq_dec b root. 1: subst; exfalso; apply H10; apply reachable_by_refl; auto. assert (~ g2 |= root ~o~> b satisfying P). { intro. apply H10. apply EST_root_reachable_by in H5; auto. apply H5, H11. } assert (N1: forall v, ~ g2 |= dst g2 e2 ~o~> b satisfying (fun x : V => (P x /\ x <> root) /\ ~ g1 |= v ~o~> x satisfying (fun x0 : V => P x0 /\ x0 <> root))). { repeat intro. apply H11. apply edge_reachable_by with (dst g2 e2); auto. + split; auto. apply reachable_by_head_valid in H13. split; auto. rewrite step_spec. exists e2. destruct H8; auto. + revert H13. apply reachable_by_weaken. hnf. unfold Ensembles.In . intros. destruct H13 as [[? _] _]; auto. } assert (~ reachable g3 (dst g3 e1) b \/ ~ out_edges g3 root e1). { apply (ST2_not_reachable (fun x : V => P x /\ x <> root) P g1 _ g2 _ _ e2); auto. + intro. destruct H13; auto. + compute. tauto. + intro. apply H10. apply edge_reachable_by with (dst g1 e1); auto. - split; auto. apply reachable_by_head_valid in H13. split; auto. rewrite step_spec. exists e1. destruct H3. auto. - apply reachable_by_weaken with (fun x : V => P x /\ x <> root); auto. compute; tauto. } assert (~ reachable g3 (dst g3 e2) b \/ ~ out_edges g3 root e2). { apply (EST_not_reachable (fun x : V => (P x /\ x <> root) /\ ~ g1 |= dst g1 e1 ~o~> x satisfying (fun x0 : V => P x0 /\ x0 <> root)) P g2); auto. + intro. destruct H14 as [[_ ?] _]; auto. + hnf. unfold Ensembles.In . intros. destruct H14 as [[? _] _]; auto. } assert (forall e, out_edges g3 root e -> In e (e1 :: e2 :: nil)). { intros. apply (EST_reverse_out_edges (fun x : V => (P x /\ x <> root) /\ ~ g1 |= dst g1 e1 ~o~> x satisfying (fun x0 : V => P x0 /\ x0 <> root)) g2 g3 e2 root) in H15; auto. 2: intro; destruct H16 as [[_ ?] _]; auto. apply (EST_reverse_out_edges (fun x : V => P x /\ x <> root) g1 g2 e1 root) in H15; auto. 2: intro; destruct H16; auto. rewrite H0; auto. } apply root_not_reachable_derive. destruct H13, H14; split; auto; intros; pose proof H16; apply H15 in H16; destruct H16 as [? | [? | ?]]; auto; subst; 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