sara lee (Aug 26 2021 at 16:23): 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.
sara lee (Aug 26 2021 at 16:33):Thank you.
sara lee (Aug 26 2021 at 16:36):OK, I open this link.
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 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
zohaze (Sep 28 2021 at 01:16):Difference between Fin.t & vector.t ? Under what conditions use of vector is helpful?
Last updated: Sep 23 2023 at 14:01 UTC