proposition: Lemma triple3_ecopy1: forall (g g2 g3: Graph) (g2' g3': Graph') (M: V -> Prop) root es es_done e0 es_later, let M0 := Union _ M (eq root) 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 PE3_root e := In e (es_done ++ e0 :: nil) in vvalid g root -> ~ M root -> (forall e, In e es <-> out_edges g root e) -> NoDup es -> es = es_done ++ e0 :: es_later -> guarded_bij (Union _ PV3 (eq root)) (Union _ PE3 PE1_root) (vmap g2) (emap g2) g2 g2' /\ g ~=~ g2 /\ (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)) -> ecopy1 e0 (g2, g2') (g3, g3') -> (forall e, (Union _ PE3 PE3_root) e -> Complement _ (Union _ PV3 (eq root)) (dst g3 e) -> vvalid g (dst g3 e) -> vmap g3 (dst g3 e) = dst g3' (emap g3 e)).
proof: Proof. intros until es_later. intros ? ? ? ? ?. intros H_VVALID H_M H_OUT_EDGES H_NODUP H_ES [PRE_bij [PRE_si PRE_consi]] ECOPY. destruct ECOPY as [ECOPY_si [ECOPY_prv [ECOPY_gpre [ECOPY_pj [? ?]]]]]. intros ? ? ? H_EXTRA. erewrite app_same_set in H1 by (eapply (aux20 e0 PE1_root PE3 PE3_root); eauto; reflexivity). rewrite Union_spec in H1; destruct H1. + assert (evalid g e). 1: { rewrite Union_spec in H1; destruct H1; [eapply aux23 | eapply aux22]; eauto; reflexivity. } assert (vvalid g (dst g2 e)) as H_EXTRA'. 1: { rewrite (proj1 (proj2 PRE_si)) in H3. rewrite (si_dst1 _ _ _ ECOPY_si) by auto. auto. } rewrite (proj1 (proj2 PRE_si)) in H3. erewrite <- si_dst1 in H2 |- * by eauto. rewrite <- ECOPY_prv. apply guarded_pointwise_relation_weaken with (P2 := Union E PE3 PE1_root) in ECOPY_gpre. 2: { apply Included_Complement_Disjoint. apply Union_left_Disjoint; split; [eapply aux10 | eapply aux11]; eauto; reflexivity. } rewrite guarded_pointwise_relation_spec in ECOPY_gpre. rewrite <- ECOPY_gpre by auto. rewrite PRE_consi by auto. pose proof pregraph_join_guarded_si _ _ _ _ ECOPY_pj. eapply guarded_si_weaken in H4; [| apply Included_refl |]. 2: { apply Included_Complement_Disjoint. destruct ECOPY_pj as [_ [? _]]. eapply Prop_join_Disjoint; eauto. } assert (evalid g2' (emap g2 e)) by (apply (evalid_preserved PRE_bij); auto). eapply guarded_si_dst1; eauto. + subst e. apply H0. rewrite <- (proj1 PRE_si); auto. 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