proposition: Lemma fr_O_semi_iso: forall (from to : nat) (p : forward_p_type) (g g1 g2 : LGraph) (roots : roots_t) l1, from <> to -> sound_gc_graph g -> sound_gc_graph g1 -> graph_has_gen g1 to -> roots_graph_compatible roots g1 -> gc_graph_semi_iso g g1 from to l1 -> forward_p_compatible p roots g1 from -> no_dangling_dst g -> no_dangling_dst g1 -> special_edge_cond g p -> special_roots_cond p roots from -> forward_relation from to O (forward_p2forward_t p roots g1) g1 g2 -> exists l2, gc_graph_semi_iso g g2 from to (l2 ++ l1) /\ upd_roots from to p g1 roots = semi_roots_map l1 (l2 ++ l1) p roots /\ semi_rf_list_relation roots (l2 ++ l1) p from.
proof: Proof. pose (H2:=True). intros from to p g g1 g2 roots l1 H Hs H0 H1 Hg H3 H4 H7 Hd Hp Hr H5. assert (DoubleNoDup l1) by (eapply semi_iso_DoubleNoDup; eauto). assert (bijective (roots_map l1) (roots_map l1)) by (now apply roots_map_bijective). destruct p; simpl in H4, H5. - destruct (Znth z roots) eqn:? ; [destruct s|]; simpl in *; rewrite Heqr; inversion H5; subst; [exists []; simpl..|]. + split; [|split; [rewrite rrm_non_vertex_id|]]; auto. rewrite <- Heqr; apply upd_Znth_unchanged'. intros; now rewrite Heqr. eapply inl_rf_list_relation; eauto. + split; [|split; [rewrite rrm_non_vertex_id|]]; auto. rewrite <- Heqr; apply upd_Znth_unchanged'. intros; now rewrite Heqr. eapply inl_rf_list_relation; eauto. + split; [|split; [rewrite if_false|]]; auto. * erewrite rrm_not_in_id; eauto. rewrite <- Heqr; apply upd_Znth_unchanged'. simpl. intro. destruct H3 as [_ [_ ?]]. rewrite map_fst_split in H9. destruct (split l1). simpl in H9. destruct H3 as [[_ ?] _]. rewrite <- H3 in H9. now destruct H9 as [_ [_ ?]]. * eapply not_rf_list_relation; eauto. + split; [|rewrite if_true, H12]; auto. destruct H3 as [_ [? ?]]. destruct (split l1) eqn:? . destruct H9 as [[? ?] [[_ [? ?]] _]]. assert (In v (map fst l1)). { rewrite map_fst_split, Heqp, <- H10. do 2 (split; auto). destruct (vvalid_lcm g v (proj1 Hs)); trivial. red in Hg. rewrite Forall_forall in Hg. assert (graph_has_v g2 v). { apply Hg; rewrite <- filter_sum_right_In_iff, <- Heqr; now apply Znth_In. } destruct H0 as [? _]. red in H0. rewrite <- H0 in H15. assert (In v l0) by now rewrite H11. exfalso. now apply H13 in H16. } split. * erewrite rmm_eq_upd_bunch; eauto. 2: rewrite map_fst_split, Heqp; now simpl. rewrite In_map_fst_iff in H14. destruct H14 as [b ?]. destruct (H3 _ _ H14) as [? _]. now subst b. * red. intros. congruence. + unfold upd_root. rewrite if_true, H11; auto. exists [(v, (new_copied_v g1 to))]. simpl. split3. * apply lcv_semi_iso; auto. red in Hg. rewrite Forall_forall in Hg. destruct H0. red in H0. rewrite H0. apply Hg. rewrite <- filter_sum_right_In_iff, <- Heqr. now apply Znth_In. * erewrite rmm_eq_upd_bunch; eauto. 1: now left. simpl. destruct H3 as [_ [_ ?]]. destruct (split l1) as [from_l to_l] eqn: ?. destruct H3 as [[? ?] _]. rewrite map_fst_split, Heqp. simpl. constructor. 2: easy. intro. rewrite <- H9 in H10. destruct H10. now rewrite H11 in H10. * red. intros. simpl. left. congruence. - destruct p as [v n]. destruct H4 as [? [? [? [H10' H11]]]]. rewrite H10 in H5. simpl in *. destruct (Znth n (make_fields g1 v)) eqn:? ; [destruct s|]; simpl in H5; inversion H5; subst; try (exists []; split; [easy | now rewrite (surjective _ _ H8)]). + exists []. split; [| now rewrite (surjective _ _ H8)]. eapply lgd_semi_iso; eauto. simpl. intuition. + exists [(dst g1 e, new_copied_v g1 to)]. simpl. assert (Hm: gc_graph_semi_iso g (lgraph_copy_v g1 (dst g1 e) to) (vgeneration (dst g1 e)) to ((dst g1 e, new_copied_v g1 to) :: l1)). { apply lcv_semi_iso; auto. red in Hd. destruct H0. red in H0. rewrite H0. apply (Hd v); auto. unfold get_edges. rewrite <- filter_sum_right_In_iff. rewrite <- Heqf. apply Znth_In. now rewrite make_fields_eq_length. } split. * cut (gc_graph_semi_iso g (lgraph_copy_v g1 (dst g1 e) to) (vgeneration (dst g1 e)) to ((dst g1 e, new_copied_v g1 to) :: l1)). 2: assumption. intros. assert (Hfn: fst e <> new_copied_v g1 to). { apply make_fields_Znth_edge in Heqf; auto. subst e. simpl. destruct v as [gen idx]. red in H4. simpl in H4. destruct H4. red in H13. intro. unfold new_copied_v in H15. inversion H15. subst gen idx. lia. } eapply (lgd_semi_iso _ _ _ _ _ v n e) in H12; eauto. -- subst new_g. simpl dst in H12. rewrite pcv_dst_old in H12; auto. simpl in H12. rewrite ucov_copied_vertex in H12. easy. -- now apply lcv_sound. -- now rewrite <- lcv_graph_has_gen. -- Opaque lgraph_copy_v. simpl. Transparent lgraph_copy_v. split; [|split; [|split3]]; auto. ++ rewrite lcv_graph_has_v_iff; auto. ++ rewrite <- lcv_raw_fields; auto. ++ rewrite <- lcv_raw_mark; auto. intro. now subst v. ++ rewrite <- lcv_raw_tag; auto. intro. now subst v. -- simpl. rewrite pcv_dst_old; auto. -- unfold lgraph_copy_v. rewrite lmc_make_fields, lacv_make_fields_not_eq. 1: easy. apply make_fields_Znth_edge in Heqf; auto. now subst e. -- simpl dst. rewrite pcv_dst_old; auto. apply lcv_raw_mark_old. * apply semi_iso_DoubleNoDup in Hm; auto. rewrite roots_map_map_cons; auto. rewrite (surjective _ _ H8), roots_map_the_same; auto. intros. red in Hr. specialize (Hr _ H12). intro. red in H13. simpl in H13. destruct H13 as [? | [? | ?]]; auto. -- now rewrite H13 in Hr. -- red in Hg. rewrite Forall_forall in Hg. rewrite filter_sum_right_In_iff in H12. apply Hg in H12. rewrite <- H13 in H12. unfold new_copied_v in H12. destruct H12. simpl in H15. red in H15. lia. Qed.
imports: Coq.ZArith.ZArith Coq.Program.Basics compcert.lib.Integers compcert.common.Values VST.veric.base VST.veric.Clight_lemmas VST.veric.val_lemmas VST.veric.shares VST.msl.seplog VST.msl.shares VST.zlist.sublist VST.floyd.coqlib3 VST.floyd.functional_base VST.floyd.data_at_rec_lemmas CertiGraph.lib.Coqlib CertiGraph.lib.EquivDec_ext CertiGraph.lib.List_ext CertiGraph.graph.graph_model CertiGraph.graph.graph_gen CertiGraph.graph.path_lemmas CertiGraph.graph.subgraph2 CertiGraph.graph.graph_relation CertiGraph.graph.graph_isomorphism CertiGraph.graph.reachable_ind CertiGraph.CertiGC.GCGraph