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: Oct 13 2024 at 01:02 UTC