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

Question

我想计算巨大（特定）矩阵的乘积。从复杂度的角度来看，乘积应该采取逐元素表达式的形式。

我尝试 "vectorize" 使用 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).

顺便说一下，对你的引理的快速 "dirty" 证明是：

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.

但实际上，如果您发现自己在使用它，则意味着您遇到了另一种问题。我只是将其作为如何操作此类表达式的说明发布。

edit：根据您的评论，操作上述内容的更有原则的方法是定义关于 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.

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

How do I describe a multiplication of vectorized matrices?

coq

ssreflect