proposition: Lemma triple_final: forall (g g1: Graph) (g1': Graph') (M: V -> Prop) root es, let PV := reachable_by g root (Complement _ M) in let PE := Intersection E (weak_edge_prop PV g) (evalid g) in vvalid g root -> ~ M root -> let M0 := Union _ M (eq root) in (forall e, In e es <-> out_edges g root e) -> NoDup es -> let PV1 := reachable_by_through_set g (map (dst g) es) (Complement _ M0) in let PE1 := Intersection _ (weak_edge_prop PV1 g) (evalid g) in let PE1_root e := In e es 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)) -> copy M root g g1 g1'.
proof: Proof. intros. assert (step_list g root (map (dst g) es)). 1: { intro x. rewrite in_map_iff. split. + intros [e [? ?]]. rewrite H1 in H5. destruct H5. exists e; auto. + intros. destruct H4 as [e ? ?]. exists e. rewrite H1. unfold out_edges; auto. } destruct H3 as [?PRE [?PRE [?PRE [?PRE [?PRE ?PRE]]]]]. assert (Same_set (reachable_by g root (Complement _ M)) (Union _ PV1 (eq root))). 1: { rewrite Same_set_spec. intro v. erewrite reachable_by_ind_equiv by eauto. rewrite Union_spec, Intersection_Complement. tauto. } assert (Same_set (Intersection E (weak_edge_prop (reachable_by g root (Complement _ M)) g) (evalid g)) (Union _ PE1 PE1_root)). 1: { rewrite Same_set_spec. intro e. rewrite Intersection_spec; unfold weak_edge_prop. erewrite reachable_by_ind_equiv by eauto. unfold PE1. rewrite Union_spec, Intersection_spec, Intersection_Complement. unfold weak_edge_prop, PV1, M0, PE1_root. rewrite H1. unfold out_edges. assert (root = src g e <-> src g e = root) by (split; intro; congruence). tauto. } unfold copy. split; [| split; [| split; [| split; [| split; [| split]]]]]. + auto. + auto. + auto. + rewrite H3. tauto. + rewrite H5. tauto. + hnf; intros. rewrite (H5 e) in H6. rewrite Intersection_spec in H7; destruct H7. apply PRE1; auto. generalize (dst g1 e), H7. apply Complement_Included_rev. rewrite <- H3. apply Included_refl. + rewrite H5, H3. 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