proposition: Lemma upd_Znth_progressive_list: forall i V, 0 <= i < Z.of_nat V -> upd_Znth i (progressive_list (Z.to_nat i) V) (Vint (Int.repr i), Vint (Int.repr 0)) = progressive_list (Z.to_nat (i + 1)) V.
proof: Proof. intros. induction V. 1: exfalso; simpl in H; intuition. rewrite Nat2Z.inj_succ in H. unfold Z.succ in H. unfold progressive_list. simpl. destruct (le_dec (Z.to_nat i) V). - destruct (le_dec (Z.to_nat (i + 1)) V). + simpl. assert (0 <= i < Z.of_nat V) by (apply inj_le in l0; rewrite Z2Nat.id in l0; lia). unfold progressive_list in IHV. rewrite <- IHV; auto. rewrite upd_Znth_app1; auto. change (rev (prog_list_helper (Z.to_nat i) V)) with (progressive_list (Z.to_nat i) V). rewrite Zlength_correct, progressive_list_length. auto. + assert (Z.to_nat (i + 1) > V)%nat by lia. apply inj_gt in H0. rewrite Z2Nat.id in H0. 2: lia. assert (i = Z.of_nat V) by lia. subst i. clear IHV l n H0 H. rewrite Nat2Z.id. simpl. rewrite upd_Znth_char. * f_equal. change 1 with (Z.of_nat 1). rewrite <- Nat2Z.inj_add, Nat2Z.id. f_equal. apply prog_list_helper_gt; lia. * change (rev (prog_list_helper V V)) with (progressive_list V V). rewrite Zlength_correct, progressive_list_length. auto. - exfalso. assert (Z.to_nat i > V)%nat by lia. apply inj_gt in H0. rewrite Z2Nat.id in H0; lia. Qed.
imports: CertiGraph.lib.List_ext CertiGraph.unionfind.env_unionfind_arr CertiGraph.graph.graph_model CertiGraph.graph.path_lemmas CertiGraph.graph.subgraph2 CertiGraph.graph.graph_relation CertiGraph.graph.reachable_computable CertiGraph.graph.UnionFind CertiGraph.msl_application.ArrayGraph CertiGraph.floyd_ext.share CertiGraph.unionfind.spatial_array_graph Coq.Lists.List CertiGraph.unionfind.uf_arr_specs VST.floyd.library