proposition: Lemma not_sat_edge: forall (g: Graph) s v p (P: V -> Prop), valid_path g (s, p) -> In_path g v (s, p) -> P s -> ~ P v -> exists e, In e p /\ P (src g e) /\ ~ P (dst g e).
proof: Proof. intros g s v p. revert s v. induction p; intros. 1: destruct H0 as [? | [e [? _]]]; simpl in H0; exfalso; [subst| ]; auto. rewrite in_path_or_cons in H0. 2: destruct H; auto. destruct H0. 1: subst; exfalso; auto. destruct (classic (P (dst g a))). + apply valid_path_cons in H. specialize (IHp _ _ _ H H0 H3 H2). destruct IHp as [e [? ?]]. exists e; split; auto. right; auto. + exists a. destruct H. subst s. split; auto. left; 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