proposition: Lemma frl_semi_iso: forall (from to : nat) g l1 (roots1' roots1 roots2: roots_t) (g1 g2 : LGraph), from <> to -> sound_gc_graph g -> sound_gc_graph g1 -> graph_has_gen g1 to -> roots_graph_compatible roots1 g1 -> no_dangling_dst g -> no_dangling_dst g1 -> copy_compatible g1 -> gc_graph_semi_iso g g1 from to l1 -> forward_roots_relation from to roots1 g1 roots2 g2 -> exists l2, gc_graph_semi_iso g g2 from to (l2++l1) /\ roots2 = quasi_roots_map roots1 (l2++l1).
proof: Proof. intros. revert l1 H1 H2 H3 H5 H6 H7. induction H8; intros; [ exists nil; simpl; auto | ]. destruct (fr_O_semi_iso from to (inl 0) g g1 g2 (r::roots1) l1) as [l2 [? [? ?]]]; simpl; auto; try list_solve. destruct (IHforward_roots_relation (l2++l1)) as [l3 [? ?]]; auto. - eapply fr_O_sound; eauto. - erewrite <- fr_graph_has_gen; eauto. - pose proof fr_roots_graph_compatible 0 from to (inl 0) g1 g2 (r::roots1) H3 ltac:(simpl; list_solve) H7. simpl in H13. rewrite Znth_0_cons, upd_Znth0 in H13. specialize (H13 H1 H H5). change (?A :: ?B) with ([A]++B) in H13. rewrite roots_graph_compatible_app in H13. destruct H13. auto. - pose proof fr_O_no_dangling_dst from to (inl 0) g1 g2 (r::roots1) ltac:(simpl; list_solve) H3 H5 H7. simpl in H13. rewrite Znth_0_cons in H13. auto. - eapply fr_copy_compatible; eauto. - exists (l3++l2). rewrite <- app_assoc. split; auto. subst roots2. f_equal. simpl in H11. unfold restricted_roots_map in H11. simpl in H11. rewrite !upd_Znth0, !Znth_0_cons in H11. inv H11. rewrite H15. unfold root_map. destruct r; auto. f_equal. assert (DoubleNoDup (l3 ++ l2 ++ l1)) by (eapply semi_iso_DoubleNoDup; eauto). apply list_map_DoubleNoDup_incl_eq; auto. simpl in H12. intros. apply (H12 0); auto. list_solve. eapply semi_iso_In_map_fst in H14; 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