proposition: Lemma graph_ramify_right: forall (g g1 g2 g3: Graph) (g1' g2' g3': LGraph) (x l r: addr) (F1 F2: pred) F3, vvalid g x -> vgamma g x = (null, l, r) -> vcopy1 x g g1 g1' -> extended_copy l (g1: LGraph, g1') (g2: LGraph, g2') -> ecopy1 (x, L) (g2: LGraph, g2') (g3: LGraph, g3') -> F1 * (F2 * reachable_vertices_at x g3) |-- reachable_vertices_at r g3 * (ALL a: Graph' * Graph * addr, !! (copy r g3 (snd (fst a)) (fst (fst a)) /\ (r = null /\ snd a = null \/ snd a = LocalGraphCopy.vmap (snd (fst a)) r)) --> (reachable_vertices_at r (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]. + destruct H2 as [? _], H3 as [? _]; rewrite <- s0, <- s, <- H1. eapply Prop_join_reachable_right; eauto. + intros. destruct H6 as [[? [? ?]] _]. destruct H2 as [? _], H3 as [? _]. rewrite <- H6, <- H3, <- H2, <- H1. eapply Prop_join_reachable_right; eauto. + intros [[[? ?] ?] ?] [? _]. destruct H2 as [? _], H3 as [? _]; rewrite H2, H3 in H1. simpl in H6 |- *. rewrite vertices_identical_spec. intros. simpl. destruct H6 as [? [? ?]]. f_equal; [f_equal |]. - destruct H9 as [_ [? _]]. rewrite guarded_pointwise_relation_spec in H9. apply H9; clear H9. unfold Complement, Ensembles.In. intro. apply reachable_by_is_reachable in H9. rewrite Intersection_spec in H7. rewrite <- H1 in H9. destruct H7; auto. - apply dst_L_eq; auto. rewrite Intersection_spec in H7. destruct H7 as [? _]. rewrite H1 in H7. apply reachable_foot_valid in H7; auto. - apply dst_R_eq; auto. rewrite Intersection_spec in H7. destruct H7 as [? _]. rewrite H1 in H7. apply reachable_foot_valid in H7; 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