proposition: Lemma gc_cond_implies_do_gen_cons: forall g h i, safe_to_copy_to_except g i -> graph_has_gen g (S i) -> graph_heap_compatible g h -> garbage_collect_condition g h -> do_generation_condition g h i (S i).
proof: Proof. intros. destruct H2 as [? [? [? ?]]]. assert (graph_has_gen g i) by (unfold graph_has_gen in H0 |-*; lia). split; [|split; [|split; [|split; [|split; [|split ]]]]]; auto. - unfold safe_to_copy_to_except, safe_to_copy_gen in H. red. unfold rest_gen_size. specialize (H (S i)). simpl in H. destruct (gt_gs_compatible _ _ H1 _ H0) as [_ [_ ?]]. destruct (gt_gs_compatible _ _ H1 _ H6) as [_ [_ ?]]. fold (graph_gen_size g (S i)) in H7. fold (graph_gen_size g i) in H8. rewrite <- H7. fold (gen_size h (S i)). destruct (space_order (nth_space h i)) as [_ ?]. fold (gen_size h i) in H9. rewrite <- H8 in H9. transitivity (gen_size h i). 1: assumption. rewrite (ti_size_gen _ _ _ H1 H6 H5), (ti_size_gen _ _ _ H1 H0 H5). apply H; [lia.. | assumption]. - apply graph_unmarked_copy_compatible; assumption. - rewrite (ti_size_gen _ _ _ H1 H0 H5). apply ngs_0_lt. - rewrite graph_gen_unmarked_iff in H2. apply H2. 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