proposition: Lemma ppg_reachable_by_path_eq: forall (g1 g2 : PreGraph V E) (P Q: V -> Prop) (p: @path V E) (a b: V), (predicate_partialgraph g1 P) ~=~ (predicate_partialgraph g2 P) -> (forall v, In_path g1 v p -> P v) -> (g1 |= p is a ~o~> b satisfying Q <-> g2 |= p is a ~o~> b satisfying Q).
proof: Proof. cut (forall (g1 g2 : PreGraph V E) (P Q: V -> Prop) (p: @path V E) (a b: V), (predicate_partialgraph g1 P) ~=~ (predicate_partialgraph g2 P) -> (forall v, In_path g2 v p -> P v) -> g1 |= p is a ~o~> b satisfying Q -> g2 |= p is a ~o~> b satisfying Q); intros. + split; intro; [apply (H g1 g2 P) | apply (H g2 g1 P)]; auto. 2: symmetry; auto. assert (valid_path (predicate_partialgraph g1 P) p) by (rewrite <- ppg_valid_path; split; [destruct H2 as [_ [? _]] |]; auto). rewrite (valid_path_si _ _ H0) in H3. rewrite <- ppg_valid_path in H3. destruct H3; auto. + destruct H1 as [[? ?] [? ?]]. split; split; auto; clear H1. Abort. #[global] Instance reachable_by_proper: Proper ((@structurally_identical V E _ _) ==> (@eq V) ==> @Same_set V ==> (@eq V) ==> iff) (@reachable_by V E _ _). Proof. intros. do 4 (hnf; intros); subst. rewrite !reachable_by_eq_partialgraph_reachable. rewrite H, H1. reflexivity. Defined.
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