## Stream: Coq users

### Topic: Matrix transpose

#### Julin Shaji (Oct 03 2023 at 05:57):

Hi.

I was trying to find the transpose of a matrix implemented as vector of vectors.

How would we go about that?

I tried:

``````Fixpoint trans {A: Type} {rows cols: nat}
(mat: matrix A rows cols): matrix A cols rows :=
match mat with
| [] => []
| _ =>
let rw := Vector.map hd mat in
let mat' := Vector.map tl mat in
rw :: (trans mat')
end.
``````

and got errors all over.

Or would it be better to implement with lists and convert to vector only as needed?

#### Paolo Giarrusso (Oct 03 2023 at 08:51):

The usual advice is: avoid `Vector` entirely and/or switch to equations and/or use something like mathcomp's `tuple`, basically `tuple A n := { xs : list A | length xs = n}`

#### Julin Shaji (Oct 03 2023 at 09:18):

Does using Equations alone help? I'm not familiar with it, but isn't that to make proofs involving recursions easier or something along those lines?

#### Paolo Giarrusso (Oct 03 2023 at 09:37):

It also helps with dependent pattern matching

#### Julin Shaji (Oct 03 2023 at 10:11):

mathcomp already has some definitions and proof involving matrix, right?
https://github.com/math-comp/math-comp/blob/master/mathcomp/algebra/matrix.v

Can they be reused just like that? For example finding the transpose of a matrix represented as a list of lists?
Or are they meant to be used only within mathcomp? Any idea?

#### Julin Shaji (Oct 03 2023 at 10:11):

Does any one know of some examples of using the mathcomp version of `matrix`? The docs by itself looks a bit intimidating at first.

#### Julin Shaji (Oct 03 2023 at 10:12):

Feels like one has to know much other mathcomp definitions before one start to use matrix definition.

#### Pierre Roux (Oct 03 2023 at 11:14):

One can read Section 7.8 of the MathComp book https://zenodo.org/record/7118596 Note that mathcomp matrices are abstract functions, not lists of lists but CoqEAL offers a refinement enabling to develop all proofs with the nice matchomp matrices and refine them with lists of lists if you need to perform actual computations: https://github.com/coq-community/coqeal/ (CoqEAL itself is unfortunately not very well documented)

#### djao (Oct 03 2023 at 12:17):

https://proofassistants.stackexchange.com/questions/2104/how-to-prove-this-correctness-principle-of-transposition-of-lists-of-lists-in-co is relevant if you are ok with lists of lists

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

Pierre Roux said:

Note that mathcomp matrices are abstract functions, not lists of lists

Thanks. Does that mean we cannot extract out (as in to ocaml) those matrix elements in any way?

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

djao said:

https://proofassistants.stackexchange.com/questions/2104/how-to-prove-this-correctness-principle-of-transposition-of-lists-of-lists-in-co is relevant if you are ok with lists of lists

How is the matrix constraint being satisfied in this version of `transpose`?
https://gist.github.com/davidjao/1a857a3c2d39dfec5cde0339d742be10#file-awesomelistlemmas-v-L266

Matrix seems to be represented just as `list (list A)` without any constraint (or am I missing something?).
Wouldn't that cause problem?

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

And how does CoLoR look up on the matrix front?
I mean, is it easy to work with?

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

@Julin Shaji the key question about matrices is whether you want to find a representation that is "extensional", that is to say , two matrices A B are equal in Coq iff `forall i j, A i j = B i j`

This is super-convenient for proving (and defining things, transpose is just `tr A := \matrix_(i, j) A j i`, however it doesn't yield the representation you'd expect (sadly, as there is no deep reason)

When that happens, there are several choices; a sensible one IMHO is to use program refinement to do your proofs on the extensional representation, but computations on a lower-level one. See the work on CoqEAL.

#### Julin Shaji (Oct 03 2023 at 16:01):

Emilio Jesús Gallego Arias said:

Julin Shaji the key question about matrices is whether you want to find a representation that is "extensional", that is to say , two matrices A B are equal in Coq iff `forall i j, A i j = B i j`

Probably a trivial question, but if `forall i j, A i j = B i j` is extensional proof, how could a more involved one look like?
(Is that called 'intentional' proof or something?)

#### Julin Shaji (Oct 03 2023 at 16:02):

Ah.. I guess that means it has to be exactly similar. Constructor-wise itself.

#### Julin Shaji (Oct 03 2023 at 16:02):

As in not just the meaning, but the structure itself has to be same as well.

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

Yes, so that's why is a bit tricky

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

Let me write lemma more exactly: `Lemma matrixP R n m (A B : matrix R n m) : (A = B) <-> (forall i j, A i j = B i j).`

#### Emilio Jesús Gallego Arias (Oct 03 2023 at 16:05):

So you use this lemma to prove a lot of stuff, for example, you can trivially show with it that matrix addition is associateive and commutrative, etc...

#### Emilio Jesús Gallego Arias (Oct 03 2023 at 16:05):

(if the underlying operator on `R` is, of course)

#### Paolo Giarrusso (Oct 03 2023 at 17:55):

Why's extensionality hard? Doesn't it just work with lists of lists and partial lookups?

#### Paolo Giarrusso (Oct 03 2023 at 17:55):

(of course, with functions you'd need funext)

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

@Paolo Giarrusso for simple cases it may be easy, but think for example of more complex matrix representations for calculus, that may be sparse, use non-canonical pasting techniques, etc...

#### Emilio Jesús Gallego Arias (Oct 03 2023 at 18:20):

Also defining the "partial lookup" may be tricky, a subtype works but you need to use something like math-comp infra to make it usable IMVHO

#### Paolo Giarrusso (Oct 03 2023 at 18:42):

lookup : nat -> list A -> option A

#### Paolo Giarrusso (Oct 03 2023 at 18:54):

or in this case, probably `lookupMat : nat -> nat -> matrix A -> option A` — that's enough to get `(A = B) <-> (forall i j, lookupMat i j A = lookupMat i j B).`

#### Paolo Giarrusso (Oct 03 2023 at 18:55):

not saying that's enough for all cases, but sparse matrixes seem off-topic in this thread.

#### Emilio Jesús Gallego Arias (Oct 03 2023 at 18:56):

Would that definition admit a group / nonCom ring structure?

#### Emilio Jesús Gallego Arias (Oct 03 2023 at 18:56):

Yup that def works, but may not be fully usable, depending on your context. I see other efforts like QWIRE went and defined matrices as functions (+ funext), so indeed YMMV.

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

I'd rephrase my thoughts on that as "you need to have a usable matrix definition for your case, it may be or may not be extensional, it is common that extensional representations are not good for computing, and non-extensional representation making resoning too hard, so in this case you'd have to use program refinement techniques"

#### Paolo Giarrusso (Oct 03 2023 at 18:58):

@Julin Shaji I guess the key question is how much are you going to use your matrices, is this a small exercise or do you plan to use this a lot in a large project? The more you use it, the more it makes sense to invest in advanced techniques

#### Paolo Giarrusso (Oct 03 2023 at 18:59):

e.g. math-comp definitely has a learning curve

#### Emilio Jesús Gallego Arias (Oct 03 2023 at 19:00):

Yes, the math students I've taken here usually become productive with math-comp matrices from 0 like in 2 months, but we code together often

#### Emilio Jesús Gallego Arias (Oct 03 2023 at 19:00):

It has a learning curve, and their representation doesn't compute without CoqEAL

#### Emilio Jesús Gallego Arias (Oct 03 2023 at 19:00):

that's not an easy obstacle

#### Paolo Giarrusso (Oct 03 2023 at 19:02):

(and to Emilio's question, I'm not 100% sure lists of lists form a group)

#### Emilio Jesús Gallego Arias (Oct 03 2023 at 19:10):

[I'm getting offtopic, but indeed I was trying to figure out how much simpler you can make an extensional matrix representation and still keep most of the nice properties of math-comp's matrices, like the isntances for algebraic structures, for example you can benefit from the fact that matrices with positive dimension over a (non) commutative ring are automatically understood by math-comp to be a nc ring. See this simpler example with an abelian group:

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

Import GRing.Theory.

Section MxEx.
Variable (R : zmodType).
Open Scope ring_scope.
Lemma mxA n m (A B : 'M[R]_(m,n)) :
A + B = B + A.
End MxEx.
```]
``````

#### Emilio Jesús Gallego Arias (Oct 03 2023 at 19:10):

Paolo Giarrusso said:

(and to Emilio's question, I'm not 100% sure lists of lists form a group)

I guess they'd do, but to make them into a ring you'd need a constraint on size, as you need `0 != 1`

#### Emilio Jesús Gallego Arias (Oct 03 2023 at 19:10):

and that's not possible for the empty matrix

#### Emilio Jesús Gallego Arias (Oct 03 2023 at 19:11):

in math-comp this is done nicely by definiting the instance to be over (square) matrices for all size n, of true size `n.+1`

#### Emilio Jesús Gallego Arias (Oct 03 2023 at 19:12):

A very nice trick when combined with bidirectional type checking but that's offtopic.

#### Julin Shaji (Oct 04 2023 at 07:19):

Paolo Giarrusso said:

Julin Shaji I guess the key question is how much are you going to use your matrices, is this a small exercise or do you plan to use this a lot in a large project? The more you use it, the more it makes sense to invest in advanced techniques

I just need a representation of matrix which can be defined over a semiring. But I need it to be extractable.
Just need matrix addition and multiplication, padding with blocks of matrices to make square matrices and the like (I'm apprehensive whether I described it properly).

CoqEAL's refinement stuff sounds way better than what I had been trying till now (`Vector.t A n`).
I can get familiar with mathcomp notations, I think. But I guess the style in which proofs are done needs some time to get familiar with.

#### Julin Shaji (Oct 04 2023 at 07:20):

I'm wondering how `\matrix` can be refined down to a vector form.
I guess it first needs to be converted to a representation in terms of `seq`?

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

`M := \matrix_(i, j) A i j` is used as a function, so you can just init a `seq` using a comprehension.

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

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

Section MxEx.
Variable (R : zmodType).
Open Scope ring_scope.
Definition a n (A : 'cV[R]_n) : n.-tuple R :=
[tuple A i 0 | i < n].
End MxEx.
``````

#### Mukesh Tiwari (Oct 08 2023 at 12:43):

Julin Shaji said:

I'm wondering how `\matrix` can be refined down to a vector form.

I have written one such implementation to move back and froth between ssreflect and coq [1].

#### Karl Palmskog (Oct 08 2023 at 12:44):

isn't it easier to go from MathComp matrices to lists to vectors (or other way around)? https://github.com/coq-community/coqeal/blob/master/refinements/seqmx.v

Last updated: Jun 22 2024 at 15:01 UTC