## Stream: Coq users

### Topic: Implement matrixes

#### sara lee (Aug 26 2021 at 16:23):

I want to write matrix in Coq. Please suggest from where I should start study(name reference book or any other helping material).

#### Enrico Tassi (Aug 26 2021 at 16:27):

One library with a formalization of matrixes is MathComp.
Their definition is also briefly explained in the MathCompBook page 150.

Thank you.

#### sara lee (Sep 18 2021 at 02:57):

I want to read matrix (axb) and then represent values of different rows(a) and columns(b) in the list. I have done pattern matching on a and b. When column(b) is equal to 1 then reduce order of row by 1 then recursively call the function . But it has some problem.Please guide me.

#### sara lee (Sep 19 2021 at 05:12):

For example [3 4 1 2
5 3 2 8
1 4 9 5
7 5 5 8] This is 4x4 matrix. I want to write it in the form of natural number list.Like [3,4,1,2,5,3,2,8,1,4,9,5,7,5,5,8].

#### Karl Palmskog (Sep 19 2021 at 05:51):

there is a refinement of MathComp matrices to lists of lists here: https://github.com/coq-community/coqeal (`seqmx`)

#### sara lee (Sep 19 2021 at 06:10):

I am new in this field. There are multiple files . I have no idea from where to start. It would be better if you give me some example ,folder,page no .

#### Karl Palmskog (Sep 19 2021 at 09:43):

based on my experience, there is no going from beginner to advanced (`seqmx.v` file I mentioned) with Coq in days or even weeks - it's going be months, typically. Enrico already mentioned the Mathematical Components book above. I'd recommend working through that book completely and looking through material like this: https://github.com/math-comp/tutorial_material
... and then, going back to matrix algebra specifically.

#### zohaze (Sep 20 2021 at 23:27):

To represent data in the form of matrix from list reference document is also useful ? I want to identify element by its position in row and column only or there is any other way for this representation?

#### Karl Palmskog (Sep 21 2021 at 07:40):

here is one way to do a two-dimensional matrix as a list: https://github.com/coq-community/sudoku

#### zohaze (Sep 22 2021 at 17:08):

I have defined matrix by using vector like this
Definition vector := list.
Definition matrix A := list (vector A).
Now with the help of Vector how can access different rows and columns of axb matrix?

#### Mukesh Tiwari (Sep 23 2021 at 02:11):

@zohaze Have a look at https://github.com/fblanqui/color/blob/master/Util/Matrix/Matrix.v. It's not exactly you are looking but almost close.

#### zohaze (Sep 26 2021 at 12:02):

@Karl Palmskog. Thank you. I have few questions regarding to reference you have given. 1) Arguments of definition cross in Sudoku are (h w:nat) (l:list nat) ,I want to ask (p:Pos x y) is also an input argument because used in the definition cross? 2) Plz explain definition with example.3) I want to compute it like Compute cross 2 2 [3 ,4,6,8]. 4) square matric having elements in the form of Pos x y will be convert into list of Pos x y?

#### zohaze (Sep 26 2021 at 12:03):

Thank you @ Mukesh Tiwari .I will study your sended reference.

#### Karl Palmskog (Sep 26 2021 at 13:28):

I've no idea about the encoding specifics of the Sudoku formalization, you probably want to read this: https://hal.inria.fr/hal-03277886/document

#### zohaze (Sep 26 2021 at 18:48):

Ok, to convert a list into rows and columns I should work on this line? Have 2x2 matric, size=4 .In the form of list [e11 e12 e21 e22]I should define a function to get an element of the list at Pos x y .Like get Pos 2 1 [e11 e12 e21 e22],then it should give e21. If i=1 row 1= e11 e12 row2=e21 e22 col1=c11 c21 col2=e12 e22

#### Laurent Théry (Sep 27 2021 at 09:36):

In the Sudoku, if you have a matrix with `m` rows and `n`columns. It is represented as a list of size `m*n`. If you want to look at position `Pos x y` (row `x` and column `y`) you go at position ` x * n + y` in the list

#### zohaze (Sep 28 2021 at 01:16):

Difference between Fin.t & vector.t ? Under what conditions use of vector is helpful?

Last updated: Jun 18 2024 at 09:02 UTC