proposition: Lemma svfl_semi_iso: forall from to v l l1 g1 g2 g3 roots, from <> to -> sound_gc_graph g1 -> sound_gc_graph g2 -> graph_has_gen g2 to -> roots_graph_compatible roots g2 -> no_dangling_dst g1 -> no_dangling_dst g2 -> roots_have_no_gen roots from -> (forall i : nat, In i l -> (i < length (raw_fields (vlabel g2 v)))%nat) -> ~ vvalid g1 v -> vvalid g2 v -> raw_mark (vlabel g2 v) = false -> raw_tag (vlabel g2 v) < NO_SCAN_TAG -> vgeneration v <> from -> copy_compatible g2 -> gc_graph_semi_iso g1 g2 from to l1 -> scan_vertex_for_loop from to v l g2 g3 -> exists l2, gc_graph_semi_iso g1 g3 from to (l2 ++ l1) /\ roots = roots_map (l2 ++ l1) (roots_map l1 roots).
proof: Proof. pose (H3:=True). do 3 intro. induction l; intros ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? NOSCAN; intros; inversion H15; subst; clear H15. - exists []. simpl. split; auto. symmetry. apply surjective, roots_map_bijective. eapply (semi_iso_DoubleNoDup _ _ from); eauto. - pose proof H18. change (forward_p2forward_t (inr (v, Z.of_nat a)) [] g2) with (forward_p2forward_t (inr (v, Z.of_nat a)) roots g2) in H18. assert (forward_p_compatible (inr (v, Z.of_nat a)) roots g2 from). { simpl. destruct H1. red in H1. rewrite <- H1. intuition auto with *. rewrite Zlength_correct. apply inj_lt, H8. now left. } eapply (fr_O_semi_iso _ _ _ g1) in H18; eauto. destruct H18 as [l3 [? [? _]]]. simpl in H18. assert (sound_gc_graph g4) by (eapply fr_O_sound; eauto). assert (graph_has_v g2 v) by (destruct H1; red in H1; now rewrite <- H1). eapply (IHl (l3 ++ l1) g1) in H21; eauto. + destruct H21 as [l2 [? ?]]. exists (l2 ++ l3). rewrite <- app_assoc. split; auto. rewrite H22 at 1. f_equal. rewrite H18 at 1. apply surjective, roots_map_bijective. eapply (semi_iso_DoubleNoDup _ _ from); eauto. + erewrite <- fr_graph_has_gen; eauto. + eapply fr_right_roots_graph_compatible; eauto. + eapply fr_O_no_dangling_dst; eauto. + intros. erewrite <- fr_raw_fields; eauto. apply H8; now right. + destruct H19. red in H19. rewrite H19. eapply fr_graph_has_v; eauto. + erewrite <- fr_raw_mark; eauto. + erewrite <- fr_raw_tag; eauto. + eapply (fr_copy_compatible O from); 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