proposition: Lemma svwl_dst_unchanged: forall from to l g1 g2, graph_has_gen g1 to -> scan_vertex_while_loop from to l g1 g2 -> from <> to -> gen_unmarked g1 to -> forall e, graph_has_v g1 (fst e) -> (vgeneration (fst e) = to -> ~ In (vindex (fst e)) l) -> dst g1 e = dst g2 e.
proof: Proof. intros. induction H0. 1: reflexivity. - apply IHscan_vertex_while_loop; try assumption. intros. specialize (H4 H7). intro. apply H4. right. assumption. - transitivity (dst g2 e). + eapply (svfl_dst_unchanged from to (to, i)); eauto. * split; assumption. * unfold no_scan in H5. lia. * intros. rewrite nat_inc_list_In_iff in H8. assumption. * intros. destruct (Nat.eq_dec (vgeneration (fst e)) to). -- specialize (H4 e0). intro. subst e. simpl in H4. apply H4. left; auto. -- intro. subst e. simpl in n. apply n; reflexivity. + apply IHscan_vertex_while_loop. * erewrite <- svfl_graph_has_gen; eauto. * eapply svfl_gen_unmarked; eauto. * eapply svfl_graph_has_v; eauto. * intros. specialize (H4 H8). intro. apply H4. right; 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