proposition: Lemma edge_copy_spec: forall (g g1 g2 g1' g2': Graph) (root: V) (es_done: list E) (e0: E), edge_copy g e0 (g1, g1') (g2, g2') -> evalid g1 e0 -> src g1 e0 = root -> Same_set (WeakMarkGraph.marked g1) (let M0 := Union _ (WeakMarkGraph.marked g) (eq root) in let PV1 := reachable_by_through_set g (map (dst g) es_done) (Complement _ M0) in let M_rec := Union _ M0 PV1 in M_rec) -> LocalGraphCopy.edge_copy g root (WeakMarkGraph.marked g) (es_done, e0) (g1, g1') (g2, g2') /\ WeakMarkGraph.componded root (WeakMarkGraph.mark (dst g e0)) g1 g2.
proof: Proof. intros. unfold edge_copy in H. destruct_relation_list gg in H; destruct gg as [g3 g3']. destruct H as [? [? ?]], H3 as [? [? ?]]. split. + cbv iota zeta in H2. unfold LocalGraphCopy.edge_copy. erewrite app_same_relation by (rewrite <- H2; reflexivity). split_relation_list ((g3, g3') :: nil); auto. + unfold WeakMarkGraph.componded. apply compond_intro with g3. 2: { erewrite <- si_src1 in H4; [| exact H3 | exact H0]. rewrite <- H1; auto. } apply compond_intro with g1; [apply WeakMarkGraph.eq_do_nothing; auto |]. 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