proposition: Lemma extend_copy_left: forall (g g1 g2: Graph) (g1': LGraph) (g2'': Graph') (x l r x0 l0: addr) d0, vvalid g x -> vgamma g x = (null, l, r) -> vcopy1 x g g1 g1' -> copy l g1 g2 g2'' -> x0 = LocalGraphCopy.vmap g1 x -> l = null /\ l0 = null \/ l0 = LocalGraphCopy.vmap g2 l -> is_guarded_BinMaFin' (fun v => x0 <> v) (fun e => ~ In e nil) g1' -> @derives pred _ (vertex_at x0 d0 * vertices_at (Intersection _ (vvalid g1') (fun x => x0 <> x)) g1' * reachable_vertices_at l0 g2'') (EX g2': LGraph, !! (extended_copy l (g1: LGraph, g1') (g2: LGraph, g2') /\ is_guarded_BinMaFin' (fun v => x0 <> v) (fun e => ~ In e nil) g2') && (vertex_at x0 d0 * vertices_at (Intersection _ (vvalid g2') (fun x => x0 <> x)) g2')).
proof: Proof. intros. rename H5 into BMF. inversion H0. pose proof @vcopy1_edge_copy_list_weak_copy_extended_copy' _ _ _ _ _ _ _ _ _ _ BinMaFin'_Normal x ((x, L) :: (x, R) :: nil) nil (x, L) ((x, R) :: nil) g g1 g1 g1' g1' g2 g2'' x0 H. spec H5; [simpl; unfold Complement, Ensembles.In; congruence |]. spec H5; [reflexivity |]. spec H5; [intros; apply (binGraph_out_edges g (binGraph _)); auto |]. spec H5; [repeat constructor; intro HH; inversion HH; inversion H9 |]. spec H5; [auto |]. spec H5; [hnf; auto |]. spec H5; [auto |]. spec H5; [subst l; auto |]. unfold reachable_vertices_at. pose proof vertices_at_sepcon_unique_1x (Graph_PointwiseGraph g2'') x0 (reachable g2'' l0) d0. pose proof vertices_at_sepcon_unique_xx g1' (Graph_PointwiseGraph g2'') (Intersection _ (vvalid g1') (fun x => x0 <> x)) (reachable g2'' l0). rewrite sepcon_assoc, (add_andp _ _ H10); normalize. rewrite (sepcon_comm (vertices_at _ _)), <- sepcon_assoc, (add_andp _ _ H9); normalize. clear H9 H10. spec H5. { apply is_BinMaFin_disjoint_guard with (x0 := x0) (es0 := nil); auto. + eapply vcopy1_copied_root_valid in H1; auto. subst x0; auto. + intros ? []. + apply (vmap_weaken g1 g2'') in H4. rewrite (copy_vvalid_weak_eq g1 g2 g2'' l l0 H4 H2). apply Disjoint_comm. apply (Disjoint_x1' _ _ _ H11 H12). } unfold map in H5; rewrite H3 in BMF. rewrite <- H3 in BMF; specialize (H5 BMF). specialize (H5 (Graph'_is_BinMaFin' _)). destruct H5 as [g2' [? [? [? ?]]]]. apply (exp_right g2'). pose proof vertex_at_not_null x0 d0. rewrite (add_andp _ _ H14) at 1. rewrite andp_comm, !sepcon_andp_prop'. apply derives_extract_prop. intro. clear H14. assert (x0 <> null) by congruence; clear H15. apply andp_right; [apply prop_right; split; auto | rewrite sepcon_assoc; apply sepcon_derives; auto]. assert (Prop_join (vvalid g1') (vvalid g2'') (vvalid g2')) as HPJ. 1: { eapply copy_and_extended_copy; eauto. rewrite <- H7; auto. } assert (Prop_join (Intersection addr (vvalid g1') (fun x1 : addr => x0 <> x1)) (vvalid g2'') (Intersection addr (vvalid g2') (fun x1 : addr => x0 <> x1))) as HPJ1. 1: { apply Prop_join_shrink1; auto. eapply vcopy1_copied_root_valid in H1; auto. rewrite H3; auto. } rewrite (vertices_at_vertices_identical (Graph_PointwiseGraph g2'') (LGraph_SGraph g2')). rewrite (vertices_at_vertices_identical (LGraph_SGraph g1') (LGraph_SGraph g2')). + erewrite vertices_at_sepcon_xx; [apply derives_refl |]. rewrite Prop_join_comm. apply (vmap_weaken g1 g2'') in H4. rewrite <- (copy_vvalid_weak_eq g1 g2 g2'' l l0 H4 H2). auto. + rewrite <- H3 in H13. apply H13. - unfold Included, Ensembles.In; intros. destruct BMF as [BMF _]. pose (pg1 := Build_GeneralGraph _ _ _ (fun g: LGraph => BinMaFin' g) (gpredicate_sub_labeledgraph (fun v => x0 <> v) (fun e : addr * LR => ~ In e nil) g1') BMF: Graph'). assert (vvalid pg1 x1) by (simpl; auto). apply vvalid_vguard' in H16. simpl in H16. rewrite !Intersection_spec in H16. simpl; tauto. - unfold Included, Ensembles.In; intros. destruct H9 as [X _]. pose (pg2 := Build_GeneralGraph _ _ _ (fun g: LGraph => BinMaFin' g) (gpredicate_sub_labeledgraph (fun v => x0 <> v) (fun e : addr * LR => ~ In e nil) g2') X: Graph'). assert (vvalid pg2 x1). simpl. rewrite Intersection_spec in H15 |- *. rewrite (proj1 HPJ); tauto. apply vvalid_vguard' in H9. simpl in H9. rewrite !Intersection_spec in H9. simpl; tauto. + apply (vmap_weaken g1 g2'') in H4. pose proof copy_vvalid_weak_eq _ _ _ _ _ H4 H2. rewrite <- H15. apply H10. - intros ? ?; apply vvalid_vguard'; auto. - unfold Included, Ensembles.In; intros. destruct H9 as [X _]. pose (pg2 := Build_GeneralGraph _ _ _ (fun g: LGraph => BinMaFin' g) (gpredicate_sub_labeledgraph (fun v => x0 <> v) (fun e : addr * LR => ~ In e nil) g2') X: Graph'). assert (vvalid pg2 x1). simpl. rewrite (proj1 HPJ1). tauto. apply vvalid_vguard' in H9. simpl in H9. rewrite !Intersection_spec in H9. simpl; tauto. 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