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

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.

但是确实，如果您发现自己正在使用此工具，则意味着您遇到了另一种问题。我只是将其发布为说明，以说明如何操纵这种表达。