proposition: Lemma gremove_not_reachable_by_derive: forall (g1 : Graph) (e : E) (g2 : Graph) (x y : V) (p: path) (P: V -> Prop), gremove_edge g1 e g2 -> g2 |= p is x ~o~> y satisfying P -> g1 |= p is x ~o~> y satisfying P.
proof: Proof. intros. destruct H as [? [? [? [? ?]]]]. destruct H0 as [[? ?] [? ?]]. assert (forall e', In e' (snd p) -> e' <> e). { repeat intro. subst. destruct H4 as [? | [? _]]; apply H0; destruct p as [v p]; pose proof (valid_path_strong_evalid _ _ _ e H6 H8); destruct H4 as [? [? ?]]; auto. } assert (Hv: valid_path g1 p). { clear H0 H5 H7. destruct p as [v p]. simpl in H8. revert v H6 H8. induction p; intros. + simpl in H6 |-* . rewrite H; auto. + rewrite valid_path_cons_iff in H6 |-* . destruct H6 as [? [? ?]]. destruct H5 as [? [? ?]]. unfold strong_evalid. assert (a <> e) by (apply H8, in_eq). specialize (H1 _ H10); specialize (H2 _ H10); specialize (H3 _ H10). assert (src g1 a = src g2 a) by (apply H2; intuition). assert (dst g1 a = dst g2 a) by (apply H3; intuition). rewrite H11, H12. subst v. rewrite !H. do 2 (split; [intuition |]). apply IHp; auto. intros. apply H8. right; auto. } split; split; auto. + rewrite pfoot_spec in H5 |-* . destruct H5; [left; auto | right]. destruct H5 as [v [l [e' [? ?]]]]. exists v, l, e'. split; auto. rewrite <- H9. assert (In e' (l +:: e')) by (apply in_or_app; right; apply in_eq). subst p. unfold snd in H8. specialize (H8 _ H10). assert (strong_evalid g2 e') by (apply (valid_path_strong_evalid _ v (l +:: e')); auto). destruct H5 as [? [? ?]]. specialize (H1 _ H8). specialize (H3 _ H8). apply H3; intuition. + rewrite path_prop_equiv in H7 |-* ; auto. intros. apply H7. unfold In_path in H9 |-* . destruct H9; [left | right]; auto. destruct H9 as [e' [? ?]]. exists e'. split; auto. specialize (H8 _ H9). specialize (H1 _ H8). specialize (H2 _ H8). specialize (H3 _ H8). assert (strong_evalid g2 e') by (destruct p as [v p]; apply (valid_path_strong_evalid _ v p); auto). destruct H11 as [? _]. assert (src g1 e' = src g2 e') by (apply H2; intuition). assert (dst g1 e' = dst g2 e') by (apply H3; intuition). rewrite <- H12, <- H13; 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