proposition: Lemma svwl_semi_iso: forall from to l l1 roots g1 g2 g3, 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, In i l -> ~ gen_has_index g1 to i) -> copy_compatible g2 -> gen_unmarked g2 to -> gc_graph_semi_iso g1 g2 from to l1 -> scan_vertex_while_loop from to 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; inversion H12; subst. - exists []; simpl. split; auto. assert (bijective (roots_map l1) (roots_map l1)). { apply roots_map_bijective. eapply semi_iso_DoubleNoDup; eauto. } symmetry. now apply surjective. - eapply IHl; eauto. intros. apply H8. now right. - pose proof H17. eapply (svfl_semi_iso _ _ _ _ _ g1) in H17; eauto. + destruct H17 as [l3 [? ?]]. eapply (IHl (l3 ++ l1) _ g1) in H20; eauto. * destruct H20 as [l2 [? ?]]. exists (l2 ++ l3). rewrite <- app_assoc. split; auto. rewrite H19 at 1. f_equal. rewrite H17 at 1. apply surjective, roots_map_bijective. eapply semi_iso_DoubleNoDup; eauto. * eapply svfl_P_holds; eauto. apply fr_O_sound. * erewrite <- svfl_graph_has_gen; eauto. * red. rewrite Forall_forall. intros. eapply svfl_graph_has_v; eauto. red in H4. rewrite Forall_forall in H4. now apply H4. * eapply (svfl_no_dangling_dst from to); eauto. 1: split; now simpl. unfold no_scan in H16; lia. intros. now rewrite nat_inc_list_In_iff in H18. * intros. apply H8. now right. * eapply svfl_copy_compatible; eauto. * eapply svfl_gen_unmarked; eauto. + intros. now rewrite nat_inc_list_In_iff in H14. + destruct H0. red in H0. rewrite H0. intro. destruct H18. simpl in H19. apply (H8 a); [left |]; auto. + destruct H1. red in H1. rewrite H1. split; now simpl. + unfold no_scan in H16; lia. 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