proposition: Lemma triple_vcopy1_edge_copy_list: forall (g g1 g2: Graph) g1' g2' root es es_done es_later (M: V -> Prop), vvalid g root -> ~ M root -> (forall e, In e es <-> out_edges g root e) -> NoDup es -> es = es_done ++ es_later -> (forall v : V, M v \/ ~ M v) -> vcopy1 root g g1 g1' -> edge_copy_list g root es_done M (g1, g1') (g2, g2') -> let PV := reachable_by g root (Complement _ M) in let PE := Intersection E (weak_edge_prop PV g) (evalid g) in let M0 := Union _ M (eq root) in let PV2 := reachable_by_through_set g (map (dst g) es_done) (Complement _ M0) in let PE2 := Intersection _ (weak_edge_prop PV2 g) (evalid g) in let PE2_root e := In e es_done in guarded_bij (Union _ PV2 (eq root)) (Union _ PE2 PE2_root) (vmap g2) (emap g2) g2 g2' /\ g ~=~ g2 /\ (forall e, Union _ PE2 PE2_root e -> Complement _ (Union _ PV2 (eq root)) (dst g2 e) -> vvalid g (dst g2 e) -> vmap g2 (dst g2 e) = dst g2' (emap g2 e)) /\ guarded_pointwise_relation (Complement V PV) eq (vmap g) (vmap g2) /\ guarded_pointwise_relation (Complement E PE) eq (emap g) (emap g2) /\ Same_set (vvalid g2') (image_set (Union _ PV2 (eq root)) (vmap g2)) /\ Same_set (evalid g2') (image_set (Union _ PE2 PE2_root) (emap g2)).
proof: Proof. intros. assert (let PV1 := reachable_by_through_set g (map (dst g) nil) (Complement _ M0) in let PE1 := Intersection _ (weak_edge_prop PV1 g) (evalid g) in let PE1_root e := In e nil in guarded_bij (Union _ PV1 (eq root)) (Union _ PE1 PE1_root) (vmap g1) (emap g1) g1 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)) /\ guarded_pointwise_relation (Complement V PV) eq (vmap g) (vmap g1) /\ guarded_pointwise_relation (Complement E PE) eq (emap g) (emap 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))). 1: { pose proof triple_vcopy1 _ _ _ _ H H5. intros. assert (Same_set PV1 (Empty_set _)). 1: { rewrite Same_set_spec; intro v. split; [intros [? [? ?]] | intros []]. inv H8. } assert (Same_set PE1 (Empty_set _)). 1: { rewrite Same_set_spec; intro v. split; [intro | intros []]. unfold PE1 in H9; rewrite Intersection_spec in H9. destruct H9 as [[? [? ?]] ?]. inv H9. } assert (Same_set PE1_root (Empty_set _)). 1: { rewrite Same_set_spec; intro v. split; [intros [] | intros []]. } split; [| split; [| split; [| split; [| split]]]]. + rewrite H8, H9, H10. rewrite !Union_Empty_left. auto. + destruct H5; auto. + intros. rewrite Union_spec, (H9 e), (H10 e) in H11. inversion H11 as [[] | []]. + destruct H5 as [_ [? _]]. eapply guarded_pointwise_relation_weaken; [| exact H5]. apply Complement_Included_rev. unfold Included, Ensembles.In; intros. subst x; unfold PV. apply reachable_by_refl; auto. + destruct H5 as [_ [_ [? _]]]. eapply guarded_pointwise_relation_weaken; [| exact H5]. apply Complement_Included_rev. unfold Included, Ensembles.In; intros. unfold PE; rewrite Intersection_spec in H11 |- *. split; [destruct H11 as [? _] | tauto]. unfold weak_edge_prop in H11 |- *. rewrite <- H11. apply reachable_by_refl; auto. + destruct H5 as [_ [_ [_ ?]]]; subst g1'. split. - rewrite H8, Union_Empty_left, image_single. reflexivity. - rewrite H9, H10, Union_Empty_left, image_Empty. simpl. rewrite Same_set_spec; intro e. tauto. } clear H5. revert g2 g2' es_later H3 H6; rev_induction es_done; intros. + unfold edge_copy_list, relation_list in H6. simpl in H6. inversion H6; subst g2 g2'. auto. + clear H7. rewrite <- app_assoc in H5. unfold edge_copy_list in H6. rewrite combine_prefixes_app_1, map_app in H6; simpl in H6. apply (proj1 ((proj1 (same_relation_spec _ _) (relation_list_tail _ _)) _ _)) in H6. rename g2 into g3, g2' into g3'. apply compond_relation_spec in H6; destruct H6 as [[g2 g2'] [? ?]]. eapply triple_loop; [auto | auto | eauto | auto | eauto | auto | ..]. 1: eapply H3; eauto. 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