proposition: Lemma apply_derives: forall P Q, (weak_derives P Q && emp) * P |-- Q.
proof: Proof. intros. unseal_derives. intros ? (? & ? & ? & [Hderives Hemp] & HP). destruct (join_level _ _ _ H). Abort. Definition heap_rest_gen_data_at_ (g: LGraph) (h: heap) (gen: nat) := data_at_ (nth_sh g gen) (tarray int_or_ptr_type (total_space (nth_space h gen) - graph_gen_size g gen)) (offset_val (WORD_SIZE * graph_gen_size g gen) (gen_start g gen)). Lemma heap_rest_rep_iter_sepcon: forall g h, graph_heap_compatible g h -> heap_rest_rep h = iter_sepcon (nat_inc_list (length (g_gen (glabel g)))) (heap_rest_gen_data_at_ g h). Proof. intros. unfold heap_rest_rep. pose proof (gt_gs_compatible _ _ H). destruct H as [? [? ?]]. rewrite <- (firstn_skipn (length (g_gen (glabel g))) (spaces h)). rewrite iter_sepcon_app_sepcon. rewrite <- map_skipn in H1. remember (skipn (length (g_gen (glabel g))) (spaces h)). assert (iter_sepcon l space_rest_rep = emp). { clear Heql. induction l; simpl. 1: reflexivity. rewrite IHl by (simpl in H1; apply Forall_tl in H1; assumption). rewrite Forall_forall in H1. simpl in H1. unfold space_rest_rep. rewrite if_true. - rewrite emp_sepcon; reflexivity. - symmetry. apply H1. left; reflexivity. } rewrite H3. replace (firstn (length (g_gen (glabel g))) (spaces h)) with (map (nth_space h) (nat_inc_list (length (g_gen (glabel g))))). - rewrite <- iter_sepcon_map, sepcon_emp. apply iter_sepcon_func_strong. intros gen ?. unfold space_rest_rep, heap_rest_gen_data_at_. rewrite nat_inc_list_In_iff in H4. specialize (H0 _ H4). destruct H0 as [? [? ?]]. rewrite <- H0, if_false. + unfold gen_start. rewrite if_true. 2: assumption. rewrite <- H5, <- H6. f_equal. + pose proof (start_isptr (nth_gen g gen)). destruct (start_address (nth_gen g gen)); try contradiction. intro. inversion H8. - unfold nth_space. remember (spaces h) as ls. remember (length (g_gen (glabel g))) as m. clear -H2. revert ls H2. induction m; intros. 1: simpl; reflexivity. rewrite nat_inc_list_S, map_app. rewrite IHm by lia. simpl map. clear IHm. revert ls H2. induction m; intros. + destruct ls. 1: simpl in H2; exfalso; lia. simpl. reflexivity. + destruct ls. 1: simpl in H2; exfalso; lia. simpl firstn at 1. simpl nth. Opaque firstn. simpl. Transparent firstn. rewrite IHm by (simpl in H2; lia). simpl. destruct ls; reflexivity. Qed.
imports: VST.veric.compcert_rmaps VST.msl.shares VST.msl.wand_frame VST.concurrency.conclib CertiGraph.lib.List_ext CertiGraph.msl_ext.log_normalize CertiGraph.msl_ext.ramification_lemmas CertiGraph.graph.graph_model CertiGraph.CertiGC.GCGraph CertiGraph.CertiGC.env_graph_gc CertiGraph.msl_ext.iter_sepcon Coq.Lists.List