proposition: Lemma frr_bep_aux: forall from to (roots1 roots2: roots_t) g1 g2, from <> to -> sound_gc_graph g1 -> graph_has_gen g1 to -> no_dangling_dst g1 -> copy_compatible g1 -> roots_graph_compatible roots1 g1 -> copied_vertex_prop g1 from to -> gen_unmarked g1 to -> forward_roots_relation from to roots1 g1 roots2 g2 -> forall done, backward_edge_prop g1 (done++roots1) from to -> backward_edge_prop g2 (done++roots2) from to.
proof: Proof. induction 9; intros; auto. assert (H0' := fr_O_sound _ _ _ _ _ H0 H1 H7). assert (H1' := proj1 (fr_graph_has_gen _ _ _ _ _ _ H1 H7 to) H1). assert (H3' := fr_copy_compatible _ _ _ _ _ _ H H1 H7 H3). assert (H2' := fr_O_no_dangling_dst from to (inl 0) g1 g2 (r::roots1) ltac:(simpl; list_solve) H1 H4 H3 H7 H2). assert (H4' := fr_roots_graph_compatible 0 from to (inl 0) g1 g2 (r::roots1) H1 ltac:(simpl; list_solve) H3 H7 H H4). simpl in H4'. rewrite Znth_0_cons, upd_Znth0 in H4'. change (?A::?B) with ([A]++B) in H4'. rewrite roots_graph_compatible_app in H4'; destruct H4'. assert (H5' := fr_O_copied_vertex_prop from to (inl 0) g1 g2 (r::roots1) H H1 H0 H2 ltac:(simpl; list_solve) H7 H5). change (?A::?B) with ([A]++B) in H9|-*. rewrite app_assoc in H9|-*. apply IHforward_roots_relation; auto. eapply fr_gen_unmarked; try apply H7; auto. assert (backward_edge_prop g2 ([upd_root from to g1 r] ++ done++roots1) from to). { pose proof fr_O_backward_edge_prop from to (inl 0) g1 g2 (r::done++roots1). simpl in H12. rewrite upd_Znth0, Znth_0_cons in H12. apply H12; auto. simpl; list_solve. clear - H9. eapply backward_edge_prop_incl; try apply H9. intros. change (r::?B) with ([r]++B). rewrite !in_app in H|-*. tauto. } clear - H12. eapply backward_edge_prop_incl; try apply H12. clear; intros. rewrite !in_app in H|-*. tauto. 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