proposition: Lemma graph_to_list_to_mat: forall g (f : E -> E) u i, 0 <= u < size -> 0 <= i < size -> 0 < size -> Forall (fun list => Zlength list = size) (graph_to_mat g f) -> Znth (u * size + i) (graph_to_list g f) = Znth i (Znth u (graph_to_mat g f)).
proof: Proof. intros. assert (Htemp: 0 <= size) by lia. clear Htemp. unfold graph_to_list, graph_to_mat in *. rewrite <- (Z2Nat.id size) in H by lia. generalize dependent u. induction (Z.to_nat size). 1: intros; lia. intros. simpl. rewrite map_app, concat_app. assert (Forall (fun list : list Z => Zlength list = size) (map (vert_to_list g f) (nat_inc_list n))). { rewrite Forall_forall in H2 |- *. intros. apply H2. simpl. rewrite map_app. apply in_or_app. left; trivial. } specialize (IHn H3). destruct H. rewrite Nat2Z.inj_succ in H4. apply Z.lt_succ_r in H4. rewrite Z.le_lteq in H4. destruct H4. - repeat rewrite app_Znth1. + apply IHn; trivial; lia. + rewrite Zlength_map, nat_inc_list_Zlength; lia. + rewrite (Zlength_concat _ size); trivial; [|lia]. rewrite <- (Z.succ_pred (Z.of_nat n)). rewrite Z.mul_succ_l. apply Z.add_le_lt_mono; try lia. apply Zorder.Zmult_le_compat_r; lia. - clear IHn. repeat rewrite app_Znth2. + rewrite (Zlength_concat _ size); trivial; [|lia]. replace (u * size + i - Z.of_nat n * size) with (u * size - Z.of_nat n * size + i) by lia. replace (u * size - Z.of_nat n * size) with ((u - Z.of_nat n) * size) by lia. rewrite Zlength_map, nat_inc_list_Zlength. simpl. rewrite app_nil_r. replace (u - Z.of_nat n) with 0 by lia. rewrite Znth_0_cons. replace (0 * size + i) with i by lia. reflexivity. + rewrite Zlength_map, nat_inc_list_Zlength; lia. + rewrite (Zlength_concat _ size); trivial; lia. Qed.
imports: Coq.ZArith.BinInt Coq.ZArith.Zcomplements Coq.micromega.Lia Coq.ZArith.Znat compcert.lib.Integers compcert.common.Values compcert.export.Clightdefs VST.veric.expr VST.veric.mpred VST.floyd.forward VST.zlist.sublist VST.floyd.field_at VST.floyd.coqlib3 VST.msl.iter_sepcon VST.msl.seplog CertiGraph.graph.graph_model CertiGraph.lib.List_ext CertiGraph.graph.MathAdjMatGraph