Matrix transpose · Coq users · Zulip Chat Archive

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

Paolo Giarrusso (Oct 03 2023 at 09:43):

Actually, here's an option: https://coq.discourse.group/t/proving-matrix-transpose-function/803/10?u=blaisorblade

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.
  Proof. by rewrite addrC. Qed.
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].

[1] https://github.com/mukeshtiwari/secure-e-voting-with-coq/blob/master/Groups/Matrix.v

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: Oct 08 2024 at 14:01 UTC