proposition: Lemma dag_ramify_left: forall (g g1: Graph) x l r, vvalid g x -> vgamma g x = (false, l, r) -> mark1 x g g1 -> @derives pred _ (reachable_dag_vertices_at x g1) (reachable_dag_vertices_at l g1 * (ALL g': Graph, !! (mark l g1 g') --> (reachable_dag_vertices_at l g' -* reachable_dag_vertices_at x g'))).
proof: Proof. intros. unfold reachable_dag_vertices_at. normalize. pose proof proj1 H1. rewrite <- H3 in H2. assert (localDag g1 l). 1: { rewrite <- H3. eapply local_dag_step; eauto. eapply gamma_step; eauto. } rewrite prop_true_andp by auto. match goal with | |- _ |-- _ * ?A => replace A with (ALL g' : Graph , (!!mark l g1 g':pred) --> (vertices_at (reachable g' l) g' -* vertices_at (reachable g' x) g')) end. 2: { apply allp_congr; intros g2. apply imp_prop_ext; [reflexivity |]. intros [_ ?]. rewrite prop_true_andp by (rewrite <- H5; auto). rewrite prop_true_andp by (rewrite <- H5, <- H3; auto). reflexivity. } eapply graph_ramify_left; eauto. Qed.
imports: CertiGraph.lib.Ensembles_ext Coq.Lists.List VST.msl.seplog VST.msl.log_normalize VST.msl.Coqlib2 CertiGraph.lib.Coqlib CertiGraph.lib.EquivDec_ext CertiGraph.lib.relation_list CertiGraph.msl_ext.log_normalize CertiGraph.msl_ext.iter_sepcon CertiGraph.graph.graph_model CertiGraph.graph.path_lemmas CertiGraph.graph.reachable_computable CertiGraph.graph.reachable_ind CertiGraph.graph.subgraph2 CertiGraph.graph.graph_gen CertiGraph.graph.dag CertiGraph.graph.weak_mark_lemmas CertiGraph.msl_application.Graph CertiGraph.msl_application.Graph_Mark CertiGraph.msl_application.GraphBin CertiGraph.msl_application.GraphBin_Mark Coq.Logic.Classical