proposition: Lemma dot_product_assoc : forall m n v v' (M : matrix m n), dot_product v (Vbuild (fun i (ip : i < m ) => dot_product (get_row M ip) v')) =A= dot_product (Vbuild (fun j (jp : j < n) => dot_product v (get_col M jp))) v'.
proof: Proof. induction m; intros. VOtac. rewrite !dot_product_zero. refl. apply Vforall_nth_intro. intros. rewrite Vbuild_nth. unfold dot_product. refl. apply Vforall_intro. intros. destruct H. VSntac v. rewrite (VSn_eq (Vbuild (fun i ip => dot_product (get_row M ip) v'))), dot_product_cons, !Vhead_nth, Vbuild_nth, Vbuild_tail. unfold matrix in M. VSntac M. simpl. match goal with |- _ + dot_product _ (Vbuild ?gen) =A= _ => replace (Vbuild gen) with (Vbuild (fun i ip => dot_product (get_row (Vtail M) ip) v')) end. rewrite (IHm n (Vtail v) v' (Vtail M)). set (a := Vbuild (fun (j : nat) (jp : j < n) => dot_product (Vtail v) (get_col (Vtail M) jp))). set (b := Vbuild (fun (j : nat) (jp : j < n) => dot_product (Vcons (Vnth v (Nat.lt_0_succ m)) (Vtail v)) (Vcons (Vnth (Vhead M) jp) (get_col (Vtail M) jp)))). set (c := Vbuild (fun j jp => Vnth v (Nat.lt_0_succ m) * (Vnth (Vhead M) jp))). set (d := Vbuild (fun j jp => dot_product (Vtail v) (get_col (Vtail M) jp))). assert (b =v c [+] d). apply Vforall2_intro_nth. intros. rewrite vector_plus_nth. unfold b, c, d. rewrite !Vbuild_nth, dot_product_cons. refl. trans (dot_product (c[+]d) v'). rewrite dot_product_distr_l, dot_product_distr_mult. refl. apply dot_product_mor. hyp. refl. apply Veq_nth. intros. rewrite !Vbuild_nth, lt_Sn_nS. refl. Qed.
imports: Coq(List Setoid Morphisms) CoLoR(VecArith OrdSemiRing VecUtil NatUtil LogicUtil RelUtil)