Ssreflect Users Discussion List

[Vincent Siles <>]

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