proposition: Lemma spanning_list_spanning_tree2_reachable: forall (P: V -> Prop) (g1 g2 g3: Graph) root (e1 e2 : E) n, (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 -> g1 |= root ~o~> n satisfying P -> reachable g3 root n.
proof: Proof. intros. rename H5 into H9. 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). assert (vvalid g3 root). { rewrite <- (not_reachable_EST_vvalid g2 e2); eauto. intro. apply reachable_by_foot_prop in H10. destruct H10 as [[_ ?] _]. apply H10; auto. } destruct_eq_dec n root. 1: subst; apply reachable_by_refl; auto. destruct (X n). + destruct H5 as [[? ?] | [? ?]]. 2: apply reachable_by_head_prop in r; exfalso; apply H5; auto. destruct H12 as [? [_ [? ?]]]. specialize (H13 _ r). assert (vvalid g2 (dst g1 e1)) by (apply reachable_by_head_valid in H13; auto). destruct H13 as [p ?]. assert (forall v, In_path g2 v p -> g1 |= dst g1 e1 ~o~> v satisfying (fun x : V => P x /\ x <> root)). { intros. destruct (X v); auto. pose proof (reachable_path_in _ _ _ _ H13 _ H16). assert (g1 |= dst g1 e1 ~o~> dst g1 e1 satisfying (fun x : V => P x /\ x <> root)). { apply reachable_by_refl; auto. apply reachable_by_head_valid in r; auto. } specialize (H14 _ _ H18 n0). exfalso; auto. } assert (Hd: dst g1 e1 = dst g2 e1) by (eapply ppg_the_same_dst in H12; eauto; intro; destruct H17; apply H18; auto). assert (g2 |= path_glue (root, e1 :: nil) p is root ~o~> n satisfying (fun _ : V => True)). { apply reachable_by_path_merge with (dst g1 e1); auto. split; split; simpl; auto. + pose proof H3. rewrite (ppg_out_edges (fun x : V => P x /\ x <> root)) in H17; eauto. 2: intro; destruct H18; auto. destruct H17. unfold strong_evalid. rewrite H18, <- Hd. do 3 (split; auto). + hnf; rewrite Forall_forall; intros; auto. } exists (path_glue (root, e1 :: nil) p). destruct H6 as [[? ?] | [? ?]]. - destruct H18 as [? _]. apply (ppg_reachable_by_path_to g2 g3 _ _ _ _ _ H18); auto. intros. assert (v = root \/ In_path g2 v p). { destruct H13 as [[? _] _]. destruct p as [v' p]. unfold path_glue in *. simpl in *. destruct H17 as [_ [[? ?] _]]. subst v'. rewrite in_path_or_cons in H19; auto. rewrite Hd. auto. } clear H19; rename H20 into H19. destruct H19; intro; [subst | apply H16 in H19]; apply reachable_by_foot_prop in H20; destruct H20 as [[? ?] ?]; auto. - apply (gremove_reachable_by_derive g2 e2 g3); auto. destruct p as [v p]. simpl. intros. destruct H19. 1: subst e'; auto. intro. subst. assert (In_path g2 (src g2 e2) (v, p)) by (right; exists e2; simpl; split; auto). specialize (H16 _ H20). apply reachable_by_foot_prop in H16. destruct H8. subst root. destruct H16; auto. + apply (root_reachable_by_derive _ _ _) in H9. destruct H9. 1: exfalso; auto. destruct H9 as [e [? ?]]. rewrite <- H0 in H9. simpl in H9. destruct H9 as [? | [? | ?]]; [subst e ..|]. 1: exfalso; auto. 2: exfalso; auto. assert (g1 |= dst g1 e2 ~o~> n satisfying (fun x : V => (P x /\ x <> root) /\ ~ g1 |= dst g1 e1 ~o~> x satisfying (fun x0 : V => P x0 /\ x0 <> root))). { destruct H12 as [p ?]. pose proof (reachable_by_path_in' _ _ _ _ _ H9). destruct H9 as [? [? ?]]. exists p. do 2 (split; auto). rewrite path_prop_equiv in H14 |-* ; auto. intros. split. apply H14; auto. intro. apply n0. specialize (H12 _ H15). apply reachable_by_trans with n1; auto. } pose proof H5. apply (EST_the_same_dst _ _ root _ _ e2) in H13; auto. 2: intro; destruct H14; auto. rewrite H13 in H9. destruct H6 as [[? ?] | [? ?]]. 2: apply reachable_by_head_prop in H9; exfalso; auto. assert (out_edges g3 root e2). { destruct H14 as [? _]. apply (ppg_out_edges _ _ root) with (e' := e2) in H14; auto. 2: intro; destruct H15 as [[_ ?] _]; auto. rewrite <- H14; auto. } assert (dst g2 e2 = dst g3 e2). { destruct H14 as [? _]. apply (ppg_the_same_dst _ _ root) with (e := e2) in H14; auto. intro. destruct H16 as [[_ ?] _]; auto. } apply edge_reachable_by with (dst g3 e2); auto. - split; auto; split. 2: rewrite step_spec; exists e2; destruct H15; auto. rewrite <- H16. apply reachable_by_head_valid in H9. apply edge_spanning_tree_vvalid_s with (x := dst g2 e2) in H5; auto. rewrite H5 in H9. apply (spanning_tree_root_vvalid _ _ _ _ H14); auto. - destruct H14 as [_ [_ [? _]]]. rewrite <- H16. apply H14. destruct H5 as [[? ?] | [? ?]]. 1: { destruct H17 as [? _]. destruct H9 as [p ?]. exists p. eapply (ppg_reachable_by_path_to g1 g2); eauto. intros. simpl. destruct H9 as [_ [? ?]]. rewrite path_prop_equiv in H19; auto. specialize (H19 _ H18). destruct H19; auto. } 1: { destruct H9 as [p ?]. exists p. apply (gremove_reachable_by_derive g1 e1 g2); auto. repeat intro. subst. destruct H9 as [_ [? ?]]. rewrite path_prop_equiv in H19; auto. assert (In_path g1 (src g1 e1) p) by (right; exists e1; split; auto). specialize (H19 _ H20). destruct H19 as [[_ ?] _]. destruct H3. subst root. 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