Stream: Coq users

Topic: Implement matrixes


view this post on Zulip 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).

view this post on Zulip 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.

view this post on Zulip sara lee (Aug 26 2021 at 16:33):

Thank you.

view this post on Zulip sara lee (Aug 26 2021 at 16:36):

OK, I open this link.

view this post on Zulip 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.

view this post on Zulip 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].

view this post on Zulip 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)

view this post on Zulip 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 .

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip zohaze (Sep 26 2021 at 12:03):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip zohaze (Sep 28 2021 at 01:16):

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


Last updated: Feb 08 2023 at 23:03 UTC