proposition: Lemma guarded_bij_disjointed_union_strong: forall PV1 PE1 PV2 PE2 vmap emap (G: PreGraph V E) (G1' G2': PreGraph V' E'), disjointed_guard (image_set PV1 vmap) (image_set PV2 vmap) (image_set PE1 emap) (image_set PE2 emap) -> guarded_bij PV1 PE1 vmap emap G G1' -> guarded_bij PV2 PE2 vmap emap G G2' -> boundary_edge_consistent PE1 PV2 vmap emap G G1' -> boundary_edge_consistent PE2 PV1 vmap emap G G2' -> exists G', guarded_bij (Union _ PV1 PV2) (Union _ PE1 PE2) vmap emap G G' /\ guarded_structurally_identical (image_set PV1 vmap) (image_set PE1 emap) G1' G' /\ guarded_structurally_identical (image_set PV2 vmap) (image_set PE2 emap) G2' G'.
proof: Proof. intros. destruct (vmap_inj H0) as [vg1 ?]. destruct (vmap_inj H1) as [vg2 ?]. destruct (emap_inj H0) as [eg1 ?]. destruct (emap_inj H1) as [eg2 ?]. set (vg := fun v' => match vg1 v' with Some v => Some v | _ => vg2 v' end). set (eg := fun e' => match eg1 e' with Some e => Some e | _ => eg2 e' end). exists (@Build_PreGraph V' E' _ _ (fun v' => match vg1 v' with Some _ => vvalid G1' v' | _ => vvalid G2' v' end) (fun e' => match eg1 e' with Some _ => evalid G1' e' | _ => evalid G2' e' end) (fun e' => match eg1 e' with Some _ => src G1' e' | _ => src G2' e' end) (fun e' => match eg1 e' with Some _ => dst G1' e' | _ => dst G2' e' end)). split; [| split]. + split; [.. | split]. - eapply is_guarded_inj_disjoint_union. * apply Disjoint_Union_Prop_join. clear - H; destruct H. apply image_Disjoint_rev in H; auto. * apply (vmap_inj H0). * apply (vmap_inj H1). * clear - H; destruct H. rewrite Disjoint_spec in H. intros. pose proof (H (vmap a1)). intro. rewrite !image_set_spec in H3. spec H3; [exists a1; auto |]. spec H3; [exists a2; auto |]. auto. - eapply is_guarded_inj_disjoint_union. * apply Disjoint_Union_Prop_join. clear - H; destruct H. apply image_Disjoint_rev in H0; auto. * apply (emap_inj H0). * apply (emap_inj H1). * clear - H; destruct H. rewrite Disjoint_spec in H0. intros. pose proof (H0 (emap a1)). intro. rewrite !image_set_spec in H3. spec H3; [exists a1; auto |]. spec H3; [exists a2; auto |]. auto. - simpl; intros. rewrite Union_spec in H8; destruct H8. * rewrite (is_guarded_inj_rev_aux PV1 vmap vg1) by auto. apply (vvalid_preserved H0); auto. * destruct H. rewrite (is_guarded_inj_rev_aux' PV1 PV2 vmap vg1) by auto. apply (vvalid_preserved H1); auto. - simpl; intros. rewrite Union_spec in H8; destruct H8. * rewrite (is_guarded_inj_rev_aux PE1 emap eg1) by auto. apply (evalid_preserved H0); auto. * destruct H. rewrite (is_guarded_inj_rev_aux' PE1 PE2 emap eg1) by auto. apply (evalid_preserved H1); auto. - simpl; intros. rewrite Union_spec in H8, H9. destruct H8, H9. * rewrite (is_guarded_inj_rev_aux PE1 emap eg1) by auto. apply (src_preserved H0); auto. * rewrite (is_guarded_inj_rev_aux PE1 emap eg1) by auto. apply (proj1 H2); auto. * rewrite (is_guarded_inj_rev_aux' PE1 PE2 emap eg1) by (destruct H; auto). apply (proj1 H3); auto. * rewrite (is_guarded_inj_rev_aux' PE1 PE2 emap eg1) by (destruct H; auto). apply (src_preserved H1); auto. - simpl; intros. rewrite Union_spec in H8, H9. destruct H8, H9. * rewrite (is_guarded_inj_rev_aux PE1 emap eg1) by auto. apply (dst_preserved H0); auto. * rewrite (is_guarded_inj_rev_aux PE1 emap eg1) by auto. apply (proj2 H2); auto. * rewrite (is_guarded_inj_rev_aux' PE1 PE2 emap eg1) by (destruct H; auto). apply (proj2 H3); auto. * rewrite (is_guarded_inj_rev_aux' PE1 PE2 emap eg1) by (destruct H; auto). apply (dst_preserved H1); auto. + rewrite guarded_si_spec; simpl. split; [| split; [| split]]. - intros v' ?. rewrite image_set_spec in H8; destruct H8 as [v [? ?]]; subst v'. rewrite (is_guarded_inj_rev_aux PV1 vmap vg1) by auto. tauto. - intros e' ?. rewrite image_set_spec in H8; destruct H8 as [e [? ?]]; subst e'. rewrite (is_guarded_inj_rev_aux PE1 emap eg1) by auto. tauto. - intros e' ? ? ?. rewrite image_set_spec in H8; destruct H8 as [e [? ?]]; subst e'. rewrite (is_guarded_inj_rev_aux PE1 emap eg1) in H10 |- * by auto. auto. - intros e' ? ? ?. rewrite image_set_spec in H8; destruct H8 as [e [? ?]]; subst e'. rewrite (is_guarded_inj_rev_aux PE1 emap eg1) in H10 |- * by auto. auto. + rewrite guarded_si_spec; simpl. split; [| split; [| split]]. - intros v' ?. rewrite image_set_spec in H8; destruct H8 as [v [? ?]]; subst v'. rewrite (is_guarded_inj_rev_aux' PV1 PV2 vmap vg1) by (destruct H; auto). tauto. - intros e' ?. rewrite image_set_spec in H8; destruct H8 as [e [? ?]]; subst e'. rewrite (is_guarded_inj_rev_aux' PE1 PE2 emap eg1) by (destruct H; auto). tauto. - intros e' ? ? ?. rewrite image_set_spec in H8; destruct H8 as [e [? ?]]; subst e'. rewrite (is_guarded_inj_rev_aux' PE1 PE2 emap eg1) by (destruct H; auto). auto. - intros e' ? ? ?. rewrite image_set_spec in H8; destruct H8 as [e [? ?]]; subst e'. rewrite (is_guarded_inj_rev_aux' PE1 PE2 emap eg1) by (destruct H; auto). 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.reachable_ind CertiGraph.graph.subgraph2 CertiGraph.graph.graph_gen CertiGraph.graph.graph_relation