proposition: Lemma upd_Znth_tl {A}: forall (i: Z) (l: list A) (x: A), 0 <= i -> l <> nil -> tl (upd_Znth (i + 1) l x) = upd_Znth i (tl l) x.
proof: Proof. intros. destruct l; simpl. 1: contradiction. destruct (Z_lt_le_dec i (Zlength l)). 2: rewrite !upd_Znth_out_of_range; auto; [|rewrite Zlength_cons]; lia. rewrite !upd_Znth_unfold; auto. 2: rewrite Zlength_cons; lia. unfold_sublist_old. replace (i - 0) with i by lia. replace (i + 1 - 0) with (i + 1) by lia. simpl. assert (forall j, 0 <= j -> Z.to_nat (j + 1) = S (Z.to_nat j)) by (intros; rewrite <- Z2Nat.inj_succ; rep_lia). rewrite (H1 _ H). simpl tl. do 3 f_equal. - f_equal. rewrite Zlength_cons. lia. - remember (S (Z.to_nat i)). replace (Z.to_nat (i + 1 + 1)) with (S n). + simpl. reflexivity. + do 2 rewrite H1 by lia. subst n. reflexivity. 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