Как мне описать умножение векторизованных матриц? - PullRequest
Новая
       71

Как мне описать умножение векторизованных матриц?

1 голос
/ 07 марта 2020

Я хочу рассчитать произведение огромных (специфицируемых c) матриц. С точки зрения сложности, продукт должен быть представлен в виде поэлементного выражения.

Я попытался «векторизовать» матрицы с помощью 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))).

1 Ответ

0 голосов
/ 08 марта 2020

Я удивлен, что вам нужно векторизовать матрицы, если ваше определение является точечным, обычно вы должны иметь возможность определить свой результат как \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.

, но, действительно, если вы обнаружите, что используете это, это означает, что вы столкнулись с проблемой другого рода. Я только что опубликовал это как иллюстрацию о том, как манипулировать такими выражениями.

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