proposition: Lemma edge_copy_spec': forall root es e0 es_done es_later (g g1 g2 g3 g1' g2' g3': Graph), vvalid g root -> WeakMarkGraph.unmarked g root -> es = es_done ++ e0 :: es_later -> (forall e, In e es <-> out_edges g root e) -> NoDup es -> vcopy1 root g g1 g1' -> relation_list (map (LocalGraphCopy.edge_copy g root (WeakMarkGraph.marked g)) (cprefix es_done)) (g1, g1') (g2, g2') -> relation_list (map (fun v => WeakMarkGraph.componded root (WeakMarkGraph.mark v)) (map (dst g) es_done)) g1 g2-> edge_copy g e0 (g2, g2') (g3, g3') -> LocalGraphCopy.edge_copy g root (WeakMarkGraph.marked g) (es_done, e0) (g2, g2') (g3, g3') /\ WeakMarkGraph.componded root (WeakMarkGraph.mark (dst g e0)) g2 g3.
proof: Proof. intros. destruct H4 as [_ [? ?]]. pose proof WeakMarkGraph.triple_mark1_componded_mark_list root (map (dst g) es_done) (map (dst g) (e0 :: es_later)) (map (dst g) es) g g2 H H0. spec H9; [apply out_edges_step_list; auto |]. spec H9; [rewrite <- map_app; f_equal; auto |]. spec H9; [split_relation_list (g :: g1 :: g1 :: nil) |]. 1: apply WeakMarkGraph.eq_do_nothing; auto. 1: auto. 1: apply WeakMarkGraph.eq_do_nothing; auto. 1: auto. cbv iota zeta in H9. pose proof LocalGraphCopy.triple_vcopy1_edge_copy_list g g1 g2 g1' g2' root es es_done (e0 :: es_later) (WeakMarkGraph.marked g) H H0 H2 H3 H1. spec H10; [intro v; destruct (node_pred_dec (WeakMarkGraph.marked g) v); auto |]. specialize (H10 H8 H5). cbv iota zeta in H10. assert (evalid g2 e0 /\ src g e0 = root). 1: { destruct H10 as [_ [? _]]. rewrite <- (proj1 (proj2 H10)); auto. assert (In e0 es) by (rewrite H1, in_app_iff; simpl; auto). rewrite H2 in H11. auto. } apply edge_copy_spec; auto. + tauto. + destruct H10 as [_ [? _]], H11 as [? ?]. erewrite <- si_src2 by eauto. auto. + destruct H9 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