proposition: Lemma triple1_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 -> extended_copy M_rec (dst g e0) (g1, g1') (g2, g2') -> (forall v, M v \/ ~ M v) -> guarded_bij (Union _ PV3 (eq root)) (Union _ PE3 PE1_root) (vmap g2) (emap g2) g2 g2'.
proof: Proof. intros until es_later. intros ? ? ? ? ? ? ? ? ?. intros H_VVALID H_CM H_OUT_EDGES H_ES [PRE_bij [PRE_vvalid [PRE_evalid PRE_si]]] COPY M_DEC. erewrite (aux18 root PV1 PV3 PV0) by first [destruct COPY; tauto | reflexivity]. erewrite (aux19 PE1 PE1_root PE3 PE0) by first [destruct COPY; tauto | reflexivity]. 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_si. 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. apply guarded_pointwise_relation_weaken with (P2 := Union V PV1 (eq root)) in COPY_gprv. 2: { apply Included_Complement_Disjoint. apply Union_left_Disjoint. split; [eapply (aux06 PV1 PV0) | eapply (aux08 root PV0)]; first [eassumption | reflexivity]. } 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 PE1 PE0) | eapply (aux09 PE1_root PE0)]; first [eassumption | reflexivity]. } rewrite COPY_gprv in PRE_bij, PRE_vvalid. rewrite COPY_gpre in PRE_bij, PRE_evalid. assert (guarded_bij PV0 PE0 (vmap g2) (emap g2) g g2'). 1: { eapply guarded_bij_proper_aux1; [| reflexivity | exact COPY_bij]. apply si_guarded_si; symmetry; auto. } assert (guarded_bij (Union _ PV1 (eq root)) (Union _ PE1 PE1_root) (vmap g2) (emap g2) g2 g2'). 1: { eapply guarded_bij_proper_aux1; [| | exact PRE_bij]. 1: apply si_guarded_si; rewrite <- COPY_si; symmetry; auto. pose proof pregraph_join_guarded_si _ _ _ _ COPY_pj. eapply guarded_si_weaken; [| | exact H0]; clear H0. + apply Included_Complement_Disjoint. destruct COPY_pj as [? _]. apply Prop_join_Disjoint in H0. rewrite PRE_vvalid in H0; auto. + apply Included_Complement_Disjoint. destruct COPY_pj as [_ [? _]]. apply Prop_join_Disjoint in H0. rewrite PRE_evalid in H0; auto. } apply guarded_bij_disjointed_union; auto. + destruct COPY_pj as [? [? _]]. apply Prop_join_Disjoint in H1. apply Prop_join_Disjoint in H2. rewrite PRE_vvalid in H1. rewrite PRE_evalid in H2. split; auto. + split; split; hnf; intros. - erewrite <- si_src2 in H2 by eauto. rewrite Union_spec in H1; destruct H1; exfalso. * revert H1 H2; eapply aux12; reflexivity. * revert H1 H2; eapply aux15; eauto; reflexivity. - erewrite <- si_dst2 in H2 by eauto. rewrite Union_spec in H1; destruct H1; exfalso. * revert H1 H2; eapply aux13; eauto; reflexivity. * revert H1 H2; eapply aux16; eauto; reflexivity. - erewrite <- si_src2 in H2 by eauto. rewrite Union_spec in H2; destruct H2; exfalso. * revert H1 H2; eapply aux14; eauto; reflexivity. * revert H1 H2; eapply aux17; eauto; reflexivity. - apply COPY_consi; [auto | | eapply aux24; eauto]. erewrite <- si_dst2 in H2 by eauto. unfold not; generalize (dst g e) H2. rewrite <- Disjoint_spec. apply Union_left_Disjoint. split; [eapply (aux06 PV1 PV0) | eapply (aux08 root PV0)]; first [eassumption | reflexivity]. 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