proposition: Lemma graph_heap_rest_iter_sepcon: forall g h, graph_heap_compatible g h -> graph_rep g * heap_rest_rep h |-- iter_sepcon (nat_inc_list (length (g_gen (glabel g)))) (generation_data_at_ g h).
proof: Proof. intros. unfold graph_rep. rewrite (heap_rest_rep_iter_sepcon _ _ H). assert (forall gen, In gen (nat_inc_list (length (g_gen (glabel g)))) -> graph_has_gen g gen) by (intros; rewrite nat_inc_list_In_iff in H0; assumption). remember (length (g_gen (glabel g))). clear Heqn. revert H0. induction n; intros. - simpl. rewrite emp_sepcon. apply derives_refl. - rewrite nat_inc_list_S. rewrite !iter_sepcon_app_sepcon. simpl. rewrite !sepcon_emp. pull_left (generation_rep g n). rewrite <- sepcon_assoc. rewrite (sepcon_assoc (generation_rep g n)). sep_apply IHn. + intros. apply H0. rewrite nat_inc_list_S, in_app_iff. left; assumption. + cancel. sep_apply (gr_hrgda_data_at_ g h n); auto. apply H0. rewrite nat_inc_list_S, in_app_iff. right. left. 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