proposition: Lemma frr_dsr_no_edge2gen: forall from to roots roots' g g1 g2, graph_has_gen g to -> from <> to -> gen_unmarked g to -> copy_compatible g -> no_dangling_dst g -> roots_graph_compatible roots g -> forward_roots_relation from to roots g roots' g1 -> do_scan_relation from to (number_of_vertices (nth_gen g to)) g1 g2 -> no_edge2gen g from -> no_edge2gen g2 from.
proof: Proof. intros. unfold no_edge2gen in *. intros. specialize (H7 _ H8). destruct (Nat.eq_dec another to). - subst. unfold gen2gen_no_edge in *. intros. destruct H9. simpl fst in *. destruct H6 as [m [? ?]]. assert (graph_has_gen g1 to) by (erewrite <- frr_graph_has_gen; eauto). assert (graph_has_v g (to, vidx) \/ gen_v_num g to <= vidx < gen_v_num g2 to). { eapply (svwl_graph_has_v_inv from to _ g1 g2) in H9; eauto. simpl in H9. destruct H9. - eapply (frr_graph_has_v_inv from _ _ g) in H9; eauto. simpl in H9. destruct H9. 1: left; assumption. right. destruct H9 as [_ [? ?]]. split; auto. apply svwl_gen_v_num_to in H6; [lia | assumption]. - right. destruct H9 as [_ [? ?]]. split; auto. apply frr_gen_v_num_to in H5; [lia | assumption]. } destruct H13. + assert (graph_has_v g1 (to, vidx)) by (eapply (frr_graph_has_v from to _ g); eauto). assert (get_edges g (to, vidx) = get_edges g2 (to, vidx)). { transitivity (get_edges g1 (to, vidx)); unfold get_edges, make_fields. - erewrite frr_raw_fields; eauto. - erewrite svwl_raw_fields; eauto. } rewrite <- H15 in H10. assert (graph_has_e g (to, vidx, eidx)) by (split; simpl; assumption). specialize (H7 _ _ H16). erewrite (frr_dst_unchanged _ _ _ _ _ g1) in H7; eauto. erewrite (svwl_dst_unchanged) in H7; eauto; simpl. * eapply (frr_gen_unmarked _ _ _ g); eauto. * repeat intro. rewrite nat_seq_In_iff in H18. destruct H18 as [? _]. destruct H13. simpl in H19. red in H19. lia. + eapply svwl_no_edge2from; eauto. * eapply (frr_gen_unmarked _ _ _ g); eauto. * eapply (frr_copy_compatible from to _ g); eauto. * eapply (frr_no_dangling_dst _ _ _ g); eauto. * apply nat_seq_NoDup. * rewrite nat_seq_In_iff. unfold gen_has_index in H11. unfold gen_v_num in H13. lia. - eapply (frr_gen2gen_no_edge _ _ _ g _ g1) in H7; eauto. destruct H6 as [m [? ?]]. eapply (svwl_gen2gen_no_edge from to _ g1 g2); eauto. + erewrite <- frr_graph_has_gen; eauto. + eapply frr_gen_unmarked; eauto. Qed.
imports: Coq.ZArith.ZArith Coq.Program.Basics Coq.micromega.Lia 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 VST.zlist.list_solver CertiGraph.lib.EquivDec_ext CertiGraph.lib.List_ext CertiGraph.graph.graph_model CertiGraph.graph.graph_gen