如何描述向量化矩阵的乘法？

Question

我想计算一个巨大(特定)矩阵的乘积。从复杂性的角度来看，产品应该采取元素表达式的形式。

我尝试用mxvec / vec_mx“矢量化”矩阵，并通过一维流计算乘积。但指数访问被enum ('I_p * 'I_q)术语所阻断。

我想知道enum ('I_p * 'I_q)的第n个值，因为我想在底层字段中以原始表达式的形式限制矩阵的乘法。

我该怎么做？特别是，我如何证明这一说法？

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))).

Answer 1

我很惊讶，如果您的定义是点式的，那么需要将矩阵向量化，通常您应该能够将结果定义为\matrix_(i, j) op，例如，矩阵乘法的标准定义是：

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

顺便说一句，关于你的引理的一个快速的“肮脏”证明是：

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.

但实际上，如果你发现自己使用了这个，那就意味着你陷入了另一种问题。我只是把它作为如何处理这类表达式的一个例子。

编辑：基于您的评论，操作上述内容的一种更有原则的方法是定义关于index和产品的引理；我将完整的证据作为练习留下，但大纲是：

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.