proposition: Lemma frr_rom_aux: forall from to (roots1 roots2: roots_t) g1 g2, from <> to -> sound_gc_graph g1 -> graph_has_gen g1 to -> roots_graph_compatible roots1 g1 -> no_dangling_dst g1 -> copied_vertex_prop g1 from to -> copy_compatible g1 -> forward_roots_relation from to roots1 g1 roots2 g2 -> forall done v, roots_graph_compatible done g1 -> (reachable_or_marked from g1 (done++roots1) v <-> reachable_or_marked from g2 (done++roots2) v).
proof: Proof. intros * ? ? ? ? ? ? ? ?. induction H6; [ tauto | ]; intros. rename IHforward_roots_relation into IH. assert (H0' := fr_O_sound _ _ _ _ _ H0 H1 H6). assert (H1' := proj1 (fr_graph_has_gen _ _ _ _ _ _ H1 H6 to) H1). assert (H5' := fr_copy_compatible _ _ _ _ _ _ H H1 H6 H5). assert (H3' := fr_O_no_dangling_dst from to (inl 0) g1 g2 (r::roots1) ltac:(simpl; list_solve) H1 H2 H5 H6 H3). assert (H2' := fr_roots_graph_compatible 0 from to (inl (Zlength done)) g1 g2 (done++r::roots1) H1 ltac:(simpl; list_solve) H5). simpl in H2'. autorewrite with sublist in H2'. rewrite upd_Znth0 in H2'. rewrite roots_graph_compatible_app in H2'. specialize (H2' H6 H (conj H8 H2)). change (?A::?B) with ([A]++B) in H2'. rewrite !roots_graph_compatible_app in H2'; destruct H2' as [H11 [H2'' H2']]. assert (H4' :=fr_O_copied_vertex_prop from to (inl 0) g1 g2 (r::roots1) H H1 H0 H3 ltac:(simpl; list_solve) H6 H4). specialize (IH H0' H1' H2' H3' H4' H5' (done +:: upd_root from to g1 r) v). rewrite <- !app_assoc in IH. rewrite <- IH; clear IH. 2: rewrite roots_graph_compatible_app; split; auto. rewrite (fr_O_reachable_or_marked from to (inl (Zlength done)) g1 g2 (done++r::roots1)); auto. - simpl. autorewrite with sublist. rewrite upd_Znth0. tauto. - change (r::roots1) with ([r]++roots1). rewrite roots_graph_compatible_app; split; auto. - simpl; list_solve. - hnf; auto. - simpl. autorewrite with sublist. auto. 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