proposition: Lemma svwl_no_edge2from: forall from to l g1 g2, graph_has_gen g1 to -> scan_vertex_while_loop from to l g1 g2 -> gen_unmarked g1 to -> copy_compatible g1 -> no_dangling_dst g1 -> from <> to -> NoDup l -> forall e i, In i l -> In e (get_edges g2 (to, i)) -> vgeneration (dst g2 e) <> from.
proof: Proof. do 3 intro. induction l; intros; inversion H0; subst. 1: inversion H6. - simpl in H6. destruct H6. 2: apply NoDup_cons_1 in H5; eapply IHl; eauto. subst a. assert (In e (get_edges g1 (to, i))). { unfold get_edges, make_fields in H7 |-*. erewrite svwl_raw_fields; eauto. split; simpl; assumption. } rewrite no_scan_no_edge in H6. 2: assumption. inversion H6. - simpl in H6. assert (graph_has_gen g3 to) by (erewrite <- svfl_graph_has_gen; eauto). assert (gen_unmarked g3 to) by (eapply (svfl_gen_unmarked _ _ _ _ g1); eauto). destruct H6. + subst a. cut (vgeneration (dst g3 e) <> from). * intros. cut (dst g3 e = dst g2 e). 1: intros HS; rewrite <- HS; assumption. eapply svwl_dst_unchanged; eauto. -- erewrite get_edges_fst; eauto. eapply (svfl_graph_has_v _ _ _ _ g1); eauto. split; simpl; assumption. -- intros. erewrite get_edges_fst; eauto. simpl. apply NoDup_cons_2 in H5. assumption. * assert (graph_has_v g1 (to, i)) by (split; simpl; assumption). eapply svfl_no_edge2from; eauto. unfold no_scan in H11; lia. unfold get_edges, make_fields in H7 |-*. erewrite svwl_raw_fields; eauto. eapply (svfl_graph_has_v _ _ _ _ g1); eauto. + eapply (IHl g3); eauto. * eapply (svfl_copy_compatible _ _ _ _ g1); eauto. * eapply (svfl_no_dangling_dst from to); eauto. -- split; simpl; assumption. -- unfold no_scan in H11. lia. -- intros. rewrite nat_inc_list_In_iff in H13. assumption. * apply NoDup_cons_1 in H5. assumption. 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