proposition: Theorem garbage_collect_isomorphism: forall roots1 roots2 g1 g2, graph_unmarked g1 -> no_backward_edge g1 -> no_dangling_dst g1 -> roots_graph_compatible roots1 g1 -> sound_gc_graph g1 -> garbage_collect_relation roots1 roots2 g1 g2 -> gc_graph_iso g1 roots1 g2 roots2.
proof: Proof. pose (H2 := True). intros. destruct H5 as [n [? ?]]. clear H6. unfold nat_inc_list in H5. pose proof (graph_has_gen_O g1). assert (firstn_gen_clear g1 O) by (red; intros; lia). remember O as s. clear Heqs. remember (S n) as m. clear n Heqm. rename m into n. revert s g1 roots1 g2 roots2 H H0 H1 H2 H3 H4 H5 H6 H7. induction n; intros; simpl in *; inversion H5; subst; clear H5. 1: apply gc_graph_iso_refl. pose proof H11. assert (sound_gc_graph g3) by (eapply ngr_sound; eauto). assert (graph_has_gen g3 (S s)) by (eapply ngr_graph_has_gen; eauto). assert (graph_unmarked g3) by (eapply ngr_graph_unmarked; eauto). assert (roots_graph_compatible roots1 g3) by (eapply ngr_roots_graph_compatible; eauto). assert (no_dangling_dst g3) by (eapply ngr_no_dangling_dst; eauto). assert (no_edge2gen g3 s) by (eapply ngr_no_edge2gen; eauto; apply fgc_nbe_no_edge2gen; auto). apply do_gen_iso in H11; auto. apply (gc_graph_iso_trans g3 roots1). 1: eapply ngr_iso; eauto. apply (gc_graph_iso_trans g4 roots3); auto. assert (gen_unmarked g3 (S s)) by (rewrite graph_gen_unmarked_iff in H12; apply H12). assert (firstn_gen_clear g3 s) by (eapply ngr_firstn_gen_clear; eauto). assert (no_backward_edge g3) by (eapply ngr_no_backward_edge; eauto). assert (copy_compatible g3) by (apply graph_unmarked_copy_compatible; auto). assert (no_dangling_dst g4). { eapply do_gen_no_dangling_dst; eauto. } apply (IHn (S s)); auto. - eapply (do_gen_graph_unmarked s (S s)); eauto. - eapply do_gen_no_backward_edge; eauto. - eapply do_gen_roots_graph_compatible; eauto. - eapply do_gen_sound; eauto. - rewrite <- do_gen_graph_has_gen; eauto. - eapply do_gen_firstn_gen_clear; eauto. Qed.
imports: Coq.ZArith.ZArith Coq.Program.Basics 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 CertiGraph.lib.Coqlib CertiGraph.lib.EquivDec_ext CertiGraph.lib.List_ext CertiGraph.graph.graph_model CertiGraph.graph.graph_gen CertiGraph.graph.path_lemmas CertiGraph.graph.subgraph2 CertiGraph.graph.graph_relation CertiGraph.graph.graph_isomorphism CertiGraph.graph.reachable_ind CertiGraph.CertiGC.GCGraph