proposition: Lemma vcopy1_edge_copy_list_spec: forall root es es_done es_later (g g1 g2 g1' g2': Graph), vvalid g root -> WeakMarkGraph.unmarked g root -> es = es_done ++ es_later -> (forall e, In e es <-> out_edges g root e) -> NoDup es -> vcopy1 root g g1 g1' -> edge_copy_list g es_done (g1, g1') (g2, g2') -> LocalGraphCopy.edge_copy_list g root es_done (WeakMarkGraph.marked g) (g1, g1') (g2, g2') /\ WeakMarkGraph.componded_mark_list root (map (dst g) es_done) g1 g2.
proof: Proof. intros. unfold edge_copy_list in H5. rewrite map_snd_cprefix' in H5. eapply relation_list_weaken_ind' with (R' := fun (p: list E * E) => relation_conjunction (LocalGraphCopy.edge_copy g root (WeakMarkGraph.marked g) p) (fst_relation (WeakMarkGraph.componded root (WeakMarkGraph.mark (dst g (snd p)))))) in H5. + apply relation_list_conjunction in H5. destruct H5. split; auto. rewrite <- map_map in H6. unfold fst_relation in H6. apply respectful_relation_list in H6. unfold respectful_relation in H6; simpl in H6. unfold WeakMarkGraph.componded_mark_list. rewrite map_map. rewrite map_snd_cprefix'. auto. + clear g2 g2' H5. intros. clear H6. unfold relation_conjunction, predicate_intersection; simpl. destruct a2 as [g2 g2'], a3 as [g3 g3']. unfold fst_relation, respectful_relation; simpl. pose proof in_cprefix _ _ _ H5. apply in_cprefix_cprefix in H5. subst bs_done. destruct b0 as [es_done0 e0]; simpl in H7 |- *. pose proof in_cprefix' _ _ _ H6. destruct H5 as [es_later0 ?]. apply relation_list_conjunction in H7. destruct H7. rewrite <- (map_map (snd) (fun e => fst_relation (WeakMarkGraph.componded root (WeakMarkGraph.mark (dst g e))))) in H9. rewrite map_snd_cprefix in H9. rewrite <- map_map in H9. unfold fst_relation in H9. apply respectful_relation_list in H9. unfold respectful_relation in H9; simpl in H9. subst es_done. rewrite <- app_assoc in H1. eapply edge_copy_spec'; try eassumption. rewrite map_map; 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