proposition: Lemma graph_ramify_left: forall (g g1: Graph) (g1': LGraph) (x l r: addr) (F1 F2: pred) F3, vvalid g x -> vgamma g x = (null, l, r) -> vcopy1 x g g1 g1' -> F1 * (F2 * reachable_vertices_at x g1) |-- reachable_vertices_at l g1 * (ALL a: Graph' * Graph * addr, !! (copy l g1 (snd (fst a)) (fst (fst a)) /\ (l = null /\ snd a = null \/ snd a = LocalGraphCopy.vmap (snd (fst a)) l)) --> (reachable_vertices_at l (snd (fst a)) * F3 (snd a) (fst (fst a)) -* F1 * (F2 * (reachable_vertices_at x (snd (fst a)) * F3 (snd a) (fst (fst a)))))).
proof: Proof. intros. destruct H1 as [? [? ?]]. rewrite <- sepcon_assoc, (sepcon_comm (F1 * F2)). RAMIF_Q'.formalize. match goal with | |- _ |-- _ * allp (_ --> (_ -* ?A)) => replace A with (fun p : Graph' * Graph * addr => reachable_vertices_at x (snd (fst p)) * F3 (snd p) (fst (fst p)) * (F1 * F2)) by (extensionality p; rewrite <- (sepcon_assoc F1 F2), (sepcon_comm _ (F1 * F2)); auto) end. apply RAMIF_Q'.frame; [auto |]. apply RAMIF_Q'.frame_post; [auto |]. simpl. eapply vertices_at_ramif_xQ. eexists. split; [| split]. + rewrite <- H1. eapply Prop_join_reachable_left; eauto. + intros. destruct H4 as [[? [? ?]] _]. rewrite <- H4, <- H1. eapply Prop_join_reachable_left; eauto. + intros [[? ?] ?] [? _]. simpl in H4 |- *. rewrite vertices_identical_spec. intros. simpl. destruct H4 as [? [? ?]]. f_equal; [f_equal |]. - destruct H7 as [_ [? _]]. rewrite guarded_pointwise_relation_spec in H7. apply H7; clear H7. unfold Complement, Ensembles.In. intro. apply reachable_by_is_reachable in H7. rewrite Intersection_spec in H5. rewrite <- H1 in H7. destruct H5; auto. - apply dst_L_eq; auto. rewrite Intersection_spec in H5. destruct H5 as [? _]. rewrite H1 in H5. apply reachable_foot_valid in H5; auto. - apply dst_R_eq; auto. rewrite Intersection_spec in H5. destruct H5 as [? _]. rewrite H1 in H5. apply reachable_foot_valid in H5; auto. Qed.
imports: CertiGraph.lib.Ensembles_ext Coq.Lists.List VST.msl.seplog VST.msl.log_normalize VST.msl.ramification_lemmas VST.msl.Coqlib2 CertiGraph.lib.Coqlib CertiGraph.lib.EquivDec_ext CertiGraph.lib.relation_list CertiGraph.lib.Morphisms_ext 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.graph_gen CertiGraph.graph.graph_relation CertiGraph.graph.subgraph2 CertiGraph.graph.dag CertiGraph.graph.weak_mark_lemmas CertiGraph.graph.graph_morphism CertiGraph.graph.local_graph_copy CertiGraph.msl_application.Graph CertiGraph.msl_application.GraphBin CertiGraph.msl_application.Graph_Copy Coq.Logic.Classical