The Coq mailing list

[Mohit Tekriwal <tmohit AT umich.edu>]

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.

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.

--

Mohit Tekriwal,

PhD Candidate,

Department of Aerospace Engineering,

University of Michigan.