## Stream: math-comp users

### Topic: A matrix mul proof

#### Julin Shaji (Oct 26 2023 at 07:30):

I had been trying this small proof with mathcomp matrix:

Goal
let mt: 'M[bool]_(2,3) := \matrix_(i<2, j<3) (if i == 0 && (j == 1) :> nat then 1 else 0) in
let rw := (\row_i (if i == 0 then 1 else 0)) *m mt in
(\sum_j (rw 0 j)) == 1.
Proof.


But I couldn't make any progress on solving it.

Because on doing a simplification, the goal became

\sum_(j < 3)
(\row_i (if i == 0 then 1 else 0) *m \matrix_(i, _)
(if i == 0%N then 1 else 0)) 0 j == 1


Can we simplify using definition of *m here? rewrite mxE didn't work. Possibly because the *m is inside the \sum?

#### Pierre Roux (Oct 26 2023 at 07:49):

Apparently, we don't even need to unfold the matrix multiplication explicitly, this works:

From mathcomp Require Import all_ssreflect all_algebra.

Local Open Scope ring_scope.

Goal
let mt: 'M[bool]_(2,3) := \matrix_(i<2, j<3) (if i == 0 && (j == 1) :> nat then 1 else 0) in
let rw := (\row_i (if i == 0 then 1 else 0)) *m mt in
(\sum_j (rw 0 j)) == 1.
Proof. by do 2 ![rewrite /= !big_ord_recl !big_ord0 !mxE]. Qed.


#### Paolo Giarrusso (Oct 26 2023 at 12:14):

Possibly because the *m is inside the \sum?

Yeah plain rewrite (vanilla or ssreflect) typically does not work under binders (and \sum_j binds j), but there are alternatives (for ssreflect that's under)

Last updated: Jul 23 2024 at 20:01 UTC