proposition: Lemma mint_eval_var_aux : forall M i k (v : vector vec k) (ip : i < k), add_vectors (Vmap2 mat_vec_prod (Vreplace (Vconst (zero_matrix dim dim) k) ip M) v) =v col_mat_to_vec (M <*> (vec_to_col_mat (Vnth v ip))).
proof: Proof. induction i; intros. destruct k. lia. unfold add_vectors. simpl. fold (add_vectors (Vmap2 mat_vec_prod (Vconst (zero_matrix dim dim) k) (Vtail v))). assert (add_vectors (Vmap2 mat_vec_prod (Vconst (zero_matrix dim dim) k) (Vtail v)) =v @zero_vec dim). 2:{ rewrite H, vector_plus_zero_l. replace (Vhead v) with (Vnth v ip). refl. rewrite Vhead_nth, (lt_unique (Nat.lt_0_succ k) ip). refl. } apply add_vectors_zero. apply Vforall_nth_intro. intros. rewrite Vnth_map2, Vnth_const. unfold M.mat_vec_prod. rewrite zero_matrix_mult_l. apply Vforall2_intro_nth. intros. rewrite Vnth_col_mat. unfold zero_matrix, zero_vec. rewrite mat_build_elem, Vnth_const. refl. destruct k. lia. rewrite Vreplace_tail. simpl. rewrite add_vectors_cons. unfold M.mat_vec_prod at 1. rewrite zero_matrix_mult_l. assert (col_mat_to_vec (zero_matrix dim 1) =v zero_vec dim). apply Vforall2_intro_nth. intros. rewrite Vnth_col_mat. unfold zero_matrix, zero_vec. rewrite mat_build_elem, Vnth_const. refl. rewrite H, vector_plus_zero_l, IHi, Vnth_tail, (le_unique (NatCompat.lt_n_S (NatCompat.lt_S_n ip)) ip). refl. Qed.
imports: CoLoR(Matrix AMonAlg VecUtil OrdSemiRing ATrs LogicUtil RelUtil NatUtil AWFMInterpretation) Coq(PeanoNat Setoid Morphisms)