Ssreflect Users Discussion List

[Mohit Tekriwal <>]

Hello,

I am trying to use the matrix algebra package in mathcomp and I am having 
trouble understanding how to instantiate the matrices and prove certain 
properties on it.

For example, I want to instantiate the matrix:

A= [ 1, 2; 3, 4] 

and be able to access any element Aij. The entries of A are reals.

Using the Coquelicot definition of matrix, I can define the matrix as:

Definition A:= mk_matrix 2%nat 2%nat (fun i j=>
               if (andb (eqb i 0) (eqb j 0)) then 1 else
                 if (andb (eqb i 0) (eqb j 1)) then 2 else
                   if (andb (eqb i 1) (eqb j 0)) then 3 else 4).

To access an element at index (0,1), I can use the following definition:
Definition A01:= coeff_mat 0 A 0%nat 1%nat.
Compute A01.

That gives me 2.

I tried the following in mathcomp:

Definition A1 := @matrix_of_fun _ 2%nat 2%nat matrix_key (fun i j=> 
               if (andb (eqb i 0) (eqb j 0)) then 1 else
                 if (andb (eqb i 0) (eqb j 1)) then 2 else
                   if (andb (eqb i 1) (eqb j 0)) then 3 else 4).

Definition A1_00:= A1 (inord 0) (inord 0).
Compute A1_00.

That gives me:
let......: (fun _ : 'I_2 * 'I_2 => R)      (inord 0, inord 0)

instead of 2.

Also, when trying to prove that the trace of A is 5 in mathcomp: 
Lemma trace_is_5: mxtrace A1 = 5.

I get the following error message:

The term "A1" has type "'M_2"
while it is expected to have type 
"'M_?n".

Am I missing something? How do I use the theorems/lemmas defined in mathcomp 
for specific matrices ? 

It would be really nice  if someone can provide inputs on this issue.

Thanking you,
Mohit Tekriwal.