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.
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 (
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
ncolumns. 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