proposition: Lemma ST2_not_reachable: forall (P Q: V -> Prop) g1 root g2 g3 (e1 e2: E) n, e1 <> e2 -> ~ P root -> Q root -> vvalid g1 root -> Included P Q -> out_edges g1 root e1 -> out_edges g1 root e2 -> edge_spanning_tree g1 e1 P g2 -> ReachDecidable g1 (dst g1 e1) P -> ~ g1 |= (dst g1 e1) ~o~> n satisfying P -> edge_spanning_tree g2 e2 (fun x : V => P x /\ ~ g1 |= dst g1 e1 ~o~> x satisfying P) g3 -> ~ g2 |= dst g2 e2 ~o~> n satisfying (fun x : V => P x /\ ~ g1 |= dst g1 e1 ~o~> x satisfying P) -> (~ reachable g3 (dst g3 e1) n \/ ~ out_edges g3 root e1).
proof: Proof. intros. assert (vvalid g2 root) by (rewrite <- (edge_spanning_tree_vvalid_s g1 e1 P); auto). assert (out_edges g2 root e2) by (apply (EST_out_edges P g1 _ _ e1); intuition). destruct (X (dst g1 e1)); destruct H6 as [[? ?] | [? ?]]. + destruct H12 as [? [_ [_ ?]]]. specialize (H13 _ _ r H7). assert (out_edges g2 root e1) by (rewrite <- (ppg_out_edges P g1); eauto). assert (dst g1 e1 = dst g2 e1) by (apply (ppg_the_same_dst _ _ root) with (e := e1) in H12; auto). rewrite H15 in *. assert (dst g2 e1 = dst g3 e1). { apply (EST_the_same_dst _ _ root _ _ e1) in H8; auto. intro. destruct H16 as [? _]. auto. } rewrite H16 in *. left. apply (EST_not_reachable_derive _ _ _ _ _ _ H8); auto. + apply reachable_by_head_prop in r; exfalso; auto. + assert (~ vvalid g1 (dst g1 e1)). { intro. apply n0. apply reachable_by_refl; auto. } pose proof H12. destruct H12 as [? _]. assert (dst g1 e1 = dst g2 e1) by (apply (ppg_the_same_dst _ _ root) with (e := e1) in H12; auto). rewrite H15 in *. assert (out_edges g2 root e1) by (rewrite <- (ppg_out_edges P g1); eauto). assert (dst g2 e1 = dst g3 e1). { apply (EST_the_same_dst _ _ root _ _ e1) in H8; auto. intro. destruct H17 as [? _]. auto. } rewrite H17 in *. assert (~ vvalid g2 (dst g3 e1)) by (rewrite <- (not_reachable_ST_vvalid g1 (dst g3 e1) P); auto). left. apply not_reachable_EST_vvalid with (x := (dst g3 e1)) in H8; auto. 2: intro; apply reachable_by_foot_valid in H19; auto. rewrite H8 in H18. intro. apply H18. apply reachable_by_head_valid in H19. auto. + destruct H12 as [? [? [? [? ?]]]]. destruct H16. - right. intro. apply H16. apply (EST_reverse_out_edges (fun x : V => P x /\ ~ g1 |= dst g1 e1 ~o~> x satisfying P) g2 _ e2) in H17; auto. 2: intro; destruct H18 as [? _]; auto. destruct H17; auto. - destruct H16 as [? [? ?]]. assert (out_edges g2 root e1). { clear -H4 H17 H18. destruct H4. subst root. split; auto. } assert (dst g2 e1 = dst g3 e1). { apply (EST_the_same_dst _ _ root _ _ e1) in H8; auto. intro. destruct H20 as [? _]. auto. } rewrite H20 in *. assert (~ reachable g2 (dst g3 e1) n). { clear -H16. intro. apply H16. apply reachable_head_valid in H. auto. } left. apply (EST_not_reachable_derive _ _ _ _ _ _ H8); 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