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