proposition: Lemma lcv_semi_iso: forall (from to: nat) (g g1: LGraph) l1 v, from <> to -> sound_gc_graph g -> sound_gc_graph g1 -> graph_has_gen g1 to -> vvalid g1 v -> vgeneration v = from -> raw_mark (vlabel g1 v) = false -> no_dangling_dst g -> gc_graph_semi_iso g g1 from to l1 -> gc_graph_semi_iso g (lgraph_copy_v g1 v to) from to ((v, new_copied_v g1 to) :: l1).
proof: Proof. intros from to g g1 l1 v H H0 H1 H3 H4 H5 H6 H7 H8. assert (sound_gc_graph (lgraph_copy_v g1 v to)) by (apply lcv_sound; auto). assert (N4: DoubleNoDup l1) by (eapply semi_iso_DoubleNoDup; eauto). destruct H8 as [? [? ?]]. destruct (split l1) as [from_l to_l] eqn: ?. destruct H10 as [[? ?] [[? [? ?]] ?]]. destruct H0 as [? [? [? Hels]]]. red in H0, H16, H17. pose proof H1. rename H18 into N1. destruct H1 as [? [? [? Hels1]]]. red in H1, H18, H19. assert (vvalid g v). { destruct (vvalid_lcm g v H0); auto. exfalso. assert (In v to_l) by (rewrite H13; now split). apply H14 in H21. now rewrite H5 in H21. } assert (~ vvalid g1 (new_copied_v g1 to)). { intro. rewrite H1 in H21. now apply (graph_has_v_not_eq g1 to) in H21. } assert (~ In v from_l) by (intro; rewrite <- H11 in H22; destruct H22; now rewrite H6 in H22). assert (N2: vlabel g v = vlabel g1 v) by now apply H15. assert (N3: ~ In (new_copied_v g1 to) to_l) by (intro; apply H13 in H23; now destruct H23). assert (N5: DoubleNoDup ((v, new_copied_v g1 to) :: l1)). { rewrite DoubleNoDup_cons_iff. split; [|split; [|split]]; auto. - intro. unfold new_copied_v in H23. destruct v. inversion H23; subst. now simpl in *. - intro. red in H23. rewrite Heqp, in_app_iff in H23. destruct H23; [easy|]. apply H14 in H23. now rewrite H5 in H23. - intro. red in H23. rewrite Heqp, in_app_iff in H23. destruct H23; [|easy]. unfold new_copied_v in H23. rewrite <- H11 in H23. destruct H23 as [_ [_ ?]]. symmetry in H23. now simpl in H23. } split3. - apply is_partial_graph_trans with g1; auto. simpl. apply pcv_is_partial_graph; auto. - intros. simpl in H23. destruct H23. + inversion H23. subst v1 v2. split3. * simpl. now rewrite ucov_copied_vertex. * rewrite lcv_vlabel_new; [easy | now rewrite H5]. * intros. simpl. rewrite pcv_dst_new. 2: erewrite <- vlabel_get_edges_snd; eauto. assert (evalid g (v, idx)). { rewrite H16. split; simpl; [now rewrite <- H0 | now rewrite get_edges_In]. } destruct H8 as [_ [_ [_ ?]]]. left. symmetry. apply H8; auto. rewrite H0. red in H7. apply (H7 v); [now rewrite <- H0 | now rewrite get_edges_In]. + assert (In v1 from_l) by (apply In_map_fst in H23; now rewrite map_fst_split, Heqp in H23). assert (In v2 to_l) by (apply In_map_snd in H23; now rewrite map_snd_split, Heqp in H23). assert (v2 <> new_copied_v g1 to) by (intro HS; now rewrite <- HS in N3). split3. * simpl. rewrite ucov_not_eq. 2: intro; now subst. rewrite lacv_vlabel_old. 1: apply (proj1 (H9 _ _ H23)). unfold new_copied_v. rewrite <- H11 in H24. destruct H24 as [_ [_ ?]]. destruct v1. simpl in *. intro HS; inversion HS. now rewrite H24 in H28. * simpl. rewrite ucov_not_eq. -- rewrite lacv_vlabel_old; auto. apply H9 in H23. now destruct H23 as [_ [? _]]. -- apply H14 in H25. intro. destruct v, v2. inversion H27; subst. now simpl in *. * intros. simpl. rewrite pcv_dst_old; auto. apply H9 in H23. destruct H23 as [_ [_ ?]]. specialize (H23 _ H27). destruct H23; [now left |]. destruct (InEither_dec (dst g (v1, idx)) l1). -- rewrite list_bi_map_cons_1. 1: now right. eapply DoubleNoDup_cons_InEither; eauto. -- rewrite list_bi_map_not_In in H23; [now left | easy]. - red in N5. simpl in *. rewrite Heqp in N5 |-* . pose proof (NoDup_app_l _ _ _ N5). pose proof (NoDup_app_r _ _ _ N5). split3. + split; auto. intros. split; intros. * destruct H25 as [? [? ?]]. destruct_eq_dec v0 v. 1: now left. rewrite <- lcv_raw_mark in H25; auto. -- right. rewrite <- H11. intuition. -- rewrite <- H1. destruct H8. now apply H8. * destruct_eq_dec v0 v. -- subst. split; [|intuition]. apply lcv_raw_mark_old. -- simpl in H25. destruct H25. 1: intuition auto with *. rewrite <- lcv_raw_mark; auto; rewrite <- H11 in H25; auto. destruct H25 as [_ [? _]]. rewrite <- H1. destruct H8. now apply H8. + split; auto. split. * intros. destruct H2. red in H2. rewrite H2. rewrite lcv_graph_has_v_iff; auto. rewrite <- H1. simpl. rewrite H13. intuition. rewrite H29 in H21. apply H21. destruct H8. now apply H8. * intros. unfold new_copied_v in H25. simpl in H25. destruct H25; [subst v0; now simpl | now apply H14]. + intros. simpl in H26. apply Decidable.not_or in H26. destruct H26. rewrite ucov_not_eq; auto. rewrite lacv_vlabel_old. 1: now apply H15. intro. rewrite <- H28 in H21. apply H21. destruct H8. now apply H8. 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