proposition: Lemma ppg_valid_path: forall (g: PreGraph V E) (P: V -> Prop) (p: @path V E), (valid_path g p /\ (forall v, In_path g v p -> P v)) <-> valid_path (predicate_partialgraph g P) p.
proof: Proof. intros g P p. destruct p as [v p]. revert v. induction p; intros; split; intros. + destruct H. simpl in *. split; auto. apply H0. unfold In_path. left; simpl; auto. + simpl in H. destruct H. simpl. split; auto. intros. unfold In_path in H1. simpl in H1. destruct H1. 1: subst; auto. destruct H1 as [e [? ?]]. exfalso; auto. + destruct H. rewrite valid_path_cons_iff in H |-* . destruct H as [? [? ?]]. split; [|split]. - simpl. auto. - unfold strong_evalid. simpl. unfold predicate_vvalid. unfold predicate_weak_evalid. destruct H1 as [? [? ?]]. assert (In_path g (src g a) (v, a :: p)) by (right; exists a; split; [apply in_eq | left; auto]). apply H0 in H5. assert (In_path g (dst g a) (v, a :: p)) by (right; exists a; split; [apply in_eq | right; auto]). apply H0 in H6. intuition. - change (dst (predicate_partialgraph g P) a) with (dst g a). apply IHp. split; auto. intros. apply H0. apply (in_path_or_cons _ _ _ p v0) in H. rewrite H. right; auto. + rewrite valid_path_cons_iff in H. destruct H as [? [? ?]]. change (dst (predicate_partialgraph g P) a) with (dst g a) in H1. simpl in H. rewrite <- IHp in H1. destruct H1. hnf in H0. simpl in H0. unfold predicate_weak_evalid, predicate_vvalid in H0. destruct H0 as [[? _] [[? ?] [? ?]]]. split. - rewrite valid_path_cons_iff. unfold strong_evalid. split; auto. - intros. pose proof (in_path_or_cons _ _ _ p v0 H). rewrite H8 in H7. clear H8. destruct H7. 1: subst; auto. apply H2; auto. 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