proposition: Lemma EST_not_reachable: forall (P Q: V -> Prop) g1 root g2 (e: E) n, ~ P root -> Q root -> vvalid g1 root -> Included P Q -> out_edges g1 root e -> edge_spanning_tree g1 e P g2 -> ~ g1 |= dst g1 e ~o~> n satisfying P -> (~ reachable g2 (dst g2 e) n \/ ~ out_edges g2 root e).
proof: Proof. intros. destruct (classic (g1 |= dst g1 e ~o~> dst g1 e satisfying P)). + destruct H4 as [[? ?] | [? ?]]. 2: apply reachable_by_head_prop in H6; exfalso; auto. destruct H7 as [? [_ [_ ?]]]. specialize (H8 _ _ H6 H5). assert (out_edges g2 root e) by (rewrite <- (ppg_out_edges P g1); eauto). assert (dst g1 e = dst g2 e) by (apply (ppg_the_same_dst _ _ root _ _ e H) in H7; auto). rewrite H10 in *. left; auto. + destruct H4 as [[? ?] | [? ?]]. - assert (~ vvalid g1 (dst g1 e)). { intro. apply H6. apply reachable_by_refl; auto. } pose proof H7. destruct H7 as [? _]. assert (dst g1 e = dst g2 e) by (apply (ppg_the_same_dst _ _ root g2 _ e) in H7; auto). rewrite H10 in *. left. assert (out_edges g2 root e) by (rewrite <- (ppg_out_edges P g1); eauto). assert (~ reachable g1 (dst g2 e) n) by (intro; apply reachable_by_head_valid in H12; auto). intro; apply H12. apply (spanning_tree_not_reachable_derive g1 _ _ g2 _ _ H9); auto. - destruct H7 as [? [? [? [? ?]]]]. destruct H11. * right. intro. apply H11. destruct H12; auto. * destruct H11 as [? [? ?]]. left; intro. apply H11. apply reachable_by_head_valid in H14; 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