proposition: Lemma graph_rep_add: forall (g : LGraph) (gi : generation_info), number_of_vertices gi = O -> copy_compatible g -> no_dangling_dst g -> graph_rep g = graph_rep (lgraph_add_new_gen g gi).
proof: Proof. intros. unfold graph_rep. simpl. rewrite app_length. simpl. rewrite Nat.add_1_r, nat_inc_list_S, iter_sepcon_app_sepcon. simpl. unfold generation_rep at 3. unfold nth_gen. simpl. rewrite app_nth2 by lia. replace (length (g_gen (glabel g)) - length (g_gen (glabel g)))%nat with O by lia. simpl. rewrite H. simpl. rewrite !sepcon_emp. apply iter_sepcon_func_strong. intros. rewrite nat_inc_list_In_iff in H2. unfold generation_rep. unfold nth_sh. rewrite !ang_nth_old by assumption. apply iter_sepcon_func_strong. intros v ?. rewrite in_map_iff in H3. destruct H3 as [idx [? ?]]. rewrite nat_inc_list_In_iff in H4. apply vertex_rep_add; auto. split; subst; simpl; assumption. 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