1

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

我试图用mxvec/对矩阵进行“矢量化”，vec_mx并通过一维流计算乘积。但是索引访问被enum ('I_p * 'I_q).

我想知道第 n 个值，enum ('I_p * 'I_q)因为我想以基础字段中的原始表达式的形式描述矩阵的乘法。

我该怎么做呢？特别是，我如何证明这个陈述？

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

1 回答 1

0

如果您的定义是逐点的，我很惊讶您需要对矩阵进行矢量化，通常您应该能够将结果定义为\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.
于 2020-03-07T23:31:54.013 回答