proposition: Lemma lcv_graph_thread_info_compatible: forall g h v to (Hi : 0 <= Z.of_nat to < Zlength (spaces h)) (Hh : has_space (Znth (Z.of_nat to) (spaces h)) (vertex_size g v)), graph_has_gen g to -> graph_heap_compatible g h -> graph_heap_compatible (lgraph_copy_v g v to) (cut_heap h (Z.of_nat to) (vertex_size g v) Hi Hh).
proof: Proof. unfold graph_heap_compatible. intros. destruct H0 as [? [? ?]]. assert (map space_start (spaces h) = map space_start (upd_Znth (Z.of_nat to) (spaces h) (cut_space (Znth (Z.of_nat to) (spaces h)) (vertex_size g v) Hh))). { rewrite <- upd_Znth_map. simpl. rewrite <- Znth_map by assumption. rewrite upd_Znth_unchanged; [reflexivity | rewrite Zlength_map; assumption]. } split; [|split]; [|simpl; rewrite cvmgil_length by assumption..]. - rewrite gsc_iff in *; simpl. 2: assumption. + intros. unfold nth_space. simpl. rewrite <- lcv_graph_has_gen in H4 by assumption. specialize (H0 _ H4). simpl in H0. destruct H0 as [? [? ?]]. split; [|split]. * clear -H0 H3 H. rewrite <- map_nth, <- H3, map_nth. clear H3. unfold nth_gen, nth_space in *. simpl. destruct (Nat.eq_dec gen to). -- subst gen. rewrite cvmgil_eq; simpl; assumption. -- rewrite cvmgil_not_eq; assumption. * assert (map space_sh (upd_Znth (Z.of_nat to) (spaces h) (cut_space (Znth (Z.of_nat to) (spaces h)) (vertex_size g v) Hh)) = map space_sh (spaces h)). { rewrite <- upd_Znth_map. simpl. rewrite <- Znth_map by assumption. rewrite upd_Znth_unchanged; [reflexivity|rewrite Zlength_map; assumption]. } rewrite <- map_nth, H7, map_nth. clear -H5 H. unfold nth_gen, nth_space in *. simpl. destruct (Nat.eq_dec gen to). -- subst gen. rewrite cvmgil_eq; simpl; assumption. -- rewrite cvmgil_not_eq; assumption. * assert (0 <= Z.of_nat gen < Zlength (spaces h)). { split. 1: apply Nat2Z.is_nonneg. rewrite Zlength_correct. apply inj_lt. red in H4. lia. } rewrite <- (Nat2Z.id gen) at 3. rewrite nth_Znth. 2: rewrite upd_Znth_Zlength; assumption. destruct (Nat.eq_dec gen to). -- subst gen. rewrite upd_Znth_same by assumption. simpl. rewrite lcv_pvs_same by assumption. rewrite H6, nth_space_Znth. reflexivity. -- assert (Z.of_nat gen <> Z.of_nat to) by (intro; apply n, Nat2Z.inj; assumption). rewrite upd_Znth_diff, <- nth_space_Znth, lcv_pvs_old; assumption. + rewrite cvmgil_length, <- !ZtoNat_Zlength, upd_Znth_Zlength, !ZtoNat_Zlength; assumption. - intros. rewrite <- H3. assumption. - rewrite <- !ZtoNat_Zlength, upd_Znth_Zlength, !ZtoNat_Zlength; assumption. Qed.
imports: Coq.ZArith.ZArith Coq.Program.Basics Coq.micromega.Lia 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 VST.zlist.list_solver CertiGraph.lib.EquivDec_ext CertiGraph.lib.List_ext CertiGraph.graph.graph_model CertiGraph.graph.graph_gen