proposition: Lemma svfl_dst_changed: forall from to v l g1 g2, graph_has_v g1 v -> raw_mark (vlabel g1 v) = false -> (raw_tag (vlabel g1 v) < NO_SCAN_TAG)%Z -> vgeneration v <> from -> copy_compatible g1 -> no_dangling_dst g1 -> from <> to -> (forall i, In i l -> i < length (raw_fields (vlabel g1 v))) -> NoDup l -> graph_has_gen g1 to -> scan_vertex_for_loop from to v l g1 g2 -> forall e i, In i l -> Znth (Z.of_nat i) (make_fields g2 v) = inr e -> vgeneration (dst g2 e) <> from.
proof: Proof. intros ? ? ? ?. induction l; intros ? ? ? ? SCAN; intros; inversion H8; subst. 1: inversion H9. assert (e = (v, i)). { apply make_fields_Znth_edge in H10. 1: rewrite Nat2Z.id in H10; assumption. split. 1: lia. rewrite Zlength_correct. apply inj_lt. erewrite <- svfl_raw_fields; eauto. } assert (graph_has_v g3 v) by (eapply fr_graph_has_v; eauto). assert (raw_mark (vlabel g3 v) = false) by (erewrite <- fr_raw_mark; eauto). assert (graph_has_gen g3 to) by (erewrite <- fr_graph_has_gen; eauto). assert (forall j : nat, In j l -> j < Datatypes.length (raw_fields (vlabel g3 v))). { intros. erewrite <- (fr_raw_fields _ _ _ _ g1); eauto. apply H5. right; assumption. } simpl in H9. destruct H9. - subst a. cut (vgeneration (dst g3 e) <> from). + intros. cut (dst g2 e = dst g3 e). 1: intro HS; rewrite HS; assumption. symmetry. apply (svfl_dst_unchanged from to v l); auto. * erewrite <- fr_raw_tag; eauto. * subst e; simpl; assumption. * intros. subst e. intro. inversion H11. subst. apply NoDup_cons_2 in H6. contradiction. + eapply (fr_O_dst_changed_field from to); eauto. * simpl. intuition auto with *. rewrite Zlength_correct. apply inj_lt. apply H5. left; reflexivity. * unfold make_fields in H8 |-*. erewrite svfl_raw_fields; eauto. - eapply (IHl g3); eauto. + erewrite <- fr_raw_tag; eauto. + eapply (fr_copy_compatible _ _ _ _ g1); eauto. + eapply (fr_O_no_dangling_dst _ _ _ g1); eauto. * simpl. intuition auto with *. rewrite Zlength_correct. apply inj_lt. apply H5. left; reflexivity. * simpl. constructor. + apply NoDup_cons_1 in H6; 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