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

One library with a formalization of matrixes is MathComp.

Their definition is also briefly explained in the MathCompBook page 150.

Thank you.

OK, I open this link.

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.

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

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

)

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 .

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.

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?

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

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?

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

@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?

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

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

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

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

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

Last updated: Sep 23 2023 at 14:01 UTC