proposition: Lemma triple3_copy: forall (g g1 g2: Graph) (g1' g2': Graph') (M: V -> Prop) root es es_done e0 es_later, let M0 := Union _ M (eq root) in let PV1 := reachable_by_through_set g (map (dst g) es_done) (Complement _ M0) in let PE1 := Intersection _ (weak_edge_prop PV1 g) (evalid g) in let PE1_root e := In e es_done in let PV3 := reachable_by_through_set g (map (dst g) (es_done ++ e0 :: nil)) (Complement _ M0) in let PE3 := Intersection _ (weak_edge_prop PV3 g) (evalid g) in let M_rec := Union _ M0 PV1 in let PV0 := reachable_by g (dst g e0) (Complement _ M_rec) in let PE0 := Intersection _ (weak_edge_prop PV0 g) (evalid g) in vvalid g root -> ~ M root -> (forall e, In e es <-> out_edges g root e) -> es = es_done ++ e0 :: es_later -> guarded_bij (Union _ PV1 (eq root)) (Union _ PE1 PE1_root) (vmap g1) (emap g1) g1 g1' /\ Same_set (vvalid g1') (image_set (Union _ PV1 (eq root)) (vmap g1)) /\ Same_set (evalid g1') (image_set (Union _ PE1 PE1_root) (emap g1)) /\ g ~=~ g1 /\ (forall e, Union _ PE1 PE1_root e -> Complement _ (Union _ PV1 (eq root)) (dst g1 e) -> vvalid g (dst g1 e) -> vmap g1 (dst g1 e) = dst g1' (emap g1 e)) -> extended_copy M_rec (dst g e0) (g1, g1') (g2, g2') -> (forall v, M v \/ ~ M v) -> (forall e, Union _ PE3 PE1_root e -> Complement _ (Union _ PV3 (eq root)) (dst g2 e) -> vvalid g (dst g2 e) ->vmap g2 (dst g2 e) = dst g2' (emap g2 e)).
proof: Proof. intros until es_later. intros ? ? ? ? ? ? ? ? ?. intros H_VVALID H_P H_OUT_EDGES H_ES [PRE_bij [PRE_vvalid [PRE_evalid [PRE_si PRE_consi]]]] COPY M_DEC. assert (forall e, PE0 e -> ~ g |= dst g e0 ~o~> dst g e satisfying (Complement _ M_rec) -> vvalid g (dst g2 e) -> vmap g2 (dst g2 e) = dst g2' (emap g2 e)) as COPY_consi by (eapply triple_aux4_copy; eauto). destruct COPY as [COPY_si [COPY_gprv [COPY_gpre [COPY_pj [_ [COPY_DEC COPY_bij]]]]]]. rewrite <- PRE_si in COPY_gprv at 1. rewrite <- PRE_si in COPY_gpre at 1. rewrite <- (weak_edge_prop_si _ _ _ PRE_si) in COPY_gpre. rewrite <- PRE_si in COPY_pj at 1 2. rewrite <- (weak_edge_prop_si _ _ _ PRE_si) in COPY_pj. rewrite <- PRE_si in COPY_bij at 1 2. rewrite <- (weak_edge_prop_si _ _ _ PRE_si) in COPY_bij. intros ? ? ? H_EXTRA. erewrite app_same_set in H by (eapply (aux19 PE1 PE1_root PE3 PE0); eauto; reflexivity). erewrite app_same_set in H0 by (erewrite (aux18 root PV1 PV3 PV0) by (eauto; reflexivity); reflexivity). erewrite app_same_set in H0 by (symmetry; apply Intersection_Complement). rewrite Intersection_spec in H0; destruct H0. rewrite Union_spec in H; destruct H. + assert (evalid g e). 1: { rewrite Union_spec in H. destruct H; revert H; [eapply aux21 | eapply aux22]; eauto; reflexivity. } assert (vvalid g (dst g1 e)) as H_EXTRA'. 1: { rewrite (proj1 (proj2 PRE_si)) in H2. rewrite (si_dst1 _ _ _ COPY_si) by auto. auto. } rewrite (proj1 (proj2 PRE_si)) in H2. erewrite <- si_dst1 in H0, H1 |- * by eauto. rewrite guarded_pointwise_relation_spec in COPY_gprv. rewrite <- COPY_gprv by auto. rewrite PRE_consi by auto. apply guarded_pointwise_relation_weaken with (P2 := Union E PE1 PE1_root) in COPY_gpre. 2: { apply Included_Complement_Disjoint. apply Union_left_Disjoint; split. + eapply aux07; eauto; reflexivity. + eapply aux09; eauto; reflexivity. } rewrite guarded_pointwise_relation_spec in COPY_gpre. rewrite COPY_gpre by auto. pose proof pregraph_join_guarded_si _ _ _ _ COPY_pj. eapply guarded_si_weaken in H3; [| apply Included_refl |]. 2: { apply Included_Complement_Disjoint. destruct COPY_pj as [_ [? _]]. eapply Prop_join_Disjoint; eauto. } assert (evalid g1' (emap g2 e)). 1: { rewrite <- COPY_gpre by auto. apply (evalid_preserved PRE_bij); auto. } eapply guarded_si_dst1; eauto. + apply COPY_consi; auto. rewrite <- PRE_si in COPY_si. erewrite <- si_dst1 in H1; eauto. unfold PE0 in H. rewrite Intersection_spec in H; tauto. Qed.
imports: CertiGraph.lib.Coqlib CertiGraph.lib.Ensembles_ext CertiGraph.lib.EquivDec_ext CertiGraph.lib.relation_list CertiGraph.lib.Morphisms_ext CertiGraph.lib.List_ext CertiGraph.graph.graph_model CertiGraph.graph.path_lemmas CertiGraph.graph.graph_gen CertiGraph.graph.graph_relation CertiGraph.graph.subgraph2 CertiGraph.graph.graph_morphism