proposition: Lemma ppg_reachable_by_path_same: forall (g : PreGraph V E) (P Q: V -> Prop) (p: @path V E) (a b: V), ((forall v, In_path g v p -> P v) /\ g |= p is a ~o~> b satisfying Q) <-> (predicate_partialgraph g P) |= p is a ~o~> b satisfying Q.
proof: Proof. intros. split; intros. + destruct H. destruct H0 as [[? ?] [? ?]]. split; split; auto. 2: rewrite <- ppg_valid_path; split; auto. destruct p as [v p]. clear H H0 H2 H3. revert v H1. induction p; intros. 1: simpl in *. auto. rewrite pfoot_cons in H1 |-* . change (dst (predicate_partialgraph g P) a0) with (dst g a0). apply IHp. auto. + destruct H as [[? ?] [? ?]]. rewrite <- ppg_valid_path in H1. destruct H1. split; auto. split; split; auto. clear H H1 H3 H2. destruct p as [v p]. revert v H0. induction p; intros. 1: simpl in *; auto. rewrite pfoot_cons in H0 |-* . apply IHp. apply H0. Qed.
imports: Coq.Arith.Arith Coq.Logic.ProofIrrelevance Coq.Logic.FunctionalExtensionality Coq.Classes.Morphisms Coq.Classes.Equivalence CertiGraph.lib.Coqlib CertiGraph.lib.Ensembles_ext CertiGraph.lib.relation_list CertiGraph.lib.List_ext CertiGraph.lib.Equivalence_ext CertiGraph.lib.EquivDec_ext VST.msl.Coqlib2 CertiGraph.graph.graph_model CertiGraph.graph.path_lemmas CertiGraph.graph.reachable_ind CertiGraph.graph.graph_gen CertiGraph.graph.graph_relation