## Stream: math-comp users

### Topic: Matrix representation

#### Julin Shaji (Oct 03 2023 at 15:49):

Hi. I was trying to have a representation of matrices using mathcomp and upon searching online, came across:
https://github.com/VeriNum/LAProof/blob/main/floatlib.v

It had this definition for matrix:

``````Definition matrix t := list (list (ftype t)).
``````

But I wasn't sure I understood it properly.
Doesn't this line mean that `matrix t` is a list of lists where `t` is a finite type?
Does that also somehow constraint it to be a proper matrix? As in every row has same number of elements?

#### Julin Shaji (Oct 03 2023 at 15:52):

Oh.. I guess the proof is made from here:
https://github.com/verified-network-toolchain/Verified-FEC/blob/cav22/proofs/Matrix/ListMatrix.v#L392

``````Definition rect {A} (l: list (list A)) m n : Prop :=
Zlength l = m /\ 0 <= n /\ Forall (fun x => Zlength x = n) l.
``````

#### Emilio Jesús Gallego Arias (Oct 03 2023 at 15:55):

Hi @Julin Shaji , math-comp matrices are defined in https://math-comp.github.io/htmldoc_2_0_0/mathcomp.algebra.matrix.html

#### Emilio Jesús Gallego Arias (Oct 03 2023 at 15:57):

See also the math-comp book , as pointed out in the other thread, section 7.8 explains how matrices are built

#### Julin Shaji (Oct 09 2023 at 05:55):

To get the notations for matrix, do we need to import some module?

I tried:

``````From mathcomp Require Import all_ssreflect all_algebra.

Compute \matrix_(i<3, j<7) if i==j then 1 else 0.
(*
Unknown interpretation for notation "\matrix_ ( _ < _ , _ < _ ) _".
*)
``````

but that's giving error.

#### Julin Shaji (Oct 09 2023 at 05:56):

Opening `ring_scope` changes the error to:

``````Local Open Scope ring_scope.

Compute \matrix_(i<3, j<7) if i==j then 1 else 0.
(*
In environment
i : ordinal_finType 3
j : ordinal_finType 7
The term "j" has type "Finite.sort (ordinal_finType 7)"
while it is expected to have type "Equality.sort (ordinal_finType 3)".
*)
``````

#### Julin Shaji (Oct 09 2023 at 05:59):

`Compute \matrix_(i<3, j<7) (fun i j => if i==j then 1 else 0).` worked though.

#### Julin Shaji (Oct 09 2023 at 06:01):

But that seems to leave holes.

#### Julin Shaji (Oct 09 2023 at 06:15):

``````Example eg1 := \matrix_(i<3, j<7) (fun i j => if i==j then 1 else 0).
(*
The following term contains unresolved implicit arguments:
(\matrix_(_, _) (fun i0 j0 : ?T =>
if i0 == j0 as x return ?t@{i:=i0; j:=j0; b:=x}
then 1
else 0))
More precisely:
- ?T: Cannot infer the implicit parameter T of eq_op whose type is "eqType".
- ?t: Cannot infer ?t in the partial instance "GRing.Ring.sort ?t" found for
this placeholder of type "Type" in environment:
i, j : ?T
b : bool
*)
``````

#### Quentin VERMANDE (Oct 09 2023 at 07:05):

The notation is indeed in ring_scope, there is nothing more to import. In the second code snippet, the problem is that the types of i and j mismatch (and Coq can't coerce between 'I_3 and 'I_7), "(i : nat) == j" or "(i == j :> nat)" would work (and you need to give the type of 1 and/or 0) . In the last one, I think the underscores mean that the arguments are not used. The error is that, since you re-bind i and j when declaring the function, Coq does not know what type to give them (and it does not know what the return type should be either).

#### Julin Shaji (Oct 09 2023 at 07:33):

I tried this but got error:

``````Fail Compute \matrix_(i<3, j<7) if (i:nat)==j then 1 else 0.
(*
The command has indeed failed with message:
In environment
i : ordinal_finType 3
j : ordinal_finType 7
Unable to unify "?t0" with "?t@{b:=(i : nat) == j}" (cannot satisfy
constraint "?t0" == "?t@{b:=(i : nat) == j}").
*)
Fail Compute \matrix_(i<3, j<7) if (i==j :> nat) then 1 else 0.
(*
The command has indeed failed with message:
In environment
i : ordinal_finType 3
j : ordinal_finType 7
Unable to unify "?t0" with "?t@{b:=i == j :> nat}" (cannot satisfy constraint
"?t0" == "?t@{b:=i == j :> nat}").
*)
``````

Is this not what was meant?

From the error, I suppose `i` is of type `'I_3` and `j` is of type `'I_7`. And the type mismatch is what's causing the problem (I guess that's what was mentioned as well). Is it so?

#### Julin Shaji (Oct 09 2023 at 07:34):

Quentin VERMANDE said:

and you need to give the type of 1 and/or 0

You mean that of a ring or is this something different?

#### Pierre Roux (Oct 09 2023 at 07:49):

In ring_scope, `1` and `0` are the units of some ring so you need to precise which one. For instance

``````Section Mat.
Variable R : ringType.
Check \matrix_(i<3, j<7) if i == j :> nat then 1 : R else 0.
``````

#### Pierre Roux (Oct 09 2023 at 07:50):

(but I agree the error message is not very informative)

#### Emilio Jesús Gallego Arias (Oct 09 2023 at 16:04):

Indeed these kind of problems are really off putting for beginners, I wonder if we could add some custom error rules as to help with the messages?

#### Michael Soegtrop (Oct 10 2023 at 06:26):

Some example files might also help ...

#### Julin Shaji (Oct 10 2023 at 10:24):

Another doubt.

How can a `\matrix` be converted to a `seq (seq))`? Do we have to use coqEAL library for that or is it doable using mathcomp alone?

#### Julin Shaji (Oct 10 2023 at 10:26):

Been trying to read https://github.com/coq-community/coqeal/blob/master/refinements/seqmx.v for a while but didn't pull through all of it..

#### Cyril Cohen (Oct 10 2023 at 10:28):

Indeed for now the only library I know that performs that is CoqEAL but it's limited to computations of concrete matrices.

#### Julin Shaji (Oct 10 2023 at 10:28):

How can we get the function used to build the matrix in `\matrix`?

#### Cyril Cohen (Oct 10 2023 at 10:28):

examples of usage are near the end of the file: https://github.com/coq-community/coqeal/blob/master/refinements/seqmx.v#L1380-L1472

#### Julin Shaji (Oct 10 2023 at 10:29):

Cyril Cohen said:

Indeed for now the only library I know that performs that is CoqEAL but it's limited to computations of concrete matrices.

Concrete as in matrices whose dimensions have been predecided?

#### Cyril Cohen (Oct 10 2023 at 10:29):

Julin Shaji said:

How can we get the function used to build the matrix in `\matrix`?

It's `matrix_of_fun`

#### Cyril Cohen (Oct 10 2023 at 10:31):

Julin Shaji said:

Cyril Cohen said:

Indeed for now the only library I know that performs that is CoqEAL but it's limited to computations of concrete matrices.

Concrete as in matrices whose dimensions have been predecided?

Concrete as in a closed term: dimensions are concrete fixed numbers, and the general term is a function that uses no other variable than the two indices

#### Julin Shaji (Oct 10 2023 at 10:36):

Cyril Cohen said:

Julin Shaji [said](https://coq.zulipchat.com/#narrow/stream/237664-math-comp-

It's `matrix_of_fun`

Okay, so the other way must be `fun_of_matrix`. :+1:

#### Cyril Cohen (Oct 10 2023 at 10:38):

Julin Shaji said:

Cyril Cohen said:

Julin Shaji [said](https://coq.zulipchat.com/#narrow/stream/237664-math-comp-

It's `matrix_of_fun`

Okay, so the other way must be `fun_of_matrix`. :+1:

Ah sure, I misread your question. This function is actually a coercion btw.

#### Emilio Jesús Gallego Arias (Oct 10 2023 at 11:53):

Indeed @Julin Shaji you don't need to use `fun_of_matrix` usually, Coq should be smart and insert it for you.

The way this works is that when you write

``````n : nat, A : 'M_n, i j : 'I_n |- A i j
``````

Coq will fail to typecheck the application `A i j` , however, the coercion mechanism knows that it can insert `fun_of_matrix` to try to repair the problem, so indeed, Coq will automatically convert `A i j` to `fun_of_matrix A i j`.

`fun_of_matrix` is not displayed by default, but can do so if you wish.

#### Julin Shaji (Oct 12 2023 at 16:26):

Given a `'M[R]_(n,m)`, is there a way to get the (i, j)-th element of it?

I tried `A i j`, but that gives a big term. Is there a way to get a 'slim' form with just the element?
Just to see it.

#### Emilio Jesús Gallego Arias (Oct 12 2023 at 16:28):

Hi @Julin Shaji , does `rewrite !mxE` improve what you see?

#### Emilio Jesús Gallego Arias (Oct 12 2023 at 16:28):

I'm afraid that without a more complete example I'm not sure how to help further

#### Emilio Jesús Gallego Arias (Oct 12 2023 at 16:29):

In math-comp, `A i j` will not reduce by default, as to better control some aspects of the proofs, thus you usually need to use `rewrite !mxE.` as to "normalize" the matrix rep.

#### Julin Shaji (Oct 12 2023 at 16:30):

No, as in how a novice would try first. :halo:

``````Example eg4 := \matrix_(i<3, j<3)
(fun i j => i+j%:Z).
(* Example eg4 := \matrix_(i<3, j<3) (i+j).   *)

Compute eg4 0 1.
``````

Would going in to proof mode reduce the term?

#### Julin Shaji (Oct 12 2023 at 16:32):

Just for someone who's curious to see an element of the matrix.

#### Emilio Jesús Gallego Arias (Oct 12 2023 at 16:32):

Indeed that's what we mean when we say "math-comp matrices are not designed for computing"

#### Emilio Jesús Gallego Arias (Oct 12 2023 at 16:33):

indeed you need to use the proof mode to rewrite the expression symbolically; there are hacks to do so with `Compute`, but they are hacks so IMHO not worth it.

#### Emilio Jesús Gallego Arias (Oct 12 2023 at 16:38):

``````Variable (R: ringType).

Example eg4 : 'M[R]_(3,3) :=
\matrix_(i<3, j<3) (i%:R + j%:R).

Theorem foo : eg4 0 1 = eg4 1 0.
Proof. rewrite /eg4 !mxE /=. Qed.
``````

#### Julin Shaji (Oct 12 2023 at 16:38):

Yeah, I was just curious if there was a way to see a specific element for curiosity's sake. :melting_face:
Definitely not for real usage.

#### Emilio Jesús Gallego Arias (Oct 12 2023 at 16:38):

Yup, that's the way

t

Thanks!

#### Emilio Jesús Gallego Arias (Oct 12 2023 at 16:39):

The type of `mxE` is interesting:

``````mxE : forall [R : Type] [m n : nat] (k : unit) (F : 'I_m -> 'I_n -> R), \matrix[k]_(i, j) F i j =2 F
``````

Most welcome!

#### Emilio Jesús Gallego Arias (Oct 12 2023 at 16:39):

So as you see, it is just an unwrapping of the `\matrix[]_(i,j)` notation; this pattern is used along all the math-comp library

#### Paolo Giarrusso (Oct 12 2023 at 18:18):

`Proof. rewrite /eg4 !mxE /=. Qed.` <- that's not meant to work, or do I miss yet more magic?

#### Emilio Jesús Gallego Arias (Oct 12 2023 at 18:22):

@Paolo Giarrusso it is indeed missing a last rewrite step, but that's not a problem in my editor.

#### Emilio Jesús Gallego Arias (Oct 12 2023 at 18:23):

I got used to write lemmas like that, finish the proofs later on.

#### Emilio Jesús Gallego Arias (Oct 12 2023 at 18:23):

even stating a false goal just to do the computation is reasonable — just always ask if it's 42 :-) `Goal eg4 0 1 = 42.`