proposition: Lemma vcopy1_edge_copy_list_weak_copy_extended_copy: forall {P: Graph -> Type} {NP: NormalGeneralGraph P}, forall root es es_done e0 es_later (g1 g2 g3 g2' g3' g4 g4'': Graph) (root0: V), vvalid g1 root -> WeakMarkGraph.unmarked g1 root -> es = es_done ++ e0 :: es_later -> (forall e, In e es <-> out_edges g1 root e) -> NoDup es -> vcopy1 root g1 g2 g2' -> edge_copy_list g1 es_done (g2, g2') (g3, g3') -> root0 = LocalGraphCopy.vmap g2 root -> copy (dst g1 e0) g3 g4 g4'' -> disjointed_guard (vvalid g4'') (vvalid g3') (evalid g4'') (evalid g3') -> (exists Pg3': P (gpredicate_sub_labeledgraph (fun v' => root0 <> v') (fun e' => ~ In e' (map (LocalGraphCopy.emap g3) es_done)) g3'), True) -> (exists Pg4'': P g4'', True) -> exists g4': Graph, extended_copy (dst g1 e0) (g3, g3') (g4, g4') /\ (exists Pg4': P (gpredicate_sub_labeledgraph (fun v' => root0 <> v') (fun e' => ~ In e' (map (LocalGraphCopy.emap g4) es_done)) g4'), True) /\ guarded_labeled_graph_equiv (vvalid g4'') (evalid g4'') g4'' g4' /\ guarded_labeled_graph_equiv (vvalid g3') (evalid g3') g3' g4'.
proof: Proof. intros. pose proof vcopy1_edge_copy_list_copy_extended_copy root es es_done e0 es_later g1 g2 g3 g2' g3' g4 g4''. repeat (spec H11; [auto |]). destruct H11 as [g4' [? [? ?]]]. exists g4'; split; [| split; [| split]]; auto. destruct H9 as [? _], H10 as [? _]. apply (lge_preserved _ (gpredicate_sub_labeledgraph (Intersection _ (vvalid g3') (fun v' : V => root0 <> v')) (Intersection _ (evalid g3') (fun e' : E => ~ In e' (map (LocalGraphCopy.emap g3) es_done))) g4')) in x. 2: { etransitivity. + apply gpredicate_sub_labeledgraph_equiv. - symmetry; apply Intersection_absort_left. apply Intersection1_Included, Included_refl. - symmetry; apply Intersection_absort_left. apply Intersection1_Included, Included_refl. + eapply stronger_gpredicate_sub_labeledgraph_simple; [| | eauto]. - apply Intersection1_Included, Included_refl. - apply Intersection1_Included, Included_refl. } apply (lge_preserved _ (gpredicate_sub_labeledgraph (vvalid g4'') (evalid g4'') g4')) in x0. 2: { etransitivity. + symmetry; apply gpredicate_sub_labeledgraph_self. + eapply stronger_gpredicate_sub_labeledgraph_simple; [| | eauto]. - apply Included_refl. - apply Included_refl. } eexists; auto. apply (lge_preserved (gpredicate_sub_labeledgraph (Intersection _ (vvalid g4') (fun v' : V => root0 <> v')) (Intersection _ (evalid g4') (fun e' : E => ~ In e' (map (LocalGraphCopy.emap g4) es_done))) g4')). 1: { apply gpredicate_sub_labeledgraph_equiv. + apply Intersection_absort_left. apply Intersection1_Included, Included_refl. + apply Intersection_absort_left. apply Intersection1_Included, Included_refl. } eapply join_preserved; [| | exact x | exact x0]. + destruct H11 as [_ [_ HH]]. destruct HH as [_ [_ [_ [HH _]]]]. destruct H7 as [_ [_ ?]]. destruct HH as [? _]. destruct H7 as [_ [_ [_ [? _]]]]. rewrite <- H7 in H9. apply Prop_join_shrink1; auto. destruct (vcopy1_edge_copy_list_spec root _ _ _ _ _ _ _ _ H H0 H1 H2 H3 H4 H5). eapply LocalGraphCopy.edge_copy_list_vvalid_mono in H10; [exact H10 |]. destruct H4 as [_ [_ ?]]. eapply LocalGraphCopy.vcopy1_copied_root_valid in H4; eauto. + replace (map (@LocalGraphCopy.emap V E V E (@SGBA_VE V E SGBA) (@SGBA_EE V E SGBA) V E M V E M GMS g4) es_done) with (map (LocalGraphCopy.emap g3) es_done) by (apply (extend_copy_emap_root g1 g2 g3 g4 g2' g3' g4' root es es_done e0 es_later); auto). destruct H11 as [_ [_ HH]]. destruct HH as [_ [_ [_ [HH _]]]]. destruct H7 as [_ [_ ?]]. destruct HH as [_ [? _]]. destruct H7 as [_ [_ [_ [_ [? _]]]]]. rewrite <- H7 in H9. apply Prop_join_shrink; auto. unfold Included, Ensembles.In. intros e ? ?. destruct H9 as [_ ?]. apply (H9 e); auto. destruct (vcopy1_edge_copy_list_spec root _ _ _ _ _ _ _ _ H H0 H1 H2 H3 H4 H5). eapply (LocalGraphCopy.vcopy1_edge_copy_list_mapped_root_edge_evalid g1 g2 g3 g2' g3'); eauto. 1: intros; destruct (node_pred_dec (WeakMarkGraph.marked g1) v); auto. 1: destruct H4 as [? [? ?]]; auto. Qed.
imports: VST.msl.seplog VST.msl.log_normalize CertiGraph.lib.Coqlib CertiGraph.lib.Ensembles_ext CertiGraph.lib.EquivDec_ext CertiGraph.lib.List_ext CertiGraph.lib.relation_list CertiGraph.lib.Morphisms_ext CertiGraph.msl_ext.log_normalize CertiGraph.msl_ext.iter_sepcon CertiGraph.msl_ext.ramification_lemmas 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 Coq.Logic.Classical