proposition: Lemma copy_final: forall (g g1 g2 g3 g4 g5: Graph) (g1' g2' g3' g4' g5': LGraph) x l r x0 l0 r0, vvalid g x -> vgamma g x = (null, l, r) -> x0 = LocalGraphCopy.vmap g1 x -> l = null /\ l0 = null \/ l0 = LocalGraphCopy.vmap g2 l -> forall (H999: dst g3' (x0, L) = l0), (x0, L) = LocalGraphCopy.emap g3 (x, L) -> r = null /\ r0 = null \/ r0 = LocalGraphCopy.vmap g4 r -> forall (H998: dst g5' (x0, R) = r0), (x0, R) = LocalGraphCopy.emap g5 (x, R) -> is_guarded_BinMaFin' (fun v => x0 <> v) (fun e => ~ In e ((x0, L) :: (x0, R) :: nil)) g5' -> vcopy1 x g g1 g1' -> extended_copy l (g1: LGraph, g1') (g2: LGraph, g2') -> ecopy1 (x, L) (g2: LGraph, g2') (g3: LGraph, g3') -> extended_copy r (g3: LGraph, g3') (g4: LGraph, g4') -> ecopy1 (x, R) (g4: LGraph, g4') (g5: LGraph, g5') -> @derives pred _ (vertex_at x0 (null, l0, r0) * vertices_at (Intersection _ (vvalid g5') (fun v => x0 <> v)) g5') (EX gg5': Graph', !! (copy x g g5 gg5' /\ LocalGraphCopy.vmap g1 x = LocalGraphCopy.vmap g5 x) && reachable_vertices_at x0 gg5').
proof: Proof. intros. assert (copy x g g5 g5'). { eapply vcopy1_edge_copy_list_copy. + assumption. + simpl in H0 |- *; unfold Complement, Ensembles.In. congruence. + intros; apply (binGraph_out_edges g (binGraph _)); auto. + repeat constructor; intro HH; inversion HH; inversion H12. + exact H7. + hnf. exists (g3: LGraph, g3'). - exists (g1: LGraph, g1'); auto. exists (g2: LGraph, g2'). * exists (g1: LGraph, g1'); auto. simpl in H0. inversion H0. rewrite H14. exact H8. * exact H9. - hnf. exists (g4: LGraph, g4'). * exists (g3: LGraph, g3'); auto. simpl in H0. inversion H0. rewrite H15. exact H10. * exact H11. } rewrite (add_andp _ _ (vertex_at_not_null x0 (null, l0, r0))). normalize. assert (x0 <> null) as LOCAL' by congruence; clear H13. assert (LocalGraphCopy.vmap g5 x = x0 /\ src g5' (x0, L) = x0 /\ src g5' (x0, R) = x0 /\ dst g5' (x0, L) = l0 /\ dst g5' (x0, R) = r0 /\ evalid g5' (x0, L) /\ evalid g5' (x0, R) /\ vvalid g5' x0) as LOCAL. { pose proof fun H => extended_copy_vmap_root _ _ _ _ _ x H H8 as Hvmap12. specialize (Hvmap12 ltac:(simpl in H1 |- *; subst x0; congruence)). pose proof ecopy1_vmap_root _ _ _ _ _ x H9 as Hvmap23. pose proof fun H => extended_copy_vmap_root _ _ _ _ _ x H H10 as Hvmap34. specialize (Hvmap34 ltac:(simpl in H1, Hvmap12, Hvmap23 |- *; subst x0; congruence)). pose proof ecopy1_vmap_root _ _ _ _ _ x H11 as Hvmap45. split; [congruence |]. pose proof vcopy1_copied_root_valid _ _ _ _ _ H7 H1 as Hx0_g5'. apply (extended_copy_vvalid_mono _ _ _ _ _ _ H8) in Hx0_g5'. apply (ecopy1_vvalid_mono _ _ _ _ _ _ H9) in Hx0_g5'. apply (extended_copy_vvalid_mono _ _ _ _ _ _ H10) in Hx0_g5'. apply (ecopy1_vvalid_mono _ _ _ _ _ _ H11) in Hx0_g5'. assert (vvalid g2 x) as Hx_g2. { rewrite <- (proj1 (proj1 H8)), <- (proj1 (proj1 H7)). auto. } assert (vvalid g3 x) as Hx_g3. { rewrite <- (proj1 (proj1 H9)). auto. } assert (vvalid g4 x) as Hx_g4. { rewrite <- (proj1 (proj1 H10)). auto. } assert (vvalid g5 x) as Hx_g5. { rewrite <- (proj1 (proj1 H11)). auto. } assert (src g3' (x0, L) = x0 /\ dst g3' (x0, L) = l0 /\ evalid g3' (x0, L)) as [Hx0L_src [Hx0L_dst Hx0L_v]]. { destruct H9 as [_ [_ ?]]. destruct H9 as [? [? [? [? [? ?]]]]]. destruct H15 as [_ [? _]]. destruct H15 as [? _]. rewrite (H15 (x0, L)). rewrite left_right_sound in H16 by auto. rewrite <- H3 in *. rewrite <- H16 by auto. simpl in H0; inversion H0. split; [congruence | split; tauto]. } pose proof (extended_copy_evalid_mono _ _ _ _ _ _ H10 Hx0L_v) as Hx0L_v'. pose proof proj2 (proj2 H10). destruct H13 as [_ [_ [_ [? [_ _]]]]]. destruct H13 as [_ [_ [? ?]]]. rewrite H13 in Hx0L_src by auto. rewrite H14 in Hx0L_dst by auto. clear H13 H14 Hx0L_v; rename Hx0L_v' into Hx0L_v. pose proof (ecopy1_evalid_mono _ _ _ _ _ _ H11 Hx0L_v) as Hx0L_v'. pose proof proj2 (proj2 H11). destruct H13 as [_ [_ [_ [? [_ _]]]]]. destruct H13 as [_ [_ [? ?]]]. rewrite H13 in Hx0L_src by auto. rewrite H14 in Hx0L_dst by auto. clear H13 H14 Hx0L_v; rename Hx0L_v' into Hx0L_v. assert (src g5' (x0, R) = x0 /\ dst g5' (x0, R) = r0 /\ evalid g5' (x0, R)) as [Hx0R_src [Hx0R_dst Hx0R_v]]. { destruct H11 as [_ [_ ?]]. destruct H11 as [? [? [? [? [? ?]]]]]. destruct H15 as [_ [? _]]. destruct H15 as [? _]. rewrite (H15 (x0, R)). rewrite left_right_sound in H16 by auto. rewrite <- H5 in *. rewrite <- H16 by auto. simpl in H0; inversion H0. split; [congruence | split; tauto]. } tauto. } pose proof H6. destruct H13 as [? _]. assert (BinMaFin' g5'). { constructor. + constructor. - intros. congruence. - intros. destruct (classic (x0 = x2)). * subst x2. destruct (classic (e = (x0, L))); [| destruct (classic (e = (x0, R)))]. ++ subst e; tauto. ++ subst e; tauto. ++ split; [intros [? ?]; exfalso | tauto]. pose proof @ma' _ _ x1. pose proof @valid_graph' _ _ _ _ _ _ H18 e. simpl in H19. rewrite !Intersection_spec in H19. specialize (H19 ltac:(pose proof @eq_sym _ (x0, L) e; pose proof @eq_sym _ (x0, R) e; tauto)). rewrite H16 in H19. tauto. * pose proof @bin' _ _ x1. pose proof @only_two_edges _ _ _ _ _ _ _ H15 x2 e. simpl in H16. rewrite !Intersection_spec in H16. specialize (H16 ltac:(tauto)). rewrite <- H16; split; [| tauto]. intros [? ?]; repeat split; auto. intros [| [| []]]; subst e; rewrite <- H17 in H14; apply H14; symmetry; tauto. + constructor. - intros. destruct (classic ((x0, L) = e)); [| destruct (classic ((x0, R) = e))]. * unfold is_null_SGBA; simpl. subst e. replace (src g5' (x0, L)) with x0 by (symmetry; tauto). tauto. * unfold is_null_SGBA; simpl. subst e. replace (src g5' (x0, R)) with x0 by (symmetry; tauto). tauto. * pose proof @ma' _ _ x1. pose proof @valid_graph' _ _ _ _ _ _ H16. unfold weak_valid in H17. simpl in H17. specialize (H17 e). rewrite !Intersection_spec in H17. specialize (H17 ltac:(tauto)). tauto. - intros. pose proof @ma' _ _ x1. pose proof @valid_not_null' _ _ _ _ _ _ H15. specialize (H16 x2). simpl in H16. rewrite Intersection_spec in H16. destruct (classic (x0 = x2)); [subst x2 |]; tauto. + assert (FiniteGraph (gpredicate_sub_labeledgraph (fun v : addr => x0 = v) (fun e : addr * LR => In e ((x0, L) :: (x0, R) :: nil)) g5')). { constructor; simpl. - exists (x0 :: nil). split; [repeat constructor; intros [] |]. intros. rewrite Intersection_spec. split; intros. * destruct H13 as [|[]]. subst x2. tauto. * left. tauto. - exists ((x0, L) :: (x0, R) :: nil). split; [repeat constructor; [intros [| []]; congruence | intros []] |]. intros. rewrite Intersection_spec. split; intros. * destruct H13 as [| [| []]]; subst x2; tauto. * simpl. tauto. } apply (@fin' _ _) in x1. pose proof fun H H0 => finite_graph_join g5' _ _ (fun _ => True) _ _ (fun _ => True) H H0 x1 X. spec X0. { split. + intros; tauto. + intros; tauto. } spec X0. { split. + intros; tauto. + intros; tauto. } pose proof @gpredicate_sub_labeledgraph_equiv _ _ _ _ _ _ _ g5' (fun _ => True) (vvalid g5') (fun _ => True) (evalid g5'). spec H13. { rewrite Same_set_spec; intro; rewrite !Intersection_spec; tauto. } spec H13. { rewrite Same_set_spec; intro; rewrite !Intersection_spec; tauto. } pose proof finite_graph_si _ _ (proj1 H13); clear H13. pose proof @gpredicate_sub_labeledgraph_self _ _ _ _ _ _ _ g5'. pose proof finite_graph_si _ _ (proj1 H13); clear H13. apply X2, X1, X0. } apply (exp_right (Build_GeneralGraph _ _ _ _ (labeledgraph_vgen g5' x0 null) X)); clear x1. apply andp_right. + apply prop_right. split; auto. rewrite <- H1; symmetry; tauto. + match goal with | |- _ |-- _ ?A => change A with (labeledgraph_vgen g5' x0 null) end. replace (vertices_at (Intersection addr (vvalid g5') (fun v : addr => x0 <> v)) g5') with (vertices_at (Intersection addr (vvalid g5') (fun v : addr => x0 <> v)) (LGraph_SGraph (labeledgraph_vgen g5' x0 null))). 2: { apply vertices_at_vertices_identical. rewrite (update_irr _ g5' x0) by (rewrite Intersection_spec; tauto). apply (GSG_VGenPreserve (Intersection addr (vvalid g5') (fun v : addr => x0 <> v)) g5'). + reflexivity. + unfold Included, Ensembles.In; intro; rewrite Intersection_spec. intros [? _]. apply (vvalid_vguard' (Build_GeneralGraph _ _ _ _ g5' X)), H13. + unfold Included, Ensembles.In; intro; rewrite Intersection_spec. intros [? _]. apply (vvalid_vguard' (Build_GeneralGraph _ _ _ _ g5' X)), H13. } change (vvalid g5') with (vvalid (labeledgraph_vgen g5' x0 null)). apply derives_refl', vertices_at_sepcon_1x. - apply Prop_join_comm. rewrite <- copy_vvalid_weak_eq; [apply Ensemble_join_Intersection_Complement | .. | exact H12]. * unfold Included, Ensembles.In; intros; subst; tauto. * intros; tauto. * right; symmetry; tauto. - change (vgamma (Graph_PointwiseGraph (labeledgraph_vgen g5' x0 null)) x0) with (vgamma (LGraph_SGraph (labeledgraph_vgen g5' x0 null)) x0). simpl. unfold update_vlabel. rewrite if_true by reflexivity. repeat f_equal; 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