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?

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

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

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

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.

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)".
*)
```

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

worked though.

But that seems to leave holes.

```
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
*)
```

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

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?

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?

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

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

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?

Some example files might also help ...

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?

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

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

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

?

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

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?

Julin Shaji said:

How can we get the function used to build the matrix in

`\matrix`

?

It's `matrix_of_fun`

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

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:

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.

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.

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.

Hi @Julin Shaji , does `rewrite !mxE`

improve what you see?

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

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.

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?

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

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

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.

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

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.

Yup, that's the way

t

Thanks!

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!

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

`Proof. rewrite /eg4 !mxE /=. Qed.`

<- that's not meant to work, or do I miss yet more magic?

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

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

as they'll be auto-admitted

It is a game changer for me.

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

Last updated: Jul 15 2024 at 21:02 UTC