proposition: Lemma upd_Znth_Graph_redirect_parent: forall (i root : Z) (g: UFGraph) n (Hw: weak_valid g root) (Hv: vvalid g i) (Hi: ~ reachable g root i), 0 <= i < Z.of_nat n -> 0 <= root < Z.of_nat n -> upd_Znth i (map (fun m : Z => vgamma2cdata (vgamma (lg_gg g) m)) (nat_inc_list n)) (Vint (Int.repr root), Vint (Int.repr (Z.of_nat (vlabel (lg_gg g) i)))) = map (fun m : Z => vgamma2cdata (vgamma (lg_gg (Graph_gen_redirect_parent g i root Hw Hv Hi)) m))(nat_inc_list n).
proof: Proof. intros. assert (Zlength (map (fun m : Z => vgamma2cdata (vgamma (lg_gg g) m)) (nat_inc_list n)) = Z.of_nat n) by (rewrite Zlength_map, Zlength_correct, nat_inc_list_length; auto). apply (list_eq_Znth _ _ n). - rewrite <- (Nat2Z.id n) at 2. rewrite <- Zlength_length. 2: lia. rewrite upd_Znth_Zlength; auto. rewrite <- H1 in H. auto. - rewrite list_length_map, nat_inc_list_length; auto. - intros. rewrite Znth_nat_inc_list; auto. rewrite (upd_Znth_lookup' (Z.of_nat n)); auto. rewrite Znth_nat_inc_list; auto. unfold vgamma2cdata, vgamma, UnionFindGraph.vgamma. simpl. unfold graph_gen.updateEdgeFunc. unfold EquivDec.equiv_dec, Z_EqDec, zeq. destruct (Z.eq_dec j i). + subst j. destruct (Z.eq_dec i i). 2: exfalso; apply n0; auto. f_equal. destruct (Z_lt_dec root 0); [exfalso; lia | auto]. + f_equal. destruct (Z.eq_dec i j). 1: exfalso; intuition. auto. 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