How do I describe a multiplication of vectorized matrices?

I want to calculate a product of huge (specific) matrices. From a point complexity of view, the product should be taken the form of an elementwise expression.

I tried to "vectorize" the matrices with mxvec / vec_mx and calculate the product via one dimensional streams. But indices access was blocked by the term of enum ('I_p * 'I_q).

I want to know a nth value of enum ('I_p * 'I_q) because I want to decscribe a multiplication of matrices in the form of a primitive expression in an underlying field.

How do I do this? In particular, how do I prove this statement?

From mathcomp Require Import all_ssreflect.

Lemma nth_enum_prod p q (a : 'I_q) :
  val a = index (ord0, a) (enum (prod_finType (ordinal_finType p.+1) (ordinal_finType q))).

Solution

I'm surprised you need to vectorize the matrices if your definition is point-wise, usually you should be able to define your result as \matrix_(i, j) op, for example the standard definition of matrix multiplication is:

\matrix_(i, k) \sum_j (A i j * B j k).

By the way, a quick "dirty" proof of your lemma is:

Lemma nth_enum_prod p q (a : 'I_q) : val a = index (@ord0 p, a) (enum predT).
Proof.
have /(_ _ 'I_q) pair_snd_inj: injective [eta pair ord0] by move => n T i j [].
have Hfst : (ord0, a) \in [seq (ord0, x2) | x2 <- enum 'I_q].
  by move=> n; rewrite mem_map /= ?mem_enum.
rewrite enumT !unlock /= /prod_enum enum_ordS /= index_cat {}Hfst.
by rewrite index_map /= ?index_enum_ord.
Qed.

but indeed if you find yourself using this it means you are into a different kind of problem. I just posted it as an illustration on how to manipulate this kind of expressions.

edit: based on your comment, a more principled way to manipulate the above is to define a lemma about index and products; I've left the full proof as an exercise, but the outline is:

Lemma index_allpairs (T U : eqType) (x : T) (y : U) r s :
  (* TODO: Some conditions are missing here *)
  index (x,y) [seq (x,y) | x <- r , y <- s] =
  size s * (index x r) + index y s.
Proof.
Admitted.

Lemma index_ord_allpairs p q (x : 'I_p) (y : 'I_q) :
  index (x,y) [seq (x,y) | x <- enum 'I_p , y <- enum 'I_q] = q * x + y.
Proof. by rewrite index_allpairs ?mem_enum ?size_enum_ord ?index_enum_ord. Qed.

Lemma nth_enum_prod p q (a : 'I_q) : val a = index (@ord0 p, a) (enum predT).
Proof. by rewrite enumT unlock index_ord_allpairs muln0. Qed.