The Coq mailing list

[mukesh tiwari <mukeshtiwari.iiitm AT gmail.com>]

Thanks Josh! Very helpful. 

Best,

Mukesh

On Mon, 25 Apr 2022 at 16:13, Joshua Cohen <jmc16 AT princeton.edu> wrote:

Hi Mukesh,

One way to do this is to use your Vector <-> Fin.t conversion functions to define versions that work on 2D Vectors (ie, your Matrix type) and then to convert between Fin.t n and Ordinal n, the type that MathComp matrices are indexed by:

https://gist.github.com/joscoh/e3bc94a35a932c1ade39bae7385cf104

This method is nice because it makes it easy to index into your matrices, in both directions.

Thanks,

Josh

On Sun, Apr 24, 2022 at 10:29 AM mukesh tiwari <mukeshtiwari.iiitm AT gmail.com> wrote:

Hi everyone,

I plan to use the matrix inverse function [1] in my project, but in
another part of the
project matrix is defined as, 'Definition Matrix R n m := Vector.t
(Vector.t R n) m'.
My question is how can I convert 'Matrix R n m' to 'M[R]_n (matrix R n n) and
back. Basically, I need two functions:
1. f  : Matrix R n n -> 'M[R]_n
2. g : 'M[R]_n -> Matrix R n n


If it is any helpful, I can easily
turn a vector, Vector.t R n, into a finite function, Fin.t n -> R, [2]
and vice versa [3] that
I learned from  [4] (Programming Systems Lab, Saarland University github page).


Best,
Mukesh


[1] https://math-comp.github.io/htmldoc/mathcomp.algebra.matrix.html#MatrixInv
[2] https://gist.github.com/mukeshtiwari/60f7974383fe9760ee57eef2026c27ad#file-matfin-v-L48
[3] https://gist.github.com/mukeshtiwari/60f7974383fe9760ee57eef2026c27ad#file-matfin-v-L62
[4] https://github.com/uds-psl/base-library/blob/master/Vectors/Vectors.v