Ssreflect Users Discussion List

[Georges Gonthier <>]

  You shouldn't be doing induction. Split M using vsubmxK, compute the block 
dot product with mul_row_col; the secont term is 0, mul_scalar_mx aligns the 
scaling factors, so you're only left with proving that usubmx M = row ord0 M, 
which rowP and ord1 will handle. By the way, the usage in matrix is to use 0 
rather than ord0 for the index 0.

Georges

-----Original Message-----
From: Vincent Siles [] 
Sent: 19 May 2011 18:27
To: Georges Gonthier
Cc: 
Subject: Re: basic question about matrices

I'm proving the correctness of a function, and I changed a bit the algorithm 
without changing the specification to deal with the same cases (n = 1 is a 
particular case is the algorithm, but not in the specification). I'll try to 
make a special case for it and it should ease this proof.

A new question which arised in the following lemma:

Lemma row_mx1_mul0 : forall (n m:nat) (a: R) (M : 'M[R]_(1+n,m)),
  row_mx (a%:M) 0 *m M = a *: row ord0 M.

(a 0 ..........0) * M = a x (first row of M)

I'm not sure how to prove it so I started to perform an induction on m, and I 
wonder how should I deal with the "dummy" case m = 0, so M is an "empty"
matrix ?

Vincent


2011/5/19 Georges Gonthier <>:
>  I usually use the mx11_scalar lemma to deal with 1x1 matrices; in the 
> reverse direction it can be used to change the rhs to col_mx (usubmx C) 0, 
> then that last 0 can be changed to dsubmx (C : 'M_(1 + 0)) with flatmx0, 
> and with vsubmxK and mul1mx you'll be done.
>  However, somehow you shouldn't be getting an equation between matrices 
> with different shapes, so there ought to be something wrong with the way 
> you set up your proof.
>
>   Georges
>
> -----Original Message-----
> From: Vincent Siles []
> Sent: 19 May 2011 16:35
> To: 
> Subject: basic question about matrices
>
> Hi everyone,
> I'm trying to learn how to use the matrix library of ssreflect, and I'm a 
> bit lost.
> On one of my easy case, I have a 1x1 matrix, and I want to prove the 
> following property
>
>  C : 'M_1
>  ============================
>   1%:M *m C = col_mx ((usubmx C) ord0 ord0)%:M 0
>
> Is there a way to tell ssreflect "C is a 1x1 matrix, so just extract its 
> value from the matrix" ?
>
> How can I get read of the col_mx ? (if I'm right, the left part is a
> 1x1 matrix, so the col_mx ... 0
> should disappear ?)
>
>
> Cheers,
> Vincent
>
>