The Coq mailing list

[Matthew Rocklin <mrocklin AT cs.uchicago.edu>]

Hello Coq community,

I am interested in developing systems to answer questions about matrix expressions like the following:

Given that 

A and B are both matrices

A is symmetric and positive definite 

B is orthogonal

C = B.T * A * B

is C symmetric?

is C positive definite? 

This was also posted as a question on scicomp.stackexchange.com

http://scicomp.stackexchange.com/questions/74/symbolic-software-packages-for-matrix-expressions

A colleague recently suggested that I look at Coq. After a brief inspection and looking at some of the linear algebra codes already developed I have become quite interested. Before devoting significant time to this project I would like to ask the community's perspective. 

Some questions

1) Is Coq likely to be able to produce a black-box solver for questions like these? My solution must be fully automated. 

2) What types of questions are likely to be easy and what types are likely to be difficult?

3) Is there a simpler method to solve my problem? Perhaps Coq is overkill. Can anyone recommend a tool more appropriate for this problem?

I appreciate your time, 

-Matthew

--

Matthew Rocklin

University of Chicago - Computer Science PhD Student

http://people.cs.uchicago.edu/~mrocklin